| EPSRC Reference: |
EP/V009214/1 |
| Title: |
Strategy Logics for the Verification of Security Protocols |
| Principal Investigator: |
Belardinelli, Dr F |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computing |
| Organisation: |
Imperial College London |
| Scheme: |
Overseas Travel Grants (OTGS) |
| Starts: |
01 August 2021 |
Ends: |
31 July 2022 |
Value (£): |
8,996
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
The verification of security and voting protocols is a subject of ever increasing importance in today's networked world. The UK-based Open Rights Group has argued that a lack of testing, inadequate audit procedures, and insufficient attention given to system or process design with electronic voting leaves "elections open to error and fraud". Hence, the growing adoption of electronic voting systems requires these systems to be certified against possible malicious behaviours, including collusion and coercion from third parties.
To this end, formal methods can provide mathematically precise techniques and tools for the certification of voting protocols. Indeed, formal methods have already shown their value, for instance, in the discovery
of several attacks, including a man-in-the-middle attack on the Needham-Schroeder protocol, one of the most widely-used public-key authentication protocols, that went unnoticed for 17 years.
In this project we aim at developing techniques for the formal verification of security properties of (electronic) voting protocols based on expressive logic-based specification languages. Specifically, the project proposal aims at capturing cryptographic aspects pertaining to security, which are not readily expressible by symbolic reasoning, by extending popular logics for multi-agent systems with equational theories to represent encoding and decoding of messages. We intend to apply the resulting framework to the verification of properties such as coercion-resistance, receipt-freeness, and anonymity to a wide range of voting protocols (e.g., ThreeBallot, Selene, FOO), thus laying the foundation for their formal certification.
|
|
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.imperial.ac.uk |