This projet is managed by ANSSI. To find out more, you can go to the page (in French) dedicated to the ANSSI open source strategy. You can also click on the badges above to learn more about their meaning
This repository contains the support material for the article published at Computer Security Foundations 2025.
Formal analysis on random nonce misuse in cryptographic protocols, G. Avoine, T. Claverie, S. Delaune.
It is composed of three main parts:
- A parser for Tamarin files, that allows recovering and rewriting the Abstract Syntax Tree of .spthy files (folder parser);
- Models of protocols used in the study (folder study);
- A server to configure the analysis and sumarizes the results for a given model (folder server).
The server and models are tightly linked to the original goal of the study, namely the study of random misgeneration in cryptographic protocols. However, the Tamarin parser has been conceived to be independant of the study, so it could be repurposed for other types of analysis, from models modification to parsing of security proofs and attacks.