Analysing Security and Privacy Properties

Lead Research Organisation: University of Birmingham
Department Name: School of Computer Science

Abstract

Security systems break because design practices focus too much on mechanisms, at the expense of clearly-defined properties. The vision of this research is to bring about a shift of emphasis to highlight the properties that security systems are expected to provide. This will be done by developing methods for verification of security systems. I will focus on a selection of interconnected real-world problems that are of great importance to society, but that are currently in need of greater industry/academe cooperation. The combination of fundamental research with close collaboration with industry, government and users is expected to achieve significant results and impact. I will develop and apply new methods and techniques to create and analyse solutions in three areas:* Trusted computing is an industry-led technology that aims to root security in hardware. Since its launch, academics including me have discovered significant issues that threaten to undermine its potential at providing a range of security benefits. This has arisen because industry does not have the expertise to analyse the protocols.* Electronic voting is an application currently attracting significant interest from government and industry, but numerous security issues have resulted in failure of confidence among politicians, commentators and public alike.* Privacy for citizens using electronic services is hotly debated by journalists and user groups and politicians, but has been substantially eroded by new technologies and policies.In these three areas, there is currently the risk of significant waste of resources on inappropriate or unaccepted technologies, resulting in user disempowerment and exclusion. The outcomes of this fellowship are intended to address that risk.A distinguishing feature of the proposal is the substantial engagement with industry and user groups that are active in these three areas. As a result of discussions with them, several organisations have committed significant resources, including cash contribution, manager and developer time, and access to users and experts.

Publications

10 25 50

publication icon
Arapinis M (2016) Analysis of privacy in mobile telephony systems in International Journal of Information Security

publication icon
Arapinis M (2017) Stateful applied pi calculus: Observational equivalence and labelled bisimilarity in Journal of Logical and Algebraic Methods in Programming

publication icon
Bursuc S (2012) E-Voting and Identity

publication icon
Chevalier C (2013) Composition of password-based protocols in Formal Methods in System Design

 
Title Inaugural lecture 
Description Mark Ryan's inaugural lecture. 
Type Of Art Film/Video/Animation 
Year Produced 2011 
Impact Enquiries from PhD students. 
URL http://vimeo.com/25449665
 
Title Online voting video 
Description Video about online internet voting. 
Type Of Art Film/Video/Animation 
Year Produced 2013 
Impact None yet. 
URL http://www.youtube.com/watch?v=dI7IHtHpwf4
 
Description Further development and prototype implementation of StatVerif, a technique and tool for analysing protocols with persistent state.

Formal analysis of authorisation protocols of the TPM. Formal analysis of state-based (PCR) protocols of the TPM.

Proposal of digital envelope using protocols of the TPM.

Formal analysis of direct anonymous attestation protocol.

Exposition of applied pi calculus.

Use of formal analysis to discover vulnerabilities in mobile phone protocols, and fixes.

Development of applied pi calculus with state, and soundness and completeness proofs.

Formal analysis of confidentiality-preserving cloud computing architecture.

Analysis of trade-off between privacy and security properties.

StatVerif verifier tool made publicly available online.
Exploitation Route StatVerif will be used by academics and industry interested in performing automatic analysis of protocols involving persistent state. Research can be used by designers of the TPM to improve their specifications. StatVerif will be used by academics and industry interested in performing automatic analysis of protocols involving persistent state. Research can be used by designers of the TPM to improve their specifications.
Sectors Creative Economy,Digital/Communication/Information Technologies (including Software),Financial Services, and Management Consultancy,Government, Democracy and Justice,Security and Diplomacy,Other

URL http://sec.cs.bham.ac.uk/research/StatVerif/
 
Description Findings have been used by other researchers. We expect some of them will be taken up by companies.
Sector Digital/Communication/Information Technologies (including Software),Government, Democracy and Justice,Security and Diplomacy,Other
Impact Types Societal,Economic

 
Description Advisory council member for WebRoots The Institute for Digital Democracy
Geographic Reach National 
Policy Influence Type Participation in a advisory committee
URL https://webrootsdemocracy.org/advisory-council/
 
Description Microsoft gift
Amount $45,000 (USD)
Organisation Microsoft Corporation 
Sector Public
Country United States
Start 04/2010 
 
Description Research Chair in Cyber Security
Amount £400,000 (GBP)
Organisation Hewlett Packard Ltd 
Department Hewlett Packard Laboratories, Bristol
Sector Private
Country United Kingdom
Start 09/2016 
End 08/2021
 
