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.