Details of Grant 

EPSRC Reference:	EP/P002692/1
Title:	Verification of cryptographic protocols: modular analysis of equivalence properties
Principal Investigator:	Arapinis, Dr M D
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Sch of Informatics
Organisation:	University of Edinburgh
Scheme:	First Grant - Revised 2009
Starts:	01 November 2016	Ends:	30 September 2018	Value (£):	97,773
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:	Panel Date Panel Name Outcome 10 Jun 2016 EPSRC ICT Prioritisation Panel - Jun 2016 Announced
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.ed.ac.uk