Verification of cryptographic protocols: modular analysis of equivalence properties

Our societies are critically dependent on computerised systems. Unfortunately, and as often reported by the media, the mechanisms employed for defending these systems against malicious offensives are repeatedly defeated, seriously threatening our individual security and privacy. Rigorous and formal analysis of sensitive computerised systems thus needs to be conducted before their deployment, to exclude the existence of security vulnerabilities.

Formal verification techniques have proved very useful so far for analysing the security and privacy guarantees of digital systems. However, existing technologies fail to handle many nowadays real-life systems, as these become more and more complex, and their intended properties become more and more subtle. For example, the UMTS standard specifies tens of sub-protocols running in composition in 3G mobile phone systems. But, our tools have not kept pace with the growing complexity of nowadays systems. Currently, one may hope to automatically verify some of the sub-components of a system in isolation, but it is unrealistic to expect that the whole protocol suite can be automatically checked using one and the same tool.

In order to enable automatic analysis of privacy of crypto-protocols underlying complex real life , this research project will develop theoretical composition results for equivalence properties and integrate them to existing tools. Such results will permit to leverage state-of-the-art protocol analysers. The idea being to enable automatic verification by applying the divide-and-conquer strategy, with the goal to infer global security and privacy properties of complex systems from local properties of their components.

A very important aspect of this project is that it will ground the theoretical investigations in the needs of real-world computerised systems, to ensure the achievement of significant and applicable results and impact. We will focus on at least three applications important to society: electronic voting which is attracting government and industry interest, mobile telephony which is used daily by billions of subscribers everywhere they go, and electronic passports of which 40 countries have together issued many millions. These three applications raise numerous security and privacy concerns resulting in failure of confidence among users, politicians, commentators and public alike.

In short, the combination of theoretical outcomes of this project (and their implementation) with readily available cryptographic protocol analysers are the exact combination needed for fully-automated analysis of many modern sensitive applications.

The following will benefit from our research:

* The wider public. Improving the privacy guarantees of very widely deployed systems such as mobile telephony systems will primarily benefit every one of us.

* Private sector. Providers of sensitive applications will be able to improve the security and privacy guarantees of their systems by using our tools. The ICAO and 3GPP consortium will in particular also benefit from the outcomes of our analysis of the new generation of electronic passports and mobile telephony systems.

* Public sector such as governments. Our results will help analyse, and design better electronic voting systems. These promise an efficient and convenient way for conducting elections, avoiding human errors in tallying.

* Research community across several areas of security. They will gain insights to where some of the challenges in security verification lie. This work will also shed light for them on subtle pitfalls in the development of a secure system.



They will benefit in the following ways:

1. The project will provide usable and effective techniques and software tools;

2. The project will provide guidance (prudent engineering techniques) for designing new secure sensitive applications.



To deliver the impact, we shall do the following:

* Establish industrial collaborations with the 3GPP consortium (and its successor) in charge of developing the UMTS standard (and the next generation mobile standard respectively), and the ICAO in charge of developing the standards for electronic passports. We have already been in contact with these two consortiums in the past, when earlier works of ours brought to the light security vulnerabilities in these systems.

* Provide packaged solutions for industry to evaluate.

* Continue active interaction with leading researchers on security verification such as Ve 'ronique Cortier and Steve Kremer from LORIA in France, Mark Ryan and Tom Chothia from the University of Birmingham in the UK, or Ste 'phanie Delaune from LSV in France.

* Publish the results of our research in top venues to ensure maximum visibility.

* Deliver seminars, public lectures, and enhance existing and create new teaching modules based on the outcomes of this project.