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).

The DeepSec prover specializes in the verification of security properties that can be expressed as behavioural equivalence, such as anonymity, vote privacy, unlinkability, strong secrecy, etc. It currently implements a procedure for checking “trace equivalence” between processes. The paper that describes the theory behind DeepSec also describe a theoretical procedure that allows to prove two stronger behavioural equivalences, that are similarity and bissimilarity. The description of these procedures is still considered “theoretical” as they are heavily non-deterministic, hence preventing efficient implementations. One part of this project thus aims to design an effective and efficient procedure for checking bissimilairty and similarity. Currently, symbolic models are purely non-deterministic. For instance, the random generation of numbers are intuitively abstracted and they are assumed to be impossible to guess by the attacker. While this is generally sensible, it is not always possible to eliminate probabilities altogether: some protocols specifically rely on probabilistic coin flips in their specification, and a recent paper [2] has shown that giving the attacker the ability to use probabilistic choices can enable him to break behavioural equivalence. This paper provides the general probabilistic model but only describe a procedure for checking probabilistic equivalence in a restrictive case, based on the internal procedure of DeepSec. This article provides the general probabilistic model, but only describes a procedure for checking probabilistic equivalence in a restrictive case, based on DeepSec's internal procedure. The second part of this project will aim to design a (potentially theoretical) procedure for verifying probabilistic equivalence in the general setting. Currently, symbolic models are purely non-deterministic. For instance, the random generation of numbers are intuitively abstracted and they are assumed to be impossible to guess by the attacker. While this is generally sensible, it is not always possible to eliminate probabilities altogether: some protocols specifically rely on probabilistic coin flips in their specification, and a recent paper [2] has shown that giving the attacker the ability to use probabilistic choices can enable him to break behavioural equivalence. This paper provides the general probabilistic model but only describe a procedure for checking probabilistic equivalence in a restrictive case, based on the internal procedure of DeepSec. This article provides the general probabilistic model, but only describes a procedure for checking probabilistic equivalence in a restrictive case, based on DeepSec's internal procedure. The second part of this project will aim to design a (potentially theoretical) procedure for verifying probabilistic equivalence in the general setting.

Objectives:         

• get familiar with the internal procedure of DeepSec [1]         
• design and implement an efficient algorithm for checking similarity/bissimilarity        
• design an algorithm for checking probabilistic equivalences in general setting       
• prove the correctness of all designed algorithms

The implemented library will be incorporated in the tool DeepSec.

[1] V. Cheval, S. Kremer and I. Rakotonirina. DEEPSEC: Deciding Equivalence Properties in Security Protocols - Theory and Practice. In Proceedings of the 39th IEEE Symposium on Security and Privacy (S&P'18), IEEE Computer Society Press, 2018.

[2] Symbolic protocol verification with dice. Vincent Cheval‚ Raphaëlle Crubillé and Steve Kremer. In J. Comput. Secur.. Vol. 31. No. 5. Pages 501–538. 2023.

Pre-requisites: Logic and Proof, Functional Programming, Probabilistic Model Checking