Security properties, process equivalences and automated verification – Sequoia

The rise of the Internet and the ubiquity of electronic devices have changed our way of life. Many previously face-to-face and paper transactions nowadays have digital counterparts: home banking, electronic commerce, e-voting, etc. This digitalization of the world comes with tremendous risks for our security and privacy. In order to protect electronic transactions security protocols are deployed. These are concurrent programs that make use of cryptographic primitives, such as encryption or digital signatures, to ensure the security of data, e.g. guarantee the confidentiality of a credit card number or authentication credentials. However, design errors in such protocols can be exploited, and given the very nature of the services provided this may have important socio-economic consequences: legally binding political elections using Internet voting, have recently been deployed in several European countries (Estonia, France, Norway and Switzerland); in France 37,7 billion euros have been spent through e-commerce in 2011; and bank fraudsters are aiming to steal ever-higher amounts (with single transfers over 50,000 euros) using fully automated attack tools.

These examples demonstrate how essential it is to have solid foundations to carefully analyse and design modern security protocols. One extremely successful approach has been symbolic security protocol analysis, based on techniques from model-checking, automated reasoning and concurrency theory. For example, while designing a formal model of Google's Single Sign-On protocol - that allows a user to identify himself only once and then access various applications (such as Gmail or Google calendar) - Armando et al. discovered that a dishonest service provider could actually impersonate any of its users at another service provider. Many automated tools - e.g. ProVerif, AVISPA, Scyther, FDR/CASPER or MaudeNPA - exist for formally verifying authentication and confidentiality properties. However, the growing complexity of Internet services and the ubiquity of connected electronic devices change both the goals of security protocols, i.e. what security properties they need to achieve, and the means they employ for achieving them. Recent work on privacy preserving properties has shown that they are naturally captured as indistinguishability properties. Indistinguishability is a powerful notion that enables the analysis of a wide range of security properties. It expresses the fact that an adversary is unable to distinguish between two situations, and can be naturally modelled as equivalences in process calculi that support the modeling of cryptographic primitives.

However, most protocol analysis tools are restricted to analyzing reachability properties, such as authentication and weak forms of confidentiality, while most security properties (in particular privacy preserving properties, such as anonymity and untraceability) need to be expressed in terms of some process equivalence. The increasing use of observational equivalence as a modeling tool shows the need for new tools and techniques that are able to analyze such equivalence properties. The aims of this project are

- to investigate which process equivalences-among the plethora of existing ones-are appropriate for a given security property, system assumptions and attacker capabilities;

- to advance the state-of-the-art of automated verification for process equivalences, allowing for instance support for more cryptographic primitives, relevant for case studies;

- to study protocols that use low-entropy secrets, which arise for instance in modern multi-factor authentication protocols. We believe that security properties relevant to the presence of such secrets can be naturally expressed using process equivalences;

- to apply these results to case studies from electronic voting. Recent proposals avoid to trust the client platform and make use of low-entropy secrets which are out of the scope of current analysis techniques.