Supervisors

Suitable for

Abstract

In large satellite networks, particularly interplanetary networks, key management is currently an unsolved problem - pre-shared keys become infeasible due to the large number of nodes in the network, and PKI is made more difficult due to the long distances and intermittent connectivity between nodes. Recent work within our group makes use of a network simulator to test the suitability of terrestrial PKI to large-scale satellite systems, finding that it can be used with a small number of modifications. This project would seek to extend this work with the aid of formal verification techniques, seeking to formally establish convergence properties, time bounds, and the ordering of actions for a given network topology and PKI system.

Prerequisites This project will require an understanding of formal verification techniques,
network protocols, and a basic understanding of key management/revocation techniques.

Useful URLs https://arxiv.org/abs/2408.10963v3