Publications
See also: Google Scholar, DBLP
Journals
-
[CCK23]Symbolic protocol verification with dice: process equivalences in the presence of probabilities. Journal of Computer Security , 2023. PDF | Bibtex | AbstractSymbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied pi-calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need for randomized schedulers and exhibit a counter-example to a result in a previous work that relied on non-randomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. In particular, when considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has---maybe surprisingly---a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity.
-
[BCK20]On the semantics of communications when verifying equivalence properties. Journal of Computer Security , 2020. | AbstractSymbolic models for security protocol verification were pioneered by Dolev and Yao in their seminal work. Since then, although inspired by the same ideas, many variants of the original model were developed. In particular, a common assumption is that the attacker has complete control over the network and can therefore intercept any message. This assumption has been interpreted in slightly different ways depending on the particular models: either any protocol output is directly routed to the adversary, or communications may be among any two participants, including the attacker --- the scheduling between which exact parties the communication happens is left to the attacker. This difference may seem unimportant at first glance and, depending on the verification tools, either one or the other semantics is implemented. We show that, unsurprisingly, they indeed coincide for reachability properties. However, for indistinguishability properties, we prove that these two interpretations lead to incomparable semantics. We also introduce and study a new semantics, where internal communications are allowed but messages are always eavesdropped by the attacker. This new semantics yields strictly stronger equivalence relations. Moreover, we identify two subclasses of protocols for which the three semantics coincide. Finally, we implemented verification of trace equivalence for each of the three semantics in the DeepSec tool and compare their performances on several classical examples.
-
[CCD17]A procedure for deciding symbolic equivalence between sets of constraint systems. Information and Computation , 2017. PDF | PDF (Long version) | Bibtex | AbstractWe consider security properties of cryptographic protocols that can be modelled using trace equivalence, a crucial notion when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability. Infinite sets of possible traces are symbolically represented using deducibility constraints. We describe an algorithm that decides trace equivalence for protocols that use standard primitives and that can be represented using such constraints. More precisely, we consider symbolic equivalence between sets of constraint systems, and we also consider disequations. Considering sets and disequations is actually crucial to decide trace equivalence for processes that may involve else branches and/or private channels (for a bounded number of sessions). Our algorithm for deciding symbolic equivalence between sets of constraint systems is implemented and performs well in practice. Unfortunately, it does not scale up well for deciding trace equivalence between processes. This is however the first implemented algorithm deciding trace equivalence on such a large class of processes.
-
[CCCK16]Automated verification of equivalence properties of cryptographic protocols. ACM Transactions on Computational Logic , 2016. Listed in ACM Computing Reviews' 21st Annual Best of Computing list of notable books and articles for 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
-
[CR23]Indistinguishability Beyond Diff-Equivalence in ProVerif. In Proceedings of the 36th IEEE Computer Security Foundations Symposium (CSF'23), IEEE Computer Society Press, 2023. Distinguished paper award. PDF | PDF (long version) | Bibtex | AbstractWhen formalising cryptographic protocols, privacy-type properties such as strong flavours of secrecy, anonymity or unlinkability, are often modelled by indistinguishability statements. Proving them is notoriously more challenging than trace properties which benefit from a well-established tool support today. State-of-the-art techniques often exhibit significant limitations, e.g., consider only a bounded number of protocol sessions, or prove diff-equivalence---a fine-grained, structure-guided notion of indistinguishability that commonly yields unnecessarily pessimistic analyses.
In this paper, we design, implement and evaluate the first general framework for proving indistinguishability properties, for an unbounded number of protocol sessions, going beyond the scope of diff-equivalence. For that we relax the structural requirements of ProVerif, a state-of-the-art tool, through a notion of session decomposition, intuitively allowing a dynamic restructuration of the proofs. We can then verify in a modular way various, more realistic models of indistinguishability such as may-testing equivalence, by exhibiting for each relation a sufficient condition on ProVerif's output ensuring that it holds. We implement our approach into a prototype and showcase the gain in scope through several case studies. -
[CCD23]Election Verifiability with ProVerif. In Proceedings of the 36th IEEE Computer Security Foundations Symposium (CSF'23), IEEE Computer Society Press, 2023. PDF | Bibtex | AbstractElectronic voting systems should guarantee (at least) vote privacy and verifiability. Formally proving these two properties is challenging. Indeed, vote privacy is typically expressed as an equivalence property, hard to analyze for automatic tools, while verifiability requires to count the number of votes, to guarantee that all honest votes are properly tallied.
We provide a full characterization of E2E-verifiability in terms of two simple properties, that are shown to be both sufficient and necessary. In contrast, previous approaches proposed sufficient conditions only. These two properties can easily be expressed in a formal tool like ProVerif but remain hard to prove automatically. Therefore, we provide a generic election framework, together with a library of lemmas, for the (automatic) proof of E2E-verifiability. We successfully apply our framework to several protocols of the literature that include two complex, industrial-scale voting protocols, namely Swiss Post and CHVote, designed for the Swiss context. -
[CMR23]Automatic verification of transparency protocols. In Proceedings of the 8th IEEE European Symposium on Security and Privacy (EuroS&P 23), IEEE, 2023. Bibtex | PDF | PDF (long) | AbstractWe introduce new features in ProVerif, an automatic tool for verifying security protocols, and a methodology for using them. This methodology and these features are aimed at protocols which involve sophisticated data types that have strong properties, such as Merkle trees, which allow compact proofs of data presence and tree extension. Such data types are widely used in protocols in systems that use distributed ledgers and/or blockchains.
With our methodology, it is possible to describe the data type quite abstractly, using ProVerif axioms, and prove the correctness of the protocol using those axioms as assumptions. Then, in separate steps, one can define one or more concrete implementations of the data type, and again use ProVerif to show that the implementations satisfy the assumptions that were coded as axioms. This helps make compositional proofs, splitting the proof burden into several manageable pieces.
To enable this methodology, we introduce new capabilities in ProVerif, by extending the class of lemmas and axioms that it can reason with. Specifically, we allow user-defined predicates, attacker predicates and message predicates to appear in lemmas and axioms, and define their semantics. We show the soundness of the implementation of this idea with respect to the semantics.
We illustrate the methodology and features by providing the first formal verification of two transparency protocols which precisely models the Merkle tree data structure. The two protocols are transparent decryption (sometimes called accountable decryption), and certificate transparency. Transparent decryption is a way of ensuring that decryption operations are visible by people who are affected by them. This can be used, for example, to support privacy: it can mean that a subject is alerted to the fact that information about them has been decrypted. Certificate transparency is an Internet security standard for monitoring and auditing the issuance of digital certificates. -
[CCDH23]Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses. In Proceedings of the 32th USENIX Security Symposium, USENIX Security 2023 (USENIX'23), USENIX Association, 2023. Bibtex | AbstractMost cryptographic protocols use cryptographic hash functions as a building block. The security analyses of these pro- tocols typically assume that the hash functions are perfect (such as in the random oracle model). However, in practice, most widely deployed hash functions are far from perfect – and as a result, the analysis may miss attacks that exploit the gap between the model and the actual hash function used. We develop the first methodology to systematically dis- cover attacks on security protocols that exploit weaknesses in widely deployed hash functions. We achieve this by revisit- ing the gap between theoretical properties of hash functions and the weaknesses of real-world hash functions, from which we develop a lattice of threat models. For all of these threat models, we develop fine-grained symbolic models.
Our methodology’s fine-grained models cannot be directly encoded in existing state-of-the-art analysis tools by just using their equational reasoning. We therefore develop extensions for the two leading tools, TAMARIN and PROVERIF. In extensive case studies using our methodology, the extended tools rediscover all attacks that were previously reported for these protocols and discover several new variants. -
[BCW22]A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello. In Proceedings of the 29th ACM Conference on Computer and Communications Security (CCS'22), ACM Press, 2022. PDF | Bibtex | AbstractTLS 1.3, the newest version of the Transport Layer Security (TLS) protocol, provides strong authentication and confidentiality guarantees that have been comprehensively analyzed in a variety of formal models. However, despite its controversial use of handshake meta-data encryption, the privacy guarantees of TLS 1.3 remain weak and poorly understood. For example, the protocol reveals the identity of the target server to network attackers, allowing the passive surveillance and active censorship of TLS connections. To close this gap, the IETF TLS working group is standardizing a new privacy extension called Encrypted Client Hello (ECH, previously called ESNI), but the absence of a formal privacy model makes it hard to verify that this extension works. Indeed, several early drafts of ECH were found to be vulnerable to active network attacks.
In this paper, we present the first mechanized formal analysis of privacy properties for the TLS 1.3 handshake. We study all standard modes of TLS 1.3, with and without ECH, using the symbolic protocol analyzer ProVerif. We discuss attacks on ECH, some found during the course of this study, and show how they are accounted for in the latest version. Our analysis has helped guide the standardization process for ECH and we provide concrete privacy recommendations for TLS implementors. We also contribute the most comprehensive model of TLS 1.3 to date, which can be used by designers experimenting with new extensions to the protocol. Ours is one of the largest privacy proofs attempted using an automated verification tool and may be of general interest to protocol analysts. -
[CJKK22]Sapic+: protocol verifiers of the world, unite!. In Proceedings of the 31th USENIX Security Symposium, USENIX Security 2022 (USENIX'22), USENIX Association, 2022. PDF | PDF (long version) | Bibtex | AbstractSymbolic security protocol verifiers have reached a high degree of automation and ma- turity. Today, experts can model real-world protocols, but this often requires model-specific encodings and deep insight into the strengths and weaknesses of each of those tools. With Sapic+, we introduce a protocol verification platform that lifts this burden and permits choosing the right tool for the job, at any development stage. We build on the existing compiler from Sapic to Tamarin, and extend it with automated translations from Sapic+ to ProVerif and DeepSec, as well as powerful, protocol-independent optimizations of the existing translation. We prove each part of these translations sound. A user can thus, with a single Sapic+ file, verify reachability and equivalence properties on the specified protocol, either using ProVerif, Tamarin or DeepSec. Moreover, the soundness of the translation allows to directly assume results proven by another tool which allows to exploit the respective strengths of each tool. We demonstrate our approach by analyzing various existing models. This includes a large case study of the 5G authentication protocols, previously analyzed in Tamarin. Encoding this model in Sapic+ we demonstrate the effectiveness of our approach. Moreover, we study four new case studies: the LAKE and the Privacy-Pass protocols, both under standardization, the SSH protocol with the agent-forwarding feature, and the recent KEMTLS [45] protocol, a post-quantum version of the main TLS key exchange.
-
[CCK22]Symbolic protocol verification with dice: process equivalences in the presence of probabilities. In Proceedings of the 35th IEEE Computer Security Foundations Symposium (CSF'22), IEEE Computer Society Press, 2022. PDF | PDF (long version) | Bibtex | AbstractSymbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied pi calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need for randomized schedulers and exhibit a counter-example to a result in a previous work that relied on non-randomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. In particular, when considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has---maybe surprisingly---a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity.
-
[BCC22]ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. In Proceedings of the 43th IEEE Symposium on Security and Privacy (S&P'22), IEEE Computer Society Press, 2022. PDF | PDF (long version) | Source & Benchmark | Bibtex | AbstractThis paper presents a major overhaul of one the most widely used symbolic security protocol verifiers, ProVerif. We provide two main contributions. First, we extend ProVerif with lemmas, axioms, proofs by induction, natural numbers, and temporal queries. These features not only extend the scope of ProVerif, but can also be used to improve its precision (that is, avoid false attacks) and make it terminate more often. Second, we rework and optimize many of the algorithms used in ProVerif (generation of clauses, resolution, subsumption, ...), resulting in impressive speed-ups on large examples.
-
[CKR20]The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols. In Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday, Lecture Notes in Computer Science 12300, Springer, 2020. PDF | PDF (long version) | Bibtex | AbstractPrivacy-preserving security properties in cryptographic protocols are typically modelled by observational equivalences in process calculi such as the applied pi-calulus. We survey decidability and complexity results for the automated verification of such equivalences, casting existing results in a common framework which allows for a precise comparison. This unified view, beyond providing a clearer insight on the current state of the art, allowed us to identify some variations in the statements of the decision problems --- sometimes resulting in different complexity results. Additionally, we prove a couple of novel or strengthened results.
-
[CKR19]Exploiting Symmetries When Proving Equivalence Properties for Security Protocols. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS'19), ACM, 2019. PDF | Bibtex | AbstractVerification of privacy-type properties for cryptographic protocols in an active adversarial environment, modelled as a behavioural equivalence in concurrent-process calculi, exhibits a high computational complexity. While undecidable in general, for some classes of common cryptographic primitives the problem is coNEXP-complete when the number of honest participants is bounded.
In this paper we develop optimisation techniques for verifying equivalences, exploiting symmetries between the two processes under study. We demonstrate that they provide a significant (several orders of magnitude) speed-up in practice, thus increasing the size of the protocols that can be analysed fully automatically. -
[CCT18]A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. In Proceedings of the 31th IEEE Computer Security Foundations Symposium (CSF'18), IEEE Computer Society Press, 2018, Accepted for publication. PDF | PDF (long version) | Bibtex | AbstractProVerif is a popular tool for the fully automatic analysis of security protocols, offering very good support to detect flaws or prove security. One exception is the case of protocols with global states such as counters, tables, or more generally, memory cells. ProVerif fails to analyse such protocols, due to its internal abstraction.
Our key idea is to devise a generic transformation of the security properties queried to ProVerif. We prove the soundness of our transformation and implement it into a front-end GSVerif. Our experiments show that our front-end (combined with ProVerif) outperforms the few existing tools, both in terms of efficiency and protocol coverage. We successfully apply our tool to a dozen of protocols of the literature, yielding the first fully automatic proof of a security API and a payment protocol of the literature. -
[CKR18b]The DEEPSEC prover. In Proceedings of the 31th International Conference on Computer Aided Verification (CAV'18), Springer, 2018. PDF | Bibtex | AbstractIn this paper we describe the DeepSec prover, a tool for security-protocol analysis deciding equivalence properties, modelled as trace equivalence of two processes in a dialect of the applied pi calculus.
-
[CKR18]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. Distinguished paper award. PDF | PDF (long version) | Bibtex | AbstractAutomated verification has become an essential part in the security evaluation of cryptographic protocols. Recently, there has been a considerable effort to lift the theory and tool support that existed for reachability properties to the more complex case of equivalence properties. In this paper we contribute both to the theory and practice of this ver- ification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives—those that can be represented by a subterm convergent destructor rewrite system. We implemented the procedure in a new tool, DEEPSEC. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.
-
[CCW17]Secure composition of PKIs with public key protocols. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), IEEE Computer Society Press, 2017. PDF | PDF (long version) | Bibtex | AbstractWe use symbolic formal models to study the composition of public key-based protocols with public key infrastructures (PKIs). We put forth a minimal set of requirements which a PKI should satisfy and then identify several reasons why composition may fail. Our main results are positive and offer various trade-offs which align the guarantees provided by the PKI with those required by the analysis of protocol with which they are composed. We consider both the case of ideally distributed keys but also the case of more realistic PKIs. Our theorems are broadly applicable. Protocols are not limited to specific primitives and compositionality asks only for minimal requirements on shared ones. Secure composition holds with respect to arbitrary trace properties that can be specified within a reasonably powerful logic. For instance, secrecy and various forms of authentication can be expressed in this logic. Finally, our results alleviate the common yet demanding assumption that protocols are fully tagged. Keywords: secure composition, PKI, protocol analysis.
-
[BCK17]On Communication Models When Verifying Equivalence Properties. In Proceedings of the 6nd International Conference on Principles of Security and Trust (POST'17), Springer Berlin Heidelberg, 2017. PDF | PDF (long version) | Bibtex | AbstractSymbolic models for security protocol verification, following the seminal ideas of Dolev and Yao, come in many flavors, even though they share the same ideas. A common assumption is that the attacker has complete control over the network: he can therefore intercept any message. Depending on the precise model this may be reflected either by the fact that any protocol output is directly routed to the adversary, or communications may be among any two participants, including the attacker --- the scheduling between which exact parties the communication happens is left to the attacker. These two models may seem equivalent at first glance and, depending on the verification tools, either one or the other semantics is implemented. We show that, unsurprisingly, they indeed coincide for reachability properties. However, when we consider indistinguishability properties, we prove that these two semantics are incomparable. We also introduce a new semantics, where internal communications are allowed but messages are always eavesdropped by the attacker. We show that this new semantics yields strictly stronger equivalence relations. We also identify two subclasses of protocols for which the three semantics coincide. Finally, we implemented verification of trace equivalence for each of these semantics in the \apte tool and compare their performances on several classical examples.
-
[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), 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 in Security Protocols: Symbolic Framework and Proof Techniques. In Proceedings of the 4nd International Conference on Principles of Security and Trust (POST'15), 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), 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), 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), 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), 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), 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), 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), 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), 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