Title StatVerif 
Description A software tool to verify the security properties of protocols. 
Type Of Material Improvements to research infrastructure 
Year Produced 2014 
Provided To Others? Yes  
Impact Take up by other researchers 
URL https://sec.cs.bham.ac.uk/research/StatVerif/
 
Description Google 
Organisation Google
Country United States 
Sector Private 
PI Contribution Collaboration of certificate management
Collaborator Contribution Collaboration of certificate management
Impact Discussion and meetings
Start Year 2010
 
Description Hewlett Packard 
Organisation Hewlett Packard Ltd
Country United Kingdom 
Sector Private 
PI Contribution Collaboration on TPM specification
Collaborator Contribution Collaboration on TPM specification
Impact Contribution to TPM 2.0 specification and multiple research papers
Start Year 2006
 
Description L-3 TRL 
Organisation L3 TRL Technology
Country United Kingdom 
Sector Private 
PI Contribution Collaboration on Secure Cloud-based Collaboration Platform
Collaborator Contribution Collaboration on Secure Cloud-based Collaboration Platform
Impact Discussion and meetings Ongoing research partnership Solutions for key management and data processing in the cloud
Start Year 2014
 
Description Microsoft 
Organisation Microsoft Corporation
Country United States 
Sector Public 
PI Contribution Collaboration on TPM specification and access conrol
Collaborator Contribution Collaboration on TPM specification and access conrol
Impact PhD secondment and planned future collaborations
Start Year 2008
 
Description Open Rights Group 
Organisation Open Rights Group
Country United Kingdom 
Sector Charity/Non Profit 
PI Contribution Collaboration on privacy
Collaborator Contribution Collaboration on privacy
Impact Contribution to Royal Society Meeting on 9 June 2014
Start Year 2014
 
Title ConfiChair 
Description ConfiChair is a cloud-based collaboration tool that guarantees confidentiality from the cloud provider. See confiChair.org 
Type Of Technology Webtool/Application 
Year Produced 2011 
Impact Follow-up funding 
URL https://www.confichair.org/
 
Title StatVerif 
Description StatVerif is a software tool for analysing the security protocols of stateful protocols. It builds upon another well known tool called ProVerif 
Type Of Technology Software 
Year Produced 2011 
Impact Papers in journals and conferences 
 
Company Name CloudTomo 
Description The company aims to commercialise some security research. 
Year Established 2011 
Impact Has won two funding awards: Scottish Enterprise award (60K) and TSB award (80K, not taken up).
 
Description British Science Festival panel 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? Yes
Geographic Reach National
Primary Audience Public/other audiences
Results and Impact Discussion.

Awareness raising.
Year(s) Of Engagement Activity 2014
URL http://www.britishscienceassociation.org/british-science-festival/privacy-and-security-age-surveilla...
 
Description Dagstuhl perspectives workshop 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? Yes
Geographic Reach International
Primary Audience Other academic audiences (collaborators, peers etc.)
Results and Impact Wide-ranging presentations.

Manifesto document.
Year(s) Of Engagement Activity 2014
URL http://www.dagstuhl.de/en/programm/kalender/semhp/?semnr=14401
 
Description Google visit 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Much discussion.

Interaction.
Year(s) Of Engagement Activity 2012
 
Description Pint of Science Festival 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Public/other audiences
Results and Impact Mark Ryan, along with colleagues Tom Chothia and Flavio Garcia, gave talks as part of the Pint of Science Festival. This international series of events offers the general public to engage with experts in scientific fields by attending talks, asking questions and entering discussion, within the informal setting of a bar or pub. The academics presented the findings of research with real-world impact to individual privacy that increased awareness and interest in the subject area.
Year(s) Of Engagement Activity 2015
URL http://www.birmingham.ac.uk/university/colleges/eps/news/college/2015/04/Pint-of-Science-Festival-20...
 
Description Royal Society meeting 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Policymakers/politicians
Results and Impact It was a high-profile meeting at the Royal Society entitled Security and Privacy in Society. The event hosts a unique combination of people from both the surveillance community and the privacy community. I am very pleased to have a stellar list of invitees, including Sir David Omand and Sir Francis Richards, both former directors of GCHQ, Rt. Hon. James Arbuthnot MP (Chairman of the Defence Select Committee), Julian Huppert MP, and Helen Goodman MP, and the privacy proponents Caspar Bowden, Charles Raab, and Bart Preneel. Yet others include Jean Jaques Quisquater, the journalists Ewen MacAskill (Guardian) and Gordon Corera (BBC). There will also be some senior current people from GCHQ.

Support for further funding applications.
Year(s) Of Engagement Activity 2014
URL http://www.cs.bham.ac.uk/research/groupings/security_and_privacy/royalsoc2014/