• School of Computer Science
  Personal Web Page
• Home
• Publications
• Talks
• Tools

Journals

• [CCD13]
  V. Cheval, V. Cortier and S. Delaune. Deciding equivalence-based properties using constraint solving. Theoretical Computer Science , 2013. PDF | Bibtex | Abstract

  Formal methods have proved their usefulness for analyzing the security of protocols. Most existing results focus on trace properties like secrecy or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require a notion of behavioural equivalence. Typical examples are anonymity, privacy related properties or statements closer to security properties used in cryptography.
       In this paper, we consider three notions of equivalence defined in the applied pi calculus: observational equivalence, may-testing equivalence, and trace equivalence. First, we study the relationship between these three notions. We show that for determinate processes, observational equivalence actually coincides with trace equivalence, a notion simpler to reason with. We exhibit a large class of determinate processes, called simple processes, that capture most existing protocols and cryptographic primitives. While trace equivalence and may-testing equivalence seem very similar, we show that may-testing equivalence is actually strictly stronger than trace equivalence. We prove that the two notions coincide for image-finite processes, such as processes without replication.
       Second, we reduce the decidability of trace equivalence (for finite processes) to deciding symbolic equivalence between sets of constraint systems. For simple processes without replication and with trivial else branches, it turns out that it is actually sufficient to decide symbolic equivalence between pairs of positive constraint systems. Thanks to this reduction and relying on a result first proved by M. Baudet, this yields the first decidability result of observational equivalence for a general class of equational theories (for processes without else branch nor replication). Moreover, based on another decidability result for deciding equivalence between sets of constraint systems, we get decidability of trace equivalence for processes with else branch for standard primitives.

Conferences

• [CCP13]
  V. Cheval, V. Cortier and A. Plet. Lengths may break privacy -- or how to check for equivalences with length. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV'13), pages 0-0 Springer, 2013. PDF | PDF (long version) | Bibtex | Abstract

  This paper presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. ProVerif can prove observational equivalence between processes that have the same structure but differ by the messages they contain. In order to extend the class of equivalences that ProVerif handles, we extend the language of terms by defining more functions (destructors) by rewrite rules. In particular, we allow rewrite rules with inequalities as side-conditions, so that we can express tests “if then else” inside terms. Finally, we provide an automatic procedure that translates a process into an equivalent process that performs as many actions as possible in- side terms, to allow ProVerif to prove the desired equivalence. These extensions have been implemented in ProVerif and allow us to au- tomatically prove anonymity in the private authentication protocol by Abadi and Fournet.
