Supervisors

Suitable for

Abstract

Formal verification techniques are widely applied to assess protocol security against unconstrained attacker models with full capabilities. However, these models do not take into account the Physical Layer environment where the
communication session occurs in real-world settings which constrain the attacker capabilities.

In this project you will apply rigorous formal methods to define and analyse the security of widely-used satellite protocols, specifically anti-jamming availability and secrecy. This will be conducted with respect to these Physical Layer
attributes including the signal structure and noise power, and be derived through both simulations and measurements of real satellite channels. Thus this work is designed to directly impact and improve the development of satellite protocols.

Interested students should have some experience in formal verification and/or optimisation problems, and be confident in developing software using Python.

No prior experience in radio communications is required.