Strategy Logics for the Verification of Security Protocols

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.