SEQUOIA - Security Properties, Process Equivalences, and Automated Verification

Description

Modern society is becoming ever-more digitalized. In particular, electronic services provided over the internet are now standard tools for individuals to network, manage their bank accounts, and even vote in important elections. It is therefore critical to deploy strongly secure systems to accomplish these tasks, which present the dual challenge of being both of socio-economic importance, and highly complex.

While cryptographic protocols are implemented to attempt securing these procedures, design errors remain abundant, as recent examples of practical attacks on such systems demonstrate. It is thus important to further refine the necessary tools to verify the correctness of these protocols. A highly successful technique to accomplish this is to use symbolic analysis. Two particularly important features of this technique stand out: 1) it is well-suited to analyze complex systems and 2) it is amenable to automation.

The aim of this project is to extend the capabilities of symbolic analysis so as to capture the subtle security properties of modern-day cryptographic protocols. Many of these properties can be expressed in terms of indistinguishabilty of processes, a notion that symbolic analysis currently lacks the necessary theoretical foundations to fully understand, and automated tools to verify. The technical objective is to begin filling this gap.

Examples of concrete security properties that indistinguishability naturally captures include anonymity, unlinkability, maximal protection of weak secrets such as passwords, and more. The main practical objective of the project is to provide an automated tool (using AKISS – Active Knowledge In Security protocolS - as a starting point) allowing the verification of indistinguishability, and therefore of the above-mentioned properties. We plan to illustrate our findings by performing an analysis on an e-voting protocol that actually relies on several of these properties.