Automatic Generation of Security Protocols Attacks Specifications and Implementations

Rémi Garcia, Paolo Modesti

Research output: Contribution to journalArticlepeer-review

12 Downloads (Pure)


Confidence in a communication protocol’s security is a key requirement for its deployment and long-term maintenance. Checking if a vulnerability exists and is exploitable requires extensive expertise. The research community has advocated for a systematic approach with formal methods to model and automatically test a protocol against a set of desired security properties. As verification tools reach conclusions, the applicability of their results still requires expert scrutiny. 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. Through our case studies, 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, in a user-friendly way, formal methods results into a Model-Driven Development process and at the same time automatically generate a program that allows to demonstrate the attack in practice. In fact, in this contribution, we produce high-level and concrete attack narrations that are both human and machine readable.
Original languageEnglish
Article number100038
Number of pages19
JournalCyber Security and Applications
Publication statusPublished - 16 Feb 2024


Dive into the research topics of 'Automatic Generation of Security Protocols Attacks Specifications and Implementations'. Together they form a unique fingerprint.

Cite this