Supervisor

Suitable for

Abstract

Security protocols aim at securing communications. They are used in various applications (e.g. establishment of secure channels over the Internet, secure messaging, electronic voting, mobile communications, etc.) Their design is known to be error prone and flaws are difficult to fix once a protocol is largely deployed. Hence a common practice is to analyze the security of a protocol using formal techniques and in particular automatic tools. This approach has lead to the development of several verification tools such as ProVerif (https://proverif.inria.fr), Tamarin (https://tamarin-prover.github.io) and DeepSec (https://deepsec-prover.github.io) that rely on symbolic models to express protocols and their security properties. Symbolic, automated verification has been a very successful approach for revealing vulnerabilities or proving the absence of entire families of attacks. For instance, these tools were used to verify the security of several major protocols (e.g. TLS 1.3, 5G protocols, Belenios electronic voting protocol).

Internally, these tools express cryptographic messages using terms. The algebraic properties of the cryptographic primitives are then expressed by mean of an equational theory on terms. For example, the equation dec(enc(x,y),y) = x expresses that deciphering (“dec”) with a key “y” a cipher of a message “x” by the same key “y”, i.e. “enc(x,y)”, allows to retrieve the message “x”. Equality of terms modulo the equational theory is one of the core problems that these tools must solve. Although unification algorithms for many primitives with complexes algebraic properties, such as finite variant, XOR with homomorphism, abelian groups, etc are known, these algorithms only work when the equations do not mix primitives, in other words when the equations are not distinct. We aim to develop new efficient unification algorithm for the union of non-distinct equational theories. Proofs of correctness would be first done by hand but an implementation in F* [1] would be of interest (or Coq [2]).

Objectives:

• get familiar with currently known algorithm for unification of union of distinct equational theories. [3]
• create a semi-decision algorithm for unification of general union of equational theories and establish its limitation. It will be based on a general framework that extend the work of [4]         
• implement the resulting algorithm and evaluate its efficiency         
• implement the correctness proof on F* or Coq

The implemented library will be incorporated in the tool ProVerif.

[1] https://www.fstar-lang.org

[2] https://coq.inria.fr/

[3] FRANZ BAADER, KLAUS U. SCHULZ, Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures, Journal of Symbolic Computation, Volume 21, Issue 2, 1996

[4] Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated Verification of Selected Equivalences for Security Protocols. Journal of Logic and Algebraic Programming, 75(1):3-51, February-March 2008.

Pre-requisites: Logic and Proof, Functional Programming