ANR Project TECAP
TECAP: Protocol Analysis - Combining Existing Tools
ANR-17-CE39-0004-01
Summary
Formal methods have been shown successful in proving security of cryptographic protocols and finding flaws.
However manually proving the security of cryptographic protocols is hard and error-prone.
Hence, a large variety of automated verification tools have been developed to prove or find attacks on protocols.
These tools differ in their scope, degree of automation and attacker models.
Despite the large number of automated verification tools, several cryptographic protocols still represent a real challenge for these tools and reveal their limitations.
The aim of this project is to get the best of all these tools, meaning, on the one hand, to improve the theory and implementations of each individual tool towards the strengths of the others and, on the other hand, build bridges that allow the cooperations of the methods/tools. We will focus in this project on the tools CryptoVerif, EasyCrypt, Scary, ProVerif, Tamarin, AKiSs and APTE. In order to validate the results obtained in this project, we will apply our results to several case studies such as the Authentication and Key Agreement protocol from the telecommunication networks, the Scytl and Helios voting protocols, and the low entropy authentication protocols 3D-Secure. These protocols have been chosen to cover many challenges that the current tools are facing.
The aim of this project is to get the best of all these tools, meaning, on the one hand, to improve the theory and implementations of each individual tool towards the strengths of the others and, on the other hand, build bridges that allow the cooperations of the methods/tools. We will focus in this project on the tools CryptoVerif, EasyCrypt, Scary, ProVerif, Tamarin, AKiSs and APTE. In order to validate the results obtained in this project, we will apply our results to several case studies such as the Authentication and Key Agreement protocol from the telecommunication networks, the Scytl and Helios voting protocols, and the low entropy authentication protocols 3D-Secure. These protocols have been chosen to cover many challenges that the current tools are facing.
Partners
Inria Nancy
Inria Paris
Inria Sophia Antipolis
IRISA
LIX
LSV-ENS Cachan
Detailed description of the project
Submission document (Avril 2017)Project Meetings
- 14/03/2018 - Kick-Off meeting in Cachan
- 08/07/2019 - Meeting in LIX
- 09/10/2020 and 15/10/2020 - Meeting Online
- 16/06/2022 - Joint Hubert Comon Retirement Workshop - Final TECAP meeting
Documents
Tools developed during the project
- AKISS: Tool for checking trace equivalence for security protocols
- APTE: Algorithm for Proving Trace Equivalence
- CryptoVerif: Cryptographic protocol verifier in the computational model
- DeepSec: DEciding Equivalence Properties in SECurity protocols
- EasyCrypt: Computer-Aided Cryptographic Proofs
- ProVerif: Cryptographic protocol verifier in the formal model
- Scary
- Tamarin ProVer
- Squirrel Prover