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.
People |
ORCID iD |
| Mark Ryan (Principal Investigator) |
Publications
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
Aybek Mukhamedov
(2007)
Anonymity Protocol with Identity Escrow, and Analysis in the Applied Pi-Calculus
Chevalier C
(2013)
Composition of password-based protocols
in Formal Methods in System Design
Bertucci F
(2023)
Effects of COVID-19 lockdown on the observed density of coral reef fish along coastal habitats of Moorea, French Polynesia.
in Regional environmental change
Mukhamedov A
(2008)
Fair multi-party contract signing using private contract signatures
in Information and Computation
Mukhamedov A
(2010)
Identity Escrow Protocol and Anonymity Analysis in the Applied Pi-Calculus
in ACM Transactions on Information and System Security
Mukhamedov A
(2010)
Identity Escrow Protocol and Anonymity Analysis in the Applied Pi-Calculus
in ACM Transactions on Information and System Security
Jia Liu
(2007)
Symbolic Bisimulation for the Applied Pi-Calculus
| 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 |