TECAP - Protocol Analysis - Combining Existing Tools

Home » TECAP - Protocol Analysis - Combining Existing Tools
01/01/2018 to 31/12/2022

Project Description:

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.

Wednesday, 12 December, 2018

Future Events

By the end of YR2, the SECREDAS project is well on its way to deliver on its promise to make automated driving secure and safe whilst giving driver's full privacy. The document provides a brief overview of the project as well as the status by July 2020.


The third Annual Fraud & Financial Crime Europe will focus on analysing the risks to determine the solutions in combating Fraud and Financial Crime.

01/09/2020 to 02/09/2020