PhD in End-to-End Verification of Security Protocols in Isabelle

Overview

The University of Exeter Department of Computer Science offers a PhD project focused on the end-to-end verification of security protocols in Isabelle. Modern security systems rely on complex software to translate programs into automatically checkable forms. To establish trust, the verified representation must faithfully capture the intended program. This research investigates the use of theorem proving to establish end-to-end guarantees.

The research concentrates on verified translations between programs and security protocol representations, utilizing Isabelle/HOL as the primary formalisation environment. Zero-knowledge proof systems, including STARK-style protocols, serve as a key application area. The central objective is connecting programs, compilation, and cryptographic protocols to ensure correctness and security guarantees compose and are reusable. The work encompasses formal methods, programming languages, cybersecurity, and cryptography, allowing the student to influence the direction based on personal interests.

Who can apply

Candidates interested in formal verification, programming languages, cybersecurity, cryptography, compilers, or theorem proving are suited for the project. Prior experience with Isabelle or zero-knowledge proofs is useful but not essential.

What you get

The studentship provides funding for fees and an annual stipend of £21,805 for the 2026/7 academic year.

Key dates

The closing date for applications is 2026-12-08.