• [CB13]
  V. Cheval and B. Blanchet. Proving More Observational Equivalences with ProVerif. In Proceedings of the 2nd International Conference on Principles of Security and Trust (POST'13), pages 226-246 Springer, 2013. PDF | PDF (long version) | Bibtex | Abstract

  This paper presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. ProVerif can prove observational equivalence between processes that have the same structure but differ by the messages they contain. In order to extend the class of equivalences that ProVerif handles, we extend the language of terms by defining more functions (destructors) by rewrite rules. In particular, we allow rewrite rules with inequalities as side-conditions, so that we can express tests “if then else” inside terms. Finally, we provide an automatic procedure that translates a process into an equivalent process that performs as many actions as possible in- side terms, to allow ProVerif to prove the desired equivalence. These extensions have been implemented in ProVerif and allow us to au- tomatically prove anonymity in the private authentication protocol by Abadi and Fournet.
• [ACD12]
  M. Arapinis, V. Cheval and S. Delaune. Verifying privacy-type properties in a modular way. In Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF'12), pages 95-109 IEEE Computer Society Press, 2012. PDF | PDF (long version) | Bibtex | Abstract

  Formal methods have proved their usefulness for analysing the security of protocols. In this setting, privacy-type security properties (e.g. vote-privacy, anonymity, unlinkability) that play an important role in many modern applications are formalised using a notion of equivalence.
       In this paper, we study the notion of trace equivalence and we show how to establish such an equivalence relation in a modular way. It is well-known that composition works well when the processes do not share secrets. However, there is no result allowing us to compose processes that rely on some shared secrets such as long term keys. We show that composition works even when the processes share secrets provided that they satisfy some reasonable conditions. Our composition result allows us to prove various equivalence-based properties in a modular way, and works in a quite general setting. In particular, we consider arbitrary cryptographic primitives and processes that use non-trivial else branches.
       As an example, we consider the ICAO e-passport standard, and we show how the privacy guarantees of the whole application can be derived from the privacy guarantees of its sub-protocols.
• [CCD11]
  V. Cheval, H. Comon-Lundh and S. Delaune. Trace Equivalence Decision: Negative Tests and Non-determinism. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS'11), pages 321-330 ACM Press, 2011. PDF | Bibtex | Abstract

  We consider security properties of cryptographic protocols that can be modeled using the notion of trace equivalence. The notion of equivalence is crucial when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability.
       In this paper, we give a calculus that is close to the applied pi calculus and that allows one to capture most existing protocols that rely on classical cryptographic primitives. First, we propose a symbolic semantics for our calculus relying on constraint systems to represent infinite sets of possible traces, and we reduce the decidability of trace equivalence to deciding a notion of symbolic equivalence between sets of constraint systems. Second, we develop an algorithm allowing us to decide whether two sets of constraint systems are in symbolic equivalence or not. Altogether, this yields the first decidability result of trace equivalence for a general class of processes that may involve else branches and/or private channels (for a bounded number of sessions).
• [CCD10]
  V. Cheval, H. Comon-Lundh and S. Delaune. Automating security analysis: symbolic equivalence of constraint systems. In Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR'10), pages 412-426 Springer-Verlag, 2010. PDF | Bibtex | Abstract

  We consider security properties of cryptographic protocols, that are either trace properties (such as confidentiality or authenticity) or equivalence properties (such as anonymity or strong secrecy). Infinite sets of possible traces are symbolically represented using deducibility constraints. We give a new algorithm that decides the trace equivalence for the traces that are represented using such constraints, in the case of signatures, symmetric and asymmetric encryptions. Our algorithm is implemented and performs well on typical benchmarks. This is the first implemented algorithm, deciding symbolic trace equivalence.

Theses

• [Che12]
  V. Cheval. Automatic verification of cryptographic protocols: privacy-type properties. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2012. PDF | Bibtex | Abstract

  Many tools have been developed to automatically verify security properties on cryptographic protocols. But until recently, most tools focused on trace properties (or reachability properties) such as authentication and secrecy. However, many security properties cannot be expressed as trace properties, but can be written as equivalence properties. Privacy, unlinkability, and strong secrecy are typical examples of equivalence properties.
       Intuitively, two protocols P, Q are equivalent if an adversary can not distinguish P from Q by interacting with these processes. In the literature, several notions of equivalence were studied, e.g. trace equivalence or a stronger one, observational equivalence. However, it is often very difficult to prove by hand any of these equivalences, hence the need for efficient and automatic tools.
       We first worked on a approach that rely on constraint solving techniques and that is well suited for bounded number of sessions. We provided a new algorithm for deciding the trace equivalence between processes that may contain negative tests and non-determinism. We applied our results on concrete examples such as anonymity of the Private Authentication protocol and the E-passport protocol.
       We also investigated composition results. More precisely, we focused on parallel composition under shared secrets. We showed that under certain conditions on the protocols, the privacy type properties is preserved under parallel composition under shared secrets. We applied our result on the e-passport protocol.
       At last this work presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. This extension have been implemented in ProVerif and allow us to automatically prove anonymity in the private authentication protocol

Other Publications

• [CCD12]
  V. Cheval, V. Cortier and S. Delaune. Deciding equivalence-based properties using constraint solving. Research report, Laboratoire Spécification et Vérification, ENS Cachan, France, August 2012. PDF | Bibtex | Abstract

  Formal methods have proved their usefulness for analyzing the security of protocols. Most existing results focus on trace properties like secrecy or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require a notion of behavioural equivalence. Typical examples are anonymity, privacy related properties or statements closer to security properties used in cryptography.
       In this paper, we consider three notions of equivalence defined in the applied pi calculus: observational equivalence, may-testing equivalence, and trace equivalence. First, we study the relationship between these three notions. We show that for determinate processes, observational equivalence actually coincides with trace equivalence, a notion simpler to reason with. We exhibit a large class of determinate processes, called simple processes, that capture most existing protocols and cryptographic primitives. While trace equivalence and may-testing equivalence seem very similar, we show that may-testing equivalence is actually strictly stronger than trace equivalence. We prove that the two notions coincide for image-finite processes, such as processes without replication.
       Second, we reduce the decidability of trace equivalence (for finite processes) to deciding symbolic equivalence between sets of constraint systems. For simple processes without replication and with trivial else branches, it turns out that it is actually sufficient to decide symbolic equivalence between pairs of positive constraint systems. Thanks to this reduction and relying on a result first proved by M. Baudet, this yields the first decidability result of observational equivalence for a general class of equational theories (for processes without else branch nor replication). Moreover, based on another decidability result for deciding equivalence between sets of constraint systems, we get decidability of trace equivalence for processes with else branch for standard primitives.
• [CCD09]
  V. Cheval, H. Comon-Lundh and S. Delaune. A decision procedure for proving observational equivalence. October 2009. PDF | Bibtex | Abstract

  We consider security properties of cryptographic protocols, that are either trace properties (such as confidentiality or authenticity) or equivalence properties (such as anonymity or strong secrecy). Infinite sets of possible traces are symbolically represented using deducibility constraints. We give a new algorithm that decides the trace equivalence for the traces that are represented using such constraints, in the case of signatures, symmetric and asymmetric encryptions. Our algorithm is implemented and performs well on typical benchmarks. This is the first implemented algorithm, deciding symbolic trace equivalence.
• [Che09]
  V. Cheval. Algorithme de décision de l'équivalence symbolique de systèmes de contraintes. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2009. PDF | Bibtex