Publications
See also: Google Scholar, DBLP
Journals
-
[CCCK16]Automated verification of equivalence properties of cryptographic protocols. ACM Transactions on Computational Logic , 2016. PDF | Bibtex | AbstractIndistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance against offline guessing attacks. Indistinguishability properties can be conveniently modeled as equivalence properties. We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryptographic protocols. As in the applied pi-calculus, our protocol specification language is parametrized by a first-order sorted term signature and an equational theory which allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence which can therefore be automatically verified for such processes. When protocols are not determinate our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those whose equational theory is generated by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool A-KiSs (Active Knowledge in Security Protocols) and has been effectively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol due to Okamoto.
-
[YCR16]DTKI: A New Formalized PKI with Verifiable Trusted Parties. The Computer Journal , 2016. PDF | Bibtex | AbstractThe security of public key validation protocols for web-based applications has recently attracted attention because of weaknesses in the certificate authority model, and consequent attacks. Recent proposals using public logs have succeeded in making certificate management more transparent and verifiable. However, those proposals involve a fixed set of authorities. This means an oligopoly is created. Another problem with current log-based system is their heavy reliance on trusted parties that monitor the logs. We propose a distributed transparent key infrastructure (DTKI), which greatly reduces the oligopoly of service providers and allows verification of the behaviour of trusted parties. In addition, this paper formalises the public log data structure and provides a formal analysis of the security that DTKI guarantees.
-
[CCD13]Deciding equivalence-based properties using constraint solving. Theoretical Computer Science , 2013. PDF | Bibtex | AbstractFormal 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
-
[CCM15]Secure Refinements of Communication Channels. In Proceedings of the 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015), pages 575--589 Schloss Dagstuhl, 2015. PDF | PDF (long version) | Bibtex | AbstractIt is a common practice to design a protocol (say Q) assuming some secure channels. Then the secure channels are implemented using any standard protocol, e.g. TLS. In this paper, we study when such a practice is indeed secure.
We provide a characterization of both confidential and authenticated channels. As an application, we study several protocols of the literature including TLS and BAC protocols. Thanks to our result, we can consider a larger number of sessions when analyzing complex protocols resulting from explicit implementation of the secure channels of some more abstract protocol Q. -
[CC15]Timing attacks: symbolic framework and proof techniques. In Proceedings of the 4nd International Conference on Principles of Security and Trust (POST'15), pages To appear Springer Berlin Heidelberg, 2015. PDF | PDF (long version) | Bibtex | AbstractWe propose a framework for timing attacks, based on (a variant of) the applied-pi calculus. Since many privacy properties, as well as strong secrecy and game-based security properties, are stated as process equivalences, we focus on (time) trace equivalence. We show that actually, considering timing attacks does not add any complexity: time trace equivalence can be reduced to length trace equivalence, where the attacker no longer has access to execution times but can still compare the length of messages. We therefore deduce from a previous decidability result for length equivalence that time trace equivalence is decidable for bounded processes and the standard cryptographic primitives.
As an application, we study several protocols that aim for privacy. In particular, we (automatically) detect an existing timing attack against the biometric passport and new timing attacks against the Private Authentication protocol. -
[ACD15]Composing security protocols: from confidentiality to privacy. In Proceedings of the 4nd International Conference on Principles of Security and Trust (POST'15), pages To appear Springer Berlin Heidelberg, 2015. PDF | PDF (long version) | Bibtex | AbstractSecurity protocols are used in many of our daily-life applications, and our privacy largely depends on their design. Formal verification techniques have proved their usefulness to analyse these protocols, but they become so complex that modular techniques have to be developed. We propose several results to safely compose security protocols. We consider arbitrary primitives modeled using an equational theory, and a rich process algebra close to the applied pi calculus.
Relying on these composition results, we derive some security properties on a protocol from the security analysis performed on each of its subprotocols individually. We consider parallel composition and the case of key-exchange protocols. Our results apply to deal with confidentiality but also privacy-type properties (e.g. anonymity) expressed using a notion of equivalence. We illustrate the usefulness of our composition results on protocols from the 3G phone application and electronic passport. -
[CDR14]Tests for establishing security properties. In Proceedings of the 9th Symposium on Trustworthy Global Computing (TGC'14), pages 82-96 Springer Berlin Heidelberg, 2014. PDF | Bibtex | AbstractEnsuring strong security properties in some cases requires participants to carry out tests during the execution of a protocol. A classical example is electronic voting: participants are required to verify the presence of their ballots on a bulletin board, and to verify the computation of the election outcome. The notion of certificate transparency is another example, in which participants in the protocol are required to perform tests to verify the integrity of a certificate log.
We present a framework for modelling systems with such `testable properties', using the applied pi calculus. We model the tests that are made by participants in order to obtain the security properties. Underlying our work is an attacker model called "malicious but cautious", which lies in between the Dolev-Yao model and the "honest but curious" model. The malicious-but-cautious model is appropriate for cloud computing providers that are potentially malicious but are assumed to be cautious about launching attacks that might cause user tests to fail. -
[Che14]APTE: an Algorithm for Proving Trace Equivalence. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), pages 0-0 Springer, 2014. PDF | Bibtex | AbstractThis paper presents APTE, a new tool for automatically proving the security of cryptographic protocols. It focuses on proving trace equivalence between processes, which is crucial for specifying privacy type properties such as anonymity and unlinkability.
The tool can handle protocols expressed in a calculus similar to the applied-pi calculus, which allows us to capture most existing protocols that rely on classical cryptographic primitives. In particular, APTE handles private channels and else branches in protocols with bounded number of sessions. Unlike most equivalence verifier tools, APTE is guaranteed to terminate. Moreover, APTE is the only tool that extends the usual notion of trace equivalence by considering side-channel information leaked to the attacker such as the length of messages and the execution times. We illustrate APTE on different case studies which allowed us to automatically (re)-discover attacks on protocols such as the Private Authentication protocol or the protocols of the electronic passports. -
[CCP13]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 708-723 Springer, 2013. PDF | PDF (long version) | Bibtex | AbstractThis 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]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 | AbstractThis 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]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 | AbstractFormal 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]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 | AbstractWe 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]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 | AbstractWe 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]Automatic verification of cryptographic protocols: privacy-type properties. PhD Thesis, Laboratoire Specification et Verification, ENS Cachan, France, December 2012. PDF | Bibtex | AbstractMany 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
-
[CCD09]
-
[Che09]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