Verification of cryptographic protocols: modular analysis of equivalence properties

我们的社会严重依赖于计算机化系统。不幸的是，正如媒体经常报道的那样，用于保护这些系统免受恶意攻击的机制一再失败，严重威胁到我们的个人安全和隐私。因此，需要在部署敏感的计算机化系统之前对其进行严格和正式的分析，以排除存在的安全漏洞。到目前为止，形式验证技术已被证明对分析数字系统的安全性和隐私保证非常有用。然而，现有的技术无法处理当今许多现实生活中的系统，因为这些系统变得越来越复杂，它们的预期属性变得越来越微妙。例如，UMTS标准规定了在3G移动电话系统中以组合形式运行的数十个子协议。但是，我们的工具并没有跟上当今系统日益复杂的步伐。目前，人们可能希望独立地自动验证系统的一些子组件，但是期望使用同一个工具自动检查整个协议套件是不现实的。为了能够自动分析复杂现实生活中加密协议的隐私，本研究项目将开发等效属性的理论组成结果，并将其集成到现有工具中。这样的结果将允许利用最先进的协议分析器。其思想是通过应用分而治之的策略来实现自动验证，其目标是从复杂系统组件的局部属性推断出复杂系统的全局安全和隐私属性。这个项目的一个非常重要的方面是，它将理论研究在现实世界的计算机化系统的需求，以确保实现显著和适用的结果和影响。我们将重点关注至少三种对社会重要的应用：吸引政府和工业界兴趣的电子投票，每天有数十亿用户无论走到哪里都在使用的移动电话，以及40个国家总共发行了数百万本的电子护照。这三个应用程序引起了大量的安全和隐私问题，导致用户、政治家、评论员和公众都失去了信心。简而言之，这个项目的理论成果（及其实现）与现成的加密协议分析器的结合是许多现代敏感应用程序全自动分析所需的确切组合。

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.