Integrating Formal Methods to Bridge Abstract and Concrete Representations of Security Protocols

Abstract

Confidence in a communication protocol’s security is a key requirement for its deployment
and long-term maintenance. This thesis focuses on integrating techniques for
the understanding of protocols, attacks, and fast prototyping of both. The technical
advantages of formal verification over manual testing are increasingly recognised in
the cybersecurity community. However, applying formal methods, even in their more
practical forms, outside highly specialised research settings remains challenging. For
practitioners, formal modelling and verification are often too complex and unfamiliar
to be used routinely. Our approach consists in making formal methods more accessible
to the general developer, and bridge the gap between abstract and concrete modelling,
being from a mental or specification standpoint.
Firstly, we propose a code generation approach to automatically build both an abstract
specification and a concrete implementation of a Dolev-Yao intruder from an abstract
attack trace, bridging the gap between theoretical attacks discovered by formal means
and practical ones. We focus on attack traces from the OFMC model checker,Alice & Bob
specifications and Java implementations. We introduce a proof-of-concept workflow for
concrete attack validation that allows to conveniently integrate formal methods results
into a Model-Driven Development process and automatically generate a program that
allows to demonstrate the attack in practice.
Secondly, we operate the translation from provable Alice & Bob to F⋆, leveraging the
DY⋆ library. The rationale is to address the expressivity gap issue between abstract and
concrete specifications, while providing flexibility to the user. We generate code from
an abstract model to a general-purpose language that supports proof mechanisms upon
arbitrary code. What could not be expressed at a high level could be detailed after
code generation, without loosing proof capabilities on the final amended implementation.
This enables a non-expert in formal languages to start from an easy-to-understand Alice
& Bob notation, observe a created formal-backed implementation without spending
considerable time and effort writing one from scratch, and amend the implementation
while verifying the correctness of the edits. This code generation is applied to several
real-world protocols, and illustrates the application of an end-to-end verification workflow.
Finally, we leverage lightweight and practical formal methods, to offer a more accessible
alternative to traditional fully formalised techniques by focusing on simplified models
and tool support. We then present an Eclipse Integrated Development Environment
for the design, verification, and implementation of security protocols and evaluate its
effectiveness, including feedback from users in educational settings. It offers user-friendly
assistance in the formalisation process as part of a Model-Driven Development approach.
This IDE centres around the Alice & Bob (AnB) notation, the AnBx Compiler and Code
Generator, the OFMC model checker, and the ProVerif cryptographic protocol verifier.
We surveyed master-level students on their knowledge prior to completing their projects,
and noticed considerable misconceptions. After project completion, we asked them to
report on their experience with our IDE. Our findings demonstrate that this contribution
is valuable as a workflow aid and helps users grasp essential cybersecurity concepts, even
for those with limited knowledge of formal methods or cryptography.

Date of Award	29 Apr 2026
Original language	English
Awarding Institution	Teesside University
Supervisor	Paolo Modesti (Supervisor), Shengchao Qin (Supervisor) & Leo Freitas (Supervisor)