Verifying anonymity and privacy properties of security protocols

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

Abstract

The project investigates systems designed to offer privacy guarantees to on-line users, such as anonymity of payment, privacy of shopping preference, of email patterns and associations between correspondents, or candidate choice in an election. It aims to develop a taxonomy of anonymity and privacy properties within two verification formalisms (strand spaces and applied pi calculus) and to develop techniques for analysing protocols that are designed to provide such properties. We shall also analyse some well-known protocols, such as private authentication protocols and direct anonymous attestation protocol. This proposal builds on the acknowledged expertise of the University of Birmingham in the area of formal methods and verification.

Publications

10 25 50

publication icon
Aybek Mukhamedov (2007) Anonymity Protocol with Identity Escrow and Analysis in the Applied pi-calculus in Anonymity Protocol with Identity Escrow and Analysis in the Applied pi-calculus

publication icon
Aybek Mukhamedov (2007) Improved Multi-party Contract Signing in Financial Crytopgrahy 2007

publication icon
Aybek Mukhamedov (Co-Author) (2010) Anonymity Protocol with Identity Escrow and Analysis in the Applied Pi-Calculus in ACM Transactions on Information and System Security (TISSEC)

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

publication icon
Delaune S (2008) Trust Management II

 
Description Formal characterisation of anonymity properties for several kinds of service-usage protocols.

Development of service-usage protocol with escrowed identity, to support a balance of privacy and accountability.

Analysis of said protocol in terms of said characterisation.

Symbolic methods for automated analysis of equivalence properties.

Development and analysis of multi-party contract-signing protocols.
Exploitation Route Can be used to inform developers of web services about how to provide privacy-supporting authentication. Such developers can include large corporations (such as Google and Microsoft) as well as small organisations that make web services.

Can be used to inform academic researchers also working on privacy, accountability and authentication.
Sectors Creative Economy,Digital/Communication/Information Technologies (including Software),Financial Services, and Management Consultancy,Government, Democracy and Justice,Security and Diplomacy,Other

 
Description Contribution Method: Concrete contribution and proposal to international debate about how individual privacy can be balanced with accountability. Beneficiaries: Computer scientists, libertarians, civil rights organisations.
Sector Digital/Communication/Information Technologies (including Software),Government, Democracy and Justice,Security and Diplomacy,Other
Impact Types Societal,Economic

 
Description Formal Protocol Verification Applied 
Form Of Engagement Activity Scientific meeting (conference/symposium etc.)
Part Of Official Scheme? Yes
Type Of Presentation workshop facilitator
Geographic Reach International
Primary Audience Health professionals
Results and Impact Co-Chair of Formal Protocol Verification Applied, Dagstul, 14 - 19 October 2007

Seminar proceedings
Year(s) Of Engagement Activity 2007