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.
On the event of the adoption of the draft regulation laying down measures for a high common level of cybersecurity at the institutions, bodies, offices and agencies of the Union, the AI4HealthSec project kicked off a process to provide its opinion.
Cyberwatching.eu has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 740129. The content of this website does not represent the opinion of the European Commission, and the European Commission is not responsible for any use that might be made of such content. Privacy Policy | Disclaimer / Terms and Conditions of Use