A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
---
paper_title: A Computationally Complete Symbolic Attacker for Equivalence Properties

paper_content:

We consider the problem of computational indistinguishability of protocols. We design a symbolic model, amenable to automated deduction, such that a successful inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. We follow the idea we introduced earlier for reachability properties, axiomatizing what an attacker cannot violate. This results a computationally complete symbolic attacker, and ensures unconditional computational soundness for the symbolic analysis. We present a small library of computationally sound, modular axioms, and test our technique on an example protocol. Despite additional difficulties stemming from the equivalence properties, the models and the soundness proofs turn out to be simpler than they were for reachability properties.
---
paper_title: Probabilistic relational verification for cryptographic implementations

paper_content:

Relational program logics have been used for mechanizing formal proofs of various cryptographic constructions. With an eye towards scaling these successes towards end-to-end security proofs for implementations of distributed systems, we present RF*, a relational extension of F*, a general-purpose higher-order stateful programming language with a verification system based on refinement types. The distinguishing feature of F* is a relational Hoare logic for a higher-order, stateful, probabilistic language. Through careful language design, we adapt the F* typechecker to generate both classic and relational verification conditions, and to automatically discharge their proofs using an SMT solver. Thus, we are able to benefit from the existing features of F*, including its abstraction facilities for modular reasoning about program fragments. We evaluate RF* experimentally by programming a series of cryptographic constructions and protocols, and by verifying their security properties, ranging from information flow to unlinkability, integrity, and privacy. Moreover, we validate the design of RF* by formalizing in Coq a core probabilistic λ calculus and a relational refinement type system and proving the soundness of the latter against a denotational semantics of the probabilistic lambda λ calculus.
---
paper_title: A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems

paper_content:

Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers with respect to the more detailed computational models have been quite unclear. For more than 20 years the two approaches have coexisted but evolved mostly independently. Recently, significant research efforts attempt to develop paradigms for cryptographic systems analysis that combines the best of both worlds. There are two broad directions that have been followed. Computational soundness aims to establish sufficient conditions under which results obtained using symbolic models imply security under computational models. The direct approach aims to apply the principles and the techniques developed in the context of symbolic models directly to computational ones. In this paper we survey existing results along both of these directions. Our goal is to provide a rather complete summary that could act as a quick reference for researchers who want to contribute to the field, want to make use of existing results, or just want to get a better picture of what results already exist.
---
paper_title: Type-Based Verification of Electronic Voting Protocols

paper_content:

E-voting protocols aim at achieving a wide range of sophisticated security properties and, consequently, commonly employ advanced cryptographic primitives. This makes their design as well as rigorous analysis quite challenging. As a matter of fact, existing automated analysis techniques, which are mostly based on automated theorem provers, are inadequate to deal with commonly used cryptographic primitives, such as homomorphic encryption and mix-nets, as well as some fundamental security properties, such as verifiability. ::: ::: This work presents a novel approach based on refinement type systems for the automated analysis of e-voting protocols. Specifically, we design a generically applicable logical theory which, based on pre- and post-conditions for security-critical code, captures and guides the type-checker towards the verification of two fundamental properties of e-voting protocols, namely, vote privacy and verifiability. We further develop a code-based cryptographic abstraction of the cryptographic primitives commonly used in e-voting protocols, showing how to make the underlying algebraic properties accessible to automated verification through logical refinements. Finally, we demonstrate the effectiveness of our approach by developing the first automated analysis of Helios, a popular web-based e-voting protocol, using an off-the-shelf type-checker.
---
paper_title: Towards unconditional soundness: Computationally complete symbolic attacker

paper_content:

We consider the question of the adequacy of symbolic models versus computational models for the verification of security protocols. We neither try to include properties in the symbolic model that reflect the properties of the computational primitives nor add computational requirements that enforce the soundness of the symbolic model. We propose in this paper a different approach: everything is possible in the symbolic model, unless it contradicts a computational assumption. In this way, we obtain unconditional soundness almost by construction. And we do not need to assume the absence of dynamic corruption or the absence of key-cycles, which are examples of hypotheses that are always used in related works. We set the basic framework, for arbitrary cryptographic primitives and arbitrary protocols, however for trace security properties only.
---
paper_title: Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)

paper_content:

Two distinct, rigorous views of cryptography have developed over the years, in two mostly separate communities. One of the views relies on a simple but effective formal approach; the other, on a detailed computational model that considers issues of complexity and probability. There is an uncomfortable and interesting gap between these two approaches to cryptography. This paper starts to bridge the gap, by providing a computational justification for a formal treatment of encryption.
---
paper_title: On the security of public key protocols

paper_content:

Recently the use of public key encryption to provide secure network communication has received considerable attention. Such public key systems are usually effective against passive eavesdroppers, who merely tap the lines and try to decipher the message. It has been pointed out, however, that an improperly designed protocol could be vulnerable to an active saboteur, one who may impersonate another user or alter the message being transmitted. Several models are formulated in which the security of protocols can be discussed precisely. Algorithms and characterizations that can be used to determine protocol security in these models are given.
---
paper_title: A Computationally Sound Mechanized Prover for Security Protocols

paper_content:

We present a new mechanized prover for secrecy properties of security protocols. In contrast to most previous provers, our tool does not rely on the Dolev-Yao model, but on the computational model. It produces proofs presented as sequences of games; these games are formalized in a probabilistic polynomial-time process calculus. Our tool provides a generic method for specifying security properties of the cryptographic primitives, which can handle shared-key and public-key encryption, signatures, message authentication codes, and hash functions. Our tool produces proofs valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. We have implemented our tool and tested it on a number of examples of protocols from the literature.
---
paper_title: A method for obtaining digital signatures and public-key cryptosystems

paper_content:

An encryption method is presented with the novel property that publicly revealing an encryption key does not thereby reveal the corresponding decryption key. This has two important consequences: (1) Couriers or other secure means are not needed to transmit keys, since a message can be enciphered using an encryption key publicly revealed by the intented recipient. Only he can decipher the message, since only he knows the corresponding decryption key. (2) A message can be “signed” using a privately held decryption key. Anyone can verify this signature using the corresponding publicly revealed encryption key. Signatures cannot be forged, and a signer cannot later deny the validity of his signature. This has obvious applications in “electronic mail” and “electronic funds transfer” systems. A message is encrypted by representing it as a number M, raising M to a publicly specified power e, and then taking the remainder when the result is divided by the publicly specified product, n , of two large secret primer numbers p and q. Decryption is similar; only a different, secret, power d is used, where e * d ≡ 1(mod (p - 1) * (q - 1)). The security of the system rests in part on the difficulty of factoring the published divisor, n .
---
paper_title: New Directions in Cryptography

paper_content:

Two kinds of contemporary developments in cryptography are examined. Widening applications of teleprocessing have given rise to a need for new types of cryptographic systems, which minimize the need for secure key distribution channels and supply the equivalent of a written signature. This paper suggests ways to solve these currently open problems. It also discusses how the theories of communication and computation are beginning to provide the tools to solve cryptographic problems of long standing.
---
paper_title: Analysing Unlinkability and Anonymity Using the Applied Pi Calculus

paper_content:

An attacker that can identify messages as coming from the same source, can use this information to build up a picture of targets’ behaviour, and so, threaten their privacy. In response to this danger, unlinkable protocols aim to make it impossible for a third party to identify two runs of a protocol as coming from the same device. We present a framework for analysing unlinkability and anonymity in the applied pi calculus. We show that unlinkability and anonymity are complementary properties; one does not imply the other. Using our framework we show that the French RFID e-passport preserves anonymity but it is linkable therefore anyone carrying a French e-passport can be physically traced.
---
paper_title: Automatic proof of strong secrecy for security protocols

paper_content:

We present a new automatic technique for proving strong secrecy for security protocols. Strong secrecy means that an adversary cannot see any difference when the value of the secret changes. Our technique relies on an automatic translation of the protocol into Horn clauses, and a resolution algorithm on the clauses. It requires important extensions with respect to previous work for the proof of (standard) secrecy and authenticity. This technique can handle a wide range of cryptographic primitives, and yields proofs valid for an unbounded number of sessions and an unbounded message space; it is also flexible and efficient. We have proved its correctness, implemented it, and tested it on several examples of protocols including JFK by W. Aiello et al. (2002).
---
paper_title: Analysing Unlinkability and Anonymity Using the Applied Pi Calculus

paper_content:

An attacker that can identify messages as coming from the same source, can use this information to build up a picture of targets’ behaviour, and so, threaten their privacy. In response to this danger, unlinkable protocols aim to make it impossible for a third party to identify two runs of a protocol as coming from the same device. We present a framework for analysing unlinkability and anonymity in the applied pi calculus. We show that unlinkability and anonymity are complementary properties; one does not imply the other. Using our framework we show that the French RFID e-passport preserves anonymity but it is linkable therefore anyone carrying a French e-passport can be physically traced.
---
paper_title: Universally composable security: a new paradigm for cryptographic protocols

paper_content:

We propose a new paradigm for defining security of cryptographic protocols, called universally composable security. The salient property of universally composable definitions of security is that they guarantee security even when a secure protocol is composed with an arbitrary set of protocols, or more generally when the protocol is used as a component of an arbitrary system. This is an essential property for maintaining security of cryptographic protocols in complex and unpredictable environments such as the Internet. In particular, universally composable definitions guarantee security even when an unbounded number of protocol instances are executed concurrently in an adversarially controlled manner, they guarantee non-malleability with respect to arbitrary protocols, and more. We show how to formulate universally composable definitions of security for practically any cryptographic task. Furthermore, we demonstrate that practically any such definition can be realized using known techniques, as long as only a minority of the participants are corrupted. We then proceed to formulate universally composable definitions of a wide array of cryptographic tasks, including authenticated and secure communication, key-exchange, public-key encryption, signature, commitment, oblivious transfer, zero knowledge and more. We also make initial steps towards studying the realizability of the proposed definitions in various settings.
---
paper_title: Analysing Unlinkability and Anonymity Using the Applied Pi Calculus

paper_content:

An attacker that can identify messages as coming from the same source, can use this information to build up a picture of targets’ behaviour, and so, threaten their privacy. In response to this danger, unlinkable protocols aim to make it impossible for a third party to identify two runs of a protocol as coming from the same device. We present a framework for analysing unlinkability and anonymity in the applied pi calculus. We show that unlinkability and anonymity are complementary properties; one does not imply the other. Using our framework we show that the French RFID e-passport preserves anonymity but it is linkable therefore anyone carrying a French e-passport can be physically traced.
---
paper_title: Linking Unlinkability

paper_content:

Unlinkability is a privacy property of crucial importance for several systems such as RFID or voting systems. Informally, unlinkability states that, given two events/items in a system, an attacker is not able to infer whether they are related to each other. However, in the literature we find several definitions for this notion, which are apparently unrelated and shows a potentially problematic lack of agreement. This paper sheds new light on unlinkability by comparing different ways of defining it and showing that in many practical situations the various definitions coincide. It does so by a expressing in a unifying framework four definitions of unlinkability from the literature b demonstrating how these definitions are different yet related to each other and to their dual notion of "inseparability" and c by identifying conditions under which all these definitions become equivalent. We argue that the conditions are reasonable to expect in identification systems, and we prove that they hold for a generic class of protocols.
---
paper_title: Practical everlasting privacy

paper_content:

Will my vote remain secret in 20 years? This is a natural question in the context of electronic voting, where encrypted votes may be published on a bulletin board for verifiability purposes, but the strength of the encryption is eroded with the passage of time. The question has been addressed through a property referred to as everlasting privacy. Perfect everlasting privacy may be difficult or even impossible to achieve, in particular in remote electronic elections. In this paper, we propose a definition of practical everlasting privacy. The key idea is that in the future, an attacker will be more powerful in terms of computation (he may be able to break the cryptography) but less powerful in terms of the data he can operate on (transactions between a vote client and the vote server may not have been stored). ::: ::: We formalize our definition of everlasting privacy in the applied-pi calculus. We provide the means to characterize what an attacker can break in the future in several cases. In particular, we model this for perfectly hiding and computationally binding primitives (or the converse), such as Pedersen commitments, and for symmetric and asymmetric encryption primitives. We adapt existing tools, in order to allow us to automatically prove everlasting privacy. As an illustration, we show that several variants of Helios (including Helios with Pedersen commitments) and a protocol by Moran and Naor achieve practical everlasting privacy, using the ProVerif and the AKiSs tools.
---
paper_title: Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus

paper_content:

We present a general technique for modeling remote electronic voting protocols in the applied pi-calculus and for automatically verifying their security. In the first part of this paper, we provide novel definitions that address several important security properties. In particular, we propose a new formalization of coercion-resistance in terms of observational equivalence. In contrast to previous definitions in the symbolic model, our definition of coercion-resistance is suitable for automation and captures simulation and forced-abstention attacks. Additionally, we express inalterability, eligibility, and non-reusability as a correspondence property on traces. In the second part, we use ProVerif to illustrate the feasibility of our technique by providing the first automated security proof of the coercion-resistant protocol proposed by Juels, Catalano, and Jakobsson.
---
paper_title: Coercion-resistance and receipt-freeness in electronic voting

paper_content:

In this paper we formally study important properties of electronic voting protocols. In particular we are interested in coercion-resistance and receipt-freeness. Intuitively, an election protocol is coercion-resistant if a voter A cannot prove to a potential coercer C that she voted in a particular way. We assume that A cooperates with C in an interactive fashion. Receipt-freeness is a weaker property, for which we assume that A and C cannot interact during the protocol: to break receipt-freeness, A later provides evidence (the receipt) of how she voted. While receipt-freeness can be expressed using observational equivalence from the applied pi calculus, we need to introduce a new relation to capture coercion-resistance. Our formalization of coercion-resistance and receipt-freeness are quite different. Nevertheless, we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies privacy, the basic anonymity property of voting protocols, as defined in previous work. Finally we illustrate the definitions on a simplified version of the Lee et al. voting protocol.
---
paper_title: Analysis of an Electronic Voting Protocol in the Applied Pi Calculus

paper_content:

Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. The applied pi calculus is a formalism for modelling such protocols, and allows us to verify properties by using automatic tools, and to rely on manual proof techniques for cases that automatic tools are unable to handle. We model a known protocol for elections known as FOO 92 in the applied pi calculus, and we formalise three of its expected properties, namely fairness, eligibility, and privacy. We use the ProVerif tool to prove that the first two properties are satisfied. In the case of the third property, ProVerif is unable to prove it directly, because its ability to prove observational equivalence between processes is not complete. We provide a manual proof of the required equivalence.
---
paper_title: Analysis of a receipt-free auction protocol in the applied pi calculus

paper_content:

We formally study two privacy-type properties for online auction protocols: bidding-price-secrecy and receipt-freeness. These properties are formalised as observational equivalences in the applied π calculus. We analyse the receipt-free auction protocol by Abe and Suzuki. Bidding-price-secrecy of the protocol is verified using ProVerif, whereas receipt-freeness of the protocol is proved manually.
---
paper_title: Secrecy by typing in security protocols

paper_content:

We develop principles and rules for achieving secrecy properties in security protocols. Our approach is based on traditional classification techniques, and extends those techniques to handle concurrent processes that use shared-key cryptography. The rules have the form of typing rules for a basic concurrent language with cryptographic primitives, the spi calculus. They guarantee that, if a protocol typechecks, then it does not leak its secret inputs.
---
paper_title: Formal Verification of Privacy for RFID Systems

paper_content:

RFID tags are being widely employed in a variety of applications, ranging from barcode replacement to electronic passports. Their extensive use, however, in combination with their wireless nature, introduces privacy concerns as a tag could leak information about the owner’s behaviour. In this paper we define two privacy notions, unlinkability and forward privacy, using a formal model based on the applied pi calculus, and we show the relationship between them. Then we focus on a generic class of simple privacy protocols, giving sufficient and necessary conditions for unlinkability and forward privacy for this class. These conditions are based on the concept of frame independence that we develop in this paper. Finally, we apply our techniques to two identification protocols, formally proving their privacy guarantees.
---
paper_title: Untraceability in the applied pi-calculus

paper_content:

The use of RFID tags in personal items, such as passports, may make it possible to track a person's movements. Even RFID protocols that encrypt their identity may leak enough information to let an attacker trace a tag. In this paper we define strong and weak forms of untraceablility, and illustrate these definitions with a simple example. We formally define these concepts in the applied pi-calculus which in some cases makes it possible to automatically check if an RFID tag running a particular protocol is untraceable.
---
paper_title: Formal Verification of e-Auction Protocols

paper_content:

Auctions have a long history, having been recorded as early as 500 B.C.. With the rise of Internet, electronic auctions have been a great success and are increasingly used. Many cryptographic protocols have been proposed to address the various security requirements of these electronic transactions. We propose a formal framework to analyze and verify security properties of e-Auction protocols. We model protocols in the Applied π-Calculus and define privacy notions, which include secrecy of bids, anonymity of the participants, receipt-freeness and coercion-resistance. We also discuss fairness, non-repudiation and non-cancellation. Additionally we show on two case studies how these properties can be verified automatically using ProVerif, and discover several attacks.
---
paper_title: A hierarchy of authentication specifications

paper_content:

Many security protocols have the aim of authenticating one agent to another. Yet there is no clear consensus in the academic literature about precisely what "authentication" means. We suggest that the appropriate authentication requirement will depend upon the use to which the protocol is put, and identify several possible definitions of "authentication". We formalize each definition using the process algebra CSP, use this formalism to study their relative strengths, and show how the model checker FDR can be used to test whether a system running the protocol meets such a specification.
---
paper_title: Symbolic Universal Composability

paper_content:

We introduce a variant of the Universal Composability framework (UC; Canetti, FOCS 2001) that uses symbolic cryptography. Two salient properties of the UC framework are secure composition and the possibility of easily defining security by giving an ideal functionality as specification. These advantages are now also available in a symbolic modeling of cryptography, allowing for a modular analysis of complex protocols. We furthermore introduce a new technique for modular design of protocols that uses UC but avoids the need for powerful cryptographic primitives that often comes with UC protocols; this "virtual primitives" approach is unique to the symbolic setting and has no counterpart in the original computational UC framework.
---
paper_title: A Calculus for Cryptographic Protocols: The Spi Calculus

paper_content:

We introduce the spi calculus, an extension of the pi calculus designed for describing and analyzing cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence.
---
paper_title: Automatic proof of strong secrecy for security protocols

paper_content:

We present a new automatic technique for proving strong secrecy for security protocols. Strong secrecy means that an adversary cannot see any difference when the value of the secret changes. Our technique relies on an automatic translation of the protocol into Horn clauses, and a resolution algorithm on the clauses. It requires important extensions with respect to previous work for the proof of (standard) secrecy and authenticity. This technique can handle a wide range of cryptographic primitives, and yields proofs valid for an unbounded number of sessions and an unbounded message space; it is also flexible and efficient. We have proved its correctness, implemented it, and tested it on several examples of protocols including JFK by W. Aiello et al. (2002).
---
paper_title: Verifying privacy-type properties of electronic voting protocols

paper_content:

Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. We study three privacy-type properties of electronic voting protocols: in increasing order of strength, they are vote-privacy, receipt-freeness and coercion-resistance. ::: ::: We use the applied pi calculus, a formalism well adapted to modelling such protocols, which has the advantages of being based on well-understood concepts. The privacy-type properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies vote-privacy. ::: ::: We illustrate our definitions on three electronic voting protocols from the literature. Ideally, these three properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy receipt-freeness or coercion-resistance may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.
---
paper_title: Mobile values, new names, and secure communication

paper_content:

We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. Specifically, we introduce a simple, general extension of the pi calculus with value passing, primitive functions, and equations among terms. We develop semantics and proof techniques for this extended language and apply them in reasoning about some security protocols.
---
paper_title: On the security of public key protocols

paper_content:

Recently the use of public key encryption to provide secure network communication has received considerable attention. Such public key systems are usually effective against passive eavesdroppers, who merely tap the lines and try to decipher the message. It has been pointed out, however, that an improperly designed protocol could be vulnerable to an active saboteur, one who may impersonate another user or alter the message being transmitted. Several models are formulated in which the security of protocols can be discussed precisely. Algorithms and characterizations that can be used to determine protocol security in these models are given.
---
paper_title: Analysis of an Electronic Voting Protocol in the Applied Pi Calculus

paper_content:

Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. The applied pi calculus is a formalism for modelling such protocols, and allows us to verify properties by using automatic tools, and to rely on manual proof techniques for cases that automatic tools are unable to handle. We model a known protocol for elections known as FOO 92 in the applied pi calculus, and we formalise three of its expected properties, namely fairness, eligibility, and privacy. We use the ProVerif tool to prove that the first two properties are satisfied. In the case of the third property, ProVerif is unable to prove it directly, because its ability to prove observational equivalence between processes is not complete. We provide a manual proof of the required equivalence.
---
paper_title: FAST: an efficient decision procedure for deduction and static equivalence

paper_content:

Message deducibility and static equivalence are central problems in ::: symbolic security protocol analysis. We present FAST, an efficient ::: decision procedure for these problems under subterm-convergent ::: equational theories. FAST is a C++ implementation of an improved ::: version of the algorithm presented in our previous work. This ::: algorithm has a better asymptotic complexity than other algorithms ::: implemented by existing tools for the same task, and FAST's ::: optimizations further improve these complexity results. ::: ::: We describe here the main ideas of our implementation and compare its ::: performance with competing tools. The results show that our ::: implementation is significantly faster: for many examples, FAST ::: terminates in under a second, whereas other tools take several ::: minutes.
---
paper_title: Decidability and Combination Results for Two Notions of Knowledge in Security Protocols

paper_content:

In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). The analysis of cryptographic protocols requires a precise understanding of the attacker knowledge. Two standard notions are usually considered: deducibility and indistinguishability. Those notions are well-studied and several decidability results already exist to deal with a variety of equational theories. Most of the existing results are dedicated to specific equational theories and only few results, especially in the case of indistinguishability, have been obtained for equational theories with associative and commutative properties $(\textsf{AC})$ . In this paper, we show that existing decidability results can be easily combined for any disjoint equational theories: if the deducibility and indistinguishability relations are decidable for two disjoint theories, they are also decidable for their union. We also propose a general setting for solving deducibility and indistinguishability for an important class (called monoidal) of equational theories involving $\textsf{AC}$ operators. As a consequence of these two results, new decidability and complexity results can be obtained for many relevant equational theories.
---
paper_title: Deciding knowledge in security protocols under equational theories

paper_content:

The analysis of security protocols requires precise formulations of the knowledge of protocol participants and attackers. In formal approaches this knowledge is often treated in terms of message deducibility and indistinguishability relations. In this paper we study the decidability of these two relations. The messages in question may employ functions (encryption, decryption, etc.) axiomatized in an equational theory. One of our main positive results says that deducibility and indistinguishability are both decidable in polynomial time for a large class of equational theories. This class of equational theories is defined syntactically and includes, for example, theories for encryption, decryption, and digital signatures. We also establish general decidability theorems for an even larger class of theories. These theorems require only loose, abstract conditions, and apply to many other useful theories, for example with blind digital signatures, homomorphic encryption, XOR, and other associative-commutative functions.
---
paper_title: Mobile values, new names, and secure communication

paper_content:

We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. Specifically, we introduce a simple, general extension of the pi calculus with value passing, primitive functions, and equations among terms. We develop semantics and proof techniques for this extended language and apply them in reasoning about some security protocols.
---
paper_title: Deciding knowledge in security protocols under (many more) equational theories

paper_content:

In the analysis of security protocols, the knowledge of attackers is often described in terms of message deducibility and indistinguishability relations. In this paper, we pursue the study of these two relations. We establish general decidability theorems for both. These theorems require only loose, abstract conditions on the equational theory for messages. They subsume previous results for a syntactically defined class of theories that allows basic equations for functions such as encryption, decryption, and digital signatures. They also apply to many other useful theories, for example with blind digital signatures, homomorphic encryption, XOR, and other associative-commutative functions.
---
paper_title: Computing Knowledge in Security Protocols Under Convergent Equational Theories

paper_content:

The analysis of security protocols requires reasoning about the knowledge an attacker acquires by eavesdropping on network traffic. In formal approaches, the messages exchanged over the network are modelled by a term algebra equipped with an equational theory axiomatising the properties of the cryptographic primitives (e.g. encryption, signature). In this context, two classical notions of knowledge, deducibility and indistinguishability, yield corresponding decision problems. We propose a procedure for both problems under arbitrary convergent equational theories. Since the underlying problems are undecidable we cannot guarantee termination. Nevertheless, our procedure terminates on a wide range of equational theories. In particular, we obtain a new decidability result for a theory we encountered when studying electronic voting protocols. We also provide a prototype implementation.
---
paper_title: YAPA: A Generic Tool for Computing Intruder Knowledge

paper_content:

Reasoning about the knowledge of an attacker is a necessary step in many formal analyses of security protocols. In the framework of the applied pi calculus, as in similar languages based on equational logics, knowledge is typically expressed by two relations: deducibility and static equivalence. Several decision procedures have been proposed for these relations under a variety of equational theories. However, each theory has its particular algorithm, and none has been implemented so far. We provide a generic procedure for deducibility and static equivalence that takes as input any convergent rewrite system. We show that our algorithm covers most of the existing decision procedures for convergent theories. We also provide an efficient implementation, and compare it briefly with the tools ProVerif and KiSs.
---
paper_title: Mobile values, new names, and secure communication

paper_content:

We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. Specifically, we introduce a simple, general extension of the pi calculus with value passing, primitive functions, and equations among terms. We develop semantics and proof techniques for this extended language and apply them in reasoning about some security protocols.
---
paper_title: A Calculus for Cryptographic Protocols: The Spi Calculus

paper_content:

We introduce the spi calculus, an extension of the pi calculus designed for describing and analyzing cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence.
---
paper_title: Proof techniques for cryptographic processes

paper_content:

Contextual equivalences for cryptographic process calculi can be used to reason about correctness of protocols, but their definition suffers from quantification over all possible contexts. Here, we focus on two such equivalences, may-testing and barbed equivalence, and investigate tractable proof methods for them. To this aim, we develop an 'environment-sensitive' labelled transition system, where transitions are constrained by the knowledge the environment has of names and keys. On top of the new transition system, a trace equivalence and a co-inductive weak bisimulation equivalence are defined, both of which avoid quantification over contexts. Our main results are soundness of trace semantics and of weak bisimulation with respect to may-testing and barbed equivalence, respectively. This leads to more direct proof methods for equivalence checking. The use of such methods is illustrated via a few examples concerning implementation of secure channels by means of encrypted public channels. We also consider a variant of the labelled transition system that gives completeness, but is less handy to use.
---
paper_title: Analysing Unlinkability and Anonymity Using the Applied Pi Calculus

paper_content:

An attacker that can identify messages as coming from the same source, can use this information to build up a picture of targets’ behaviour, and so, threaten their privacy. In response to this danger, unlinkable protocols aim to make it impossible for a third party to identify two runs of a protocol as coming from the same device. We present a framework for analysing unlinkability and anonymity in the applied pi calculus. We show that unlinkability and anonymity are complementary properties; one does not imply the other. Using our framework we show that the French RFID e-passport preserves anonymity but it is linkable therefore anyone carrying a French e-passport can be physically traced.
---
paper_title: Mobile values, new names, and secure communication

paper_content:

We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. Specifically, we introduce a simple, general extension of the pi calculus with value passing, primitive functions, and equations among terms. We develop semantics and proof techniques for this extended language and apply them in reasoning about some security protocols.
---
paper_title: Psi-calculi: a framework for mobile processes with nominal data and logic

paper_content:

The framework of psi-calculi extends the pi-calculus with nominal datatypes for data structures and for logical assertions and conditions. These can be transmitted between processes and their names ...
---
paper_title: Deciding equivalence-based properties using constraint solving

paper_content:

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 sucient 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.
---
paper_title: A Bisimulation Method for Cryptographic Protocols

paper_content:

We introduce a definition of bisimulation for cryptographic protocols. The definition includes a simple and precise model of the knowledge of the environment with which a protocol interacts. Bisimulation is the basis of an effective proof technique, which yields proofs of classical security properties of protocols and also justifies certain protocol optimisations. The setting for our work is the spi calculus, an extension of the pi calculus with cryptographic primitives. We prove the soundness of the bisimulation proof technique within the spi calculus.
---
paper_title: A Calculus for Cryptographic Protocols: The Spi Calculus

paper_content:

We introduce the spi calculus, an extension of the pi calculus designed for describing and analyzing cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence.
---
paper_title: Verifying privacy-type properties of electronic voting protocols

paper_content:

Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. We study three privacy-type properties of electronic voting protocols: in increasing order of strength, they are vote-privacy, receipt-freeness and coercion-resistance. ::: ::: We use the applied pi calculus, a formalism well adapted to modelling such protocols, which has the advantages of being based on well-understood concepts. The privacy-type properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies vote-privacy. ::: ::: We illustrate our definitions on three electronic voting protocols from the literature. Ideally, these three properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy receipt-freeness or coercion-resistance may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.
---
paper_title: From security protocols to pushdown automata

paper_content:

Formal methods have been very successful in analyzing security pro- tocols for reachability properties such as secrecy or authentication. In contrast, there are very few results for equivalence-based properties, crucial for studying e.g. privacy-like properties such as anonymity or vote secrecy. We study the problem of checking equivalence of security protocols for an un- bounded number of sessions. Since replication leads very quickly to undecidabil- ity (even in the simple case of secrecy), we focus on a limited fragment of pro- tocols (standard primitives but pairs, one variable per protocol's rules) for which the secrecy preservation problem is known to be decidable. Surprisingly, this frag- ment turns out to be undecidable for equivalence. Then, restricting our attention to deterministic protocols, we propose the first decidability result for checking equivalence of protocols for an unbounded number of sessions. This result is ob- tained through a characterization of equivalence of protocols in terms of equality of languages of (generalized, real-time) deterministic pushdown automata.
---
paper_title: The Psi-Calculi Workbench: A Generic Tool for Applied Process Calculi

paper_content:

Psi-calculi is a parametric framework for extensions of the pi-calculus with arbitrary data and logic. All instances of the framework inherit machine-checked proofs of the metatheory such as compositionality and bisimulation congruence. We present a generic analysis tool for psi-calculus instances, enabling symbolic execution and (bi)simulation checking for both unicast and broadcast communication. The tool also provides a library for implementing new psi-calculus instances. We provide examples from traditional communication protocols and wireless sensor networks. We also describe the theoretical foundations of the tool, including an improved symbolic operational semantics, with additional support for scoped broadcast communication.
---
paper_title: Symbolic bisimulation for the applied pi calculus

paper_content:

We propose a symbolic semantics for the finite applied pi calculus, which is a variant of the pi calculus with extensions for modelling cryptographic protocols. By treating inputs symbolically, our semantics avoids potentially infinite branching of execution trees due to inputs from the environment. Correctness is maintained by associating with each process a set of constraints on terms. We define a sound symbolic labelled bisimulation relation. This is an important step towards automation of observational equivalence for the finite applied pi calculus, e.g. for verification of anonymity or strong secrecy properties.
---
paper_title: Automatic testing equivalence verification of spi calculus specifications

paper_content:

Testing equivalence is a powerful means for expressing the security properties of cryptographic protocols, but its formal verification is a difficult task because of the quantification over contexts on which it is based. Previous articles have provided insights into using theorem-proving for the verification of testing equivalence of spi calculus specifications. This article addresses the same verification problem, but uses a state exploration approach. The verification technique is based on the definition of an environment-sensitive, labeled transition system representing a spi calculus specification. Trace equivalence defined on such a transition system coincides with testing equivalence. Symbolic techniques are used to keep the set of traces finite. If a difference in the traces of two spi descriptions (typically a specification and the corresponding implementation of a protocol) is found, it can be used to automatically build the spi calculus description of an intruder process that can exploit the difference.
---
paper_title: A Complete Symbolic Bisimilarity for an Extended Spi Calculus

paper_content:

Several symbolic notions of bisimilarity have been defined for the spi calculus and the applied pi calculus. In this paper, we treat a spi calculus with a general constructor-destructor message algebra, and define a symbolic bisimilarity that is both sound and complete with respect to its concrete counterpart.
---
paper_title: A Trace Based Bisimulation for the Spi Calculus

paper_content:

A notion of open bisimulation is formulated for the spi calculus, an extension of the π-calculus with cryptographic primitives. In this formulation, open bisimulation is indexed by pairs of symbolic traces, which represent the history of interactions between the environment with the pairs of processes being checked for bisimilarity. The use of symbolic traces allows for a symbolic treatment of bound input in bisimulation checking which avoids quantification over input values. Open bisimilarity is shown to be sound with respect to testing equivalence, and futher, it is shown to be an equivalence relation on processes and a congruence on finite processes.
---
paper_title: Trace equivalence decision: negative tests and non-determinism

paper_content:

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).
---
paper_title: Lengths may break privacy – or how to check for equivalences with length ⋆

paper_content:

Security protocols have been successfully analyzed using symbolic models, where messages are represented by terms and protocols by processes. Privacy properties like anonymity or untraceability are typically expressed as equivalence between processes. While some decision procedures have been proposed for automatically deciding process equivalence, all existing approaches abstract away the information an attacker may get when observing the length of messages. ::: ::: In this paper, we study process equivalence with length tests. We first show that, in the static case, almost all existing decidability results for static equivalence can be extended to cope with length tests. In the active case, we prove decidability of trace equivalence with length tests, for a bounded number of sessions and for standard primitives. Our result relies on a previous decidability result from Cheval et al [15] without length tests. Our procedure has been implemented and we have discovered a new flaw against privacy in the biometric passport protocol.
---
paper_title: Automated Verification of Equivalence Properties of Cryptographic Protocols

paper_content:

Indistinguishability 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 that 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 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.
---
paper_title: Deciding security of protocols against off-line guessing attacks

paper_content:

We provide an effective procedure for deciding the existence of off-line guessing attacks on security protocols, for a bounded number of sessions.The procedure consists of a constraint solving algorithm for determining satisfiability and equivalence of a class of second-order E-unification problems, where the equational theory E is presented by a convergent subterm rewriting system.To the best of our knowledge, this is the first decidability result to use the generic definition of off-line guessing attacks due to Corin et al. based on static equivalence in the applied pi calculus.
---
paper_title: APTE: An Algorithm for Proving Trace Equivalence

paper_content:

This 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.
---
paper_title: Deciding equivalence-based properties using constraint solving

paper_content:

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 sucient 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.
---
paper_title: Timing Attacks in Security Protocols: Symbolic Framework and Proof Techniques

paper_content:

We 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.
---
paper_title: Automating security analysis: symbolic equivalence of constraint systems

paper_content:

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.
---
paper_title: Automating Open Bisimulation Checking for the Spi Calculus

paper_content:

We consider the problem of automating open bisimulation checking for the spi calculus, an extension of the pi-calculus with cryptographic primitives. The notion of open bisimulation considered here is indexed by a (symbolic) environment, represented as bi-traces (i.e., pairs of symbolic traces), which encode the history of interaction between the intruder with the processes being checked for bisimilarity. A crucial part of the definition of this open bisimulation, that is, the notion of consistency of bi-traces, involves infinite quantification over a certain notion of “respectful substitutions”. We show that one needs only to check a finite number of respectful substitutions in order to check bi-trace consistency. Our decision procedure uses techniques that have been well developed in the area of symbolic trace analysis for security protocols. More specifically, we make use of techniques for symbolic trace refinement, which transform a symbolic trace into a finite set of symbolic traces in a certain “solved form”. Crucially, we show that refinements of a projection of a bitrace can be uniquely extended to refinements of the bi-trace, and that consistency of all instances of the original bi-trace can be reduced to consistency of its finite set of refinements. We then give a sound and complete procedure for deciding open bisimilarity for finite spi processes.
---
paper_title: Automated Verification of Equivalence Properties of Cryptographic Protocols

paper_content:

Indistinguishability 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 that 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 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.
---
paper_title: Partial Order Reduction for Security Protocols

paper_content:

Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g., anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools. ::: In this paper, we overcome this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.
---
paper_title: A reduced semantics for deciding trace equivalence using constraint systems

paper_content:

Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e. without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. Modersheim et al. [18] have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimization in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly.
---
paper_title: The Finite Variant Property: How to Get Rid of Some Algebraic Properties

paper_content:

We consider the following problem: Given a term t, a rewrite system $\cal R$, a finite set of equations E′ such that $\cal R$ is E′-convergent, compute finitely many instances of t: t1,...,tn such that, for every substitution σ, there is an index i and a substitution θ such that $t\sigma\mathord\downarrow =_{E'} t_i\theta$ (where $t\sigma\mathord\downarrow$ is the normal form of tσ w.r.t. $\to_{E'\mathord{\setminus}\mathcal R}$). ::: ::: The goal of this paper is to give equivalent (resp. sufficient) conditions for the finite variant property and to systematically investigate this property for equational theories, which are relevant to security protocols verification. For instance, we prove that the finite variant property holds for Abelian Groups, and a theory of modular exponentiation and does not hold for the theory ACUNh (Associativity, Commutativity, Unit, Nilpotence, homomorphism).
---
paper_title: Decidability of Trace Equivalence for Protocols with Nonces

paper_content:

Privacy properties such as anonymity, unlink ability, or vote secrecy are typically expressed as equivalence properties. In this paper, we provide the first decidability result for trace equivalence of security protocols, for an unbounded number of sessions and unlimited fresh nonce's. Our class encompasses most symmetric key protocols of the literature, in their tagged variant.
---
paper_title: Typing messages for free in security protocols: the case of equivalence properties

paper_content:

Privacy properties such as untraceability, vote secrecy, or anonymity are typically expressed as behavioural equivalence in a process algebra that models security protocols. In this paper, we study how to decide one particular relation, namely trace equivalence, for an unbounded number of sessions.
---
paper_title: From security protocols to pushdown automata

paper_content:

Formal methods have been very successful in analyzing security pro- tocols for reachability properties such as secrecy or authentication. In contrast, there are very few results for equivalence-based properties, crucial for studying e.g. privacy-like properties such as anonymity or vote secrecy. We study the problem of checking equivalence of security protocols for an un- bounded number of sessions. Since replication leads very quickly to undecidabil- ity (even in the simple case of secrecy), we focus on a limited fragment of pro- tocols (standard primitives but pairs, one variable per protocol's rules) for which the secrecy preservation problem is known to be decidable. Surprisingly, this frag- ment turns out to be undecidable for equivalence. Then, restricting our attention to deterministic protocols, we propose the first decidability result for checking equivalence of protocols for an unbounded number of sessions. This result is ob- tained through a characterization of equivalence of protocols in terms of equality of languages of (generalized, real-time) deterministic pushdown automata.
---
paper_title: Proving More Observational Equivalences with ProVerif

paper_content:

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 inside terms, to allow ProVerif to prove the desired equivalence. These extensions have been implemented in ProVerif and allow us to automatically prove anonymity in the private authentication protocol by Abadi and Fournet.
---
paper_title: Automatic verification of privacy properties in the applied pi calculus

paper_content:

We develop a formal method verification technique for cryptographic protocols. We focus on proving observational equivalences of the kind P ∼ Q, where the processes P and Q have the same structure and differ only in the choice of terms. The calculus of ProVerif, a variant of the applied pi calculus, makes some progress in this direction. We expand the scope of ProVerif, to provide reasoning about further equivalences. We also provide an extension which allows modelling of protocols which require global synchronisation. Finally we develop an algorithm to enable automated reasoning. We demonstrate the practicality of our work with two case studies.
---
paper_title: Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers

paper_content:

Observational equivalence allows us to study important security properties such as anonymity. Unfortunately, the difficulty of proving observational equivalence hinders analysis. Blanchet, Abadi & Fournet simplify its proof by introducing a sufficient condition for observational equivalence, called diff-equivalence, which is a reachability condition that can be proved automatically by ProVerif. However, diff-equivalence is a very strong condition, which often does not hold even if observational equivalence does. In particular, when proving equivalence between processes that contain several parallel components, e.g., P | Q and P' | Q', diff-equivalence requires that P is equivalent to P' and Q is equivalent to Q'. To relax this constraint, Delaune, Ryan & Smyth introduced the idea of swapping data between parallel processes P' and Q' at synchronisation points, without proving its soundness. We extend their work by formalising the semantics of synchronisation, formalising the definition of swapping, and proving its soundness. We also relax some restrictions they had on the processes to which swapping can be applied. Moreover, we have implemented our results in ProVerif. Hence, we extend the class of equivalences that can be proved automatically. We showcase our results by analysing privacy in election schemes by Fujioka, Okamoto & Ohta and Lee et al., and in the vehicular ad-hoc network by Freudiger et al.
---
paper_title: Analysing Unlinkability and Anonymity Using the Applied Pi Calculus

paper_content:

An attacker that can identify messages as coming from the same source, can use this information to build up a picture of targets’ behaviour, and so, threaten their privacy. In response to this danger, unlinkable protocols aim to make it impossible for a third party to identify two runs of a protocol as coming from the same device. We present a framework for analysing unlinkability and anonymity in the applied pi calculus. We show that unlinkability and anonymity are complementary properties; one does not imply the other. Using our framework we show that the French RFID e-passport preserves anonymity but it is linkable therefore anyone carrying a French e-passport can be physically traced.
---
paper_title: Automated Symbolic Proofs of Observational Equivalence

paper_content:

Many cryptographic security definitions can be naturally formulated as observational equivalence properties. However, existing automated tools for verifying the observational equivalence of cryptographic protocols are limited: they do not handle protocols with mutable state and an unbounded number of sessions. We propose a novel definition of observational equivalence for multiset rewriting systems. We then extend the Tamarin prover, based on multiset rewriting, to prove the observational equivalence of protocols with mutable state, an unbounded number of sessions, and equational theories such as Diffie-Hellman exponentiation. We demonstrate its effectiveness on case studies, including a stateful TPM protocol.
---
paper_title: The Finite Variant Property: How to Get Rid of Some Algebraic Properties

paper_content:

We consider the following problem: Given a term t, a rewrite system $\cal R$, a finite set of equations E′ such that $\cal R$ is E′-convergent, compute finitely many instances of t: t1,...,tn such that, for every substitution σ, there is an index i and a substitution θ such that $t\sigma\mathord\downarrow =_{E'} t_i\theta$ (where $t\sigma\mathord\downarrow$ is the normal form of tσ w.r.t. $\to_{E'\mathord{\setminus}\mathcal R}$). ::: ::: The goal of this paper is to give equivalent (resp. sufficient) conditions for the finite variant property and to systematically investigate this property for equational theories, which are relevant to security protocols verification. For instance, we prove that the finite variant property holds for Abelian Groups, and a theory of modular exponentiation and does not hold for the theory ACUNh (Associativity, Commutativity, Unit, Nilpotence, homomorphism).
---
paper_title: A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA

paper_content:

Intuitively, two protocols \({\mathcal P}_1\) and \({\mathcal P}_2\) are indistinguishable if an attacker cannot tell the difference between interactions with \({\mathcal P}_1\) and with \({\mathcal P}_2\). In this paper we: (i) propose an intuitive notion of indistinguishability in Maude-NPA; (ii) formalize such a notion in terms of state unreachability conditions on their synchronous product; (iii) prove theorems showing how —assuming the protocol’s algebraic theory has a finite variant (FV) decomposition– these conditions can be checked by the Maude-NPA tool; and (iv) illustrate our approach with concrete examples. This provides for the first time a framework for automatic analysis of indistinguishability modulo as wide a class of algebraic properties as FV, which includes many associative-commutative theories of interest to cryptographic protocol analysis.
---
paper_title: Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity

paper_content:

Verification of trace equivalence is difficult to automate in general because it requires relating two infinite sets of traces. The problem becomes even more complex when algebraic properties of cryptographic primitives are taken in account in the formal model. For example, no verification tool or technique can currently handle automatically a realistic model of re-encryption or associative-commutative operators. ::: ::: In this setting, we propose a general technique for reducing the set of traces that have to be analyzed to a set of local traces. A local trace restricts the way in which some function symbols are used, and this allows us to perform a second reduction, by showing that some algebraic properties can be safely ignored in local traces. ::: ::: In particular, local traces for re-encryption will contain only a bounded number of re-encryptions for any given ciphertext, leading to a sound elimination of equations that model re-encryption. For associativity and commutativity, local traces will determine a canonical use of the associative-commutative operator, where reasoning modulo AC is no stronger than reasoning without AC. ::: ::: We illustrate these results by considering a non-disjoint combination of equational theories for the verification of vote privacy in Pret a Voter. ProVerif can not handle the input theory as it is, but it does terminate with success on the theory obtained using our reduction result.
---
paper_title: Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties

paper_content:

We present a general approach for the symbolic analysis of security protocols that use Diffie-Hellman exponentiation to achieve advanced security properties. We model protocols as multiset rewriting systems and security properties as first-order formulas. We analyze them using a novel constraint-solving algorithm that supports both falsification and verification, even in the presence of an unbounded number of protocol sessions. The algorithm exploits the finite variant property and builds on ideas from strand spaces and proof normal forms. We demonstrate the scope and the effectiveness of our algorithm on non-trivial case studies. For example, the algorithm successfully verifies the NAXOS protocol with respect to a symbolic version of the eCK security model.
---
paper_title: Verifying privacy-type properties of electronic voting protocols

paper_content:

Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. We study three privacy-type properties of electronic voting protocols: in increasing order of strength, they are vote-privacy, receipt-freeness and coercion-resistance. ::: ::: We use the applied pi calculus, a formalism well adapted to modelling such protocols, which has the advantages of being based on well-understood concepts. The privacy-type properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies vote-privacy. ::: ::: We illustrate our definitions on three electronic voting protocols from the literature. Ideally, these three properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy receipt-freeness or coercion-resistance may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.
---
paper_title: Folding variant narrowing and optimal variant termination

paper_content:

If a set of equations E∪Ax is such that E is confluent, terminating, and coherent modulo Ax, narrowing with E modulo Ax provides a complete E∪Ax-unification algorithm. However, except for the hopelessly inefficient case of full narrowing, nothing seems to be known about effective narrowing strategies in the general modulo case beyond the quite depressing observation that basic narrowing is incomplete modulo AC. In this work we propose an effective strategy based on the idea of the E∪Ax-variants of a term that we call folding variant narrowing. This strategy is complete, both for computing E∪Ax-unifiers and for computing a minimal complete set of variants for any input term. And it is optimally variant terminating in the sense of terminating for an input term t iff t has a finite, complete set of variants. The applications of folding variant narrowing go beyond providing a complete E∪Ax - unification algorithm: computing the E∪Ax-variants of a term may be just as important as computing E∪Ax-unifiers in recent applications of folding variant narrowing such as termination methods modulo axioms, and checking confluence and coherence of rules modulo axioms.
---
paper_title: Automated verification of selected equivalences for security protocols

paper_content:

In the analysis of security protocols, methods and tools for reasoning about protocol behaviors have been quite effective. We aim to expand the scope of those methods and tools. We focus on proving equivalences P/spl ap/Q in which P and Q are two processes that differ only in the choice of some terms. These equivalences arise often in applications. We show how to treat them as predicates on the behaviors of a process that represents P and Q at the same time. We develop our techniques in the context of the applied pi calculus and implement them in the tool ProVerif.
---
paper_title: Privacy through Pseudonymity in Mobile Telephony Systems

paper_content:

To protect mobile phone from tracking by third parties, mobile telephony systems rely on periodically chang- ing pseudonyms. We experimentally and formally analyse the mechanism adopted to update these pseudonyms and point out design and implementation weaknesses that defeat its purpose by allowing the identification and/or tracking of mobile telephony users. In particular, the experiments show that the pseudonym changing mechanism as implemented by real networks does not achieve the intended privacy goals. Moreover, we found out that the standard is flawed and that it is possible to exploit the procedure used to assign a new pseudonym, the TMSI reallocation procedure, in order to track users. We propose countermeasures to tackle the exposed vulnerabilities and formally prove that the 3GPP standard should require the establishment of a fresh ciphering key before each execution of the TMSI reallocation procedure to provide unlinkability.
---
paper_title: Attacking and fixing Helios: An analysis of ballot secrecy

paper_content:

Helios 2.0 is an open-source web-based end-to-end verifiable electronic voting system, suitable for use in low-coercion environments. In this article, we analyse ballot secrecy in Helios and discover a vulnerability which allows an adversary to compromise the privacy of voters. The vulnerability exploits the absence of ballot independence in Helios and works by replaying a voter's ballot or a variant of it, the replayed ballot magnifies the voter's contribution to the election outcome and this magnification can be used to violated privacy. We demonstrate the practicality of the attack by violating a voter's privacy in a mock election using the software implementation of Helios. Moreover, the feasibility of an attack is considered in the context of French legislative elections and, based upon our findings, we believe it constitutes a real threat to ballot secrecy. We present a fix and show that our solution satisfies a formal definition of ballot secrecy using the applied pi calculus. Furthermore, we present similar vulnerabilities in other electronic voting protocols --namely, the schemes by Lee et al., Sako and Kilian and Schoenmakers --which do not assure ballot independence. Finally, we argue that independence and privacy properties are unrelated, and non-malleability is stronger than independence.
---
paper_title: A Method for Verifying Privacy-Type Properties: The Unbounded Case

paper_content:

In this paper, we consider the problem of verifying anonymity and unlinkability in the symbolic model, where protocols are represented as processes in a variant of the applied pi calculus notably used in the ProVerif tool. Existing tools and techniques do not allow one to verify directly these properties, expressed as behavioral equivalences. We propose a different approach: we design two conditions on protocols which are sufficient to ensure anonymity and unlinkability, and which can then be effectively checked automatically using ProVerif. Our two conditions correspond to two broad classes of attacks on unlinkability, corresponding to data and control-flow leaks. This theoretical result is general enough to apply to a wide class of protocols. In particular, we apply our techniques to provide the first formal security proof of the BAC protocol (e-passport). Our work has also lead to the discovery of new attacks, including one on the LAK protocol (RFID authentication) which was previously claimed to be unlinkable (in a weak sense) and one on the PACE protocol (e-passport).
---
paper_title: Formal Verification of Privacy for RFID Systems

paper_content:

RFID tags are being widely employed in a variety of applications, ranging from barcode replacement to electronic passports. Their extensive use, however, in combination with their wireless nature, introduces privacy concerns as a tag could leak information about the owner’s behaviour. In this paper we define two privacy notions, unlinkability and forward privacy, using a formal model based on the applied pi calculus, and we show the relationship between them. Then we focus on a generic class of simple privacy protocols, giving sufficient and necessary conditions for unlinkability and forward privacy for this class. These conditions are based on the concept of frame independence that we develop in this paper. Finally, we apply our techniques to two identification protocols, formally proving their privacy guarantees.
---
paper_title: Attacking and fixing Helios: An analysis of ballot secrecy

paper_content:

Helios 2.0 is an open-source web-based end-to-end verifiable electronic voting system, suitable for use in low-coercion environments. In this article, we analyse ballot secrecy in Helios and discover a vulnerability which allows an adversary to compromise the privacy of voters. The vulnerability exploits the absence of ballot independence in Helios and works by replaying a voter's ballot or a variant of it, the replayed ballot magnifies the voter's contribution to the election outcome and this magnification can be used to violated privacy. We demonstrate the practicality of the attack by violating a voter's privacy in a mock election using the software implementation of Helios. Moreover, the feasibility of an attack is considered in the context of French legislative elections and, based upon our findings, we believe it constitutes a real threat to ballot secrecy. We present a fix and show that our solution satisfies a formal definition of ballot secrecy using the applied pi calculus. Furthermore, we present similar vulnerabilities in other electronic voting protocols --namely, the schemes by Lee et al., Sako and Kilian and Schoenmakers --which do not assure ballot independence. Finally, we argue that independence and privacy properties are unrelated, and non-malleability is stronger than independence.
---
paper_title: Security protocols, constraint systems, and group theories

paper_content:

When formally analyzing security protocols it is often important to express properties in terms of an adversary's inability to distinguish two protocols. It has been shown that this problem amounts to deciding the equivalence of two constraint systems, i.e., whether they have the same set of solutions. In this paper we study this equivalence problem when cryptographic primitives are modeled using a group equational theory, a special case of monoidal equational theories. The results strongly rely on the isomorphism between group theories and rings. This allows us to reduce the problem under study to the problem of solving systems of equations over rings. We provide several new decidability and complexity results, notably for equational theories which have applications in security protocols, such as exclusive or and Abelian groups which may additionally admit a unary, homomorphic symbol.
---
paper_title: Algebraic Attacks on RFID Protocols

paper_content:

This work aims to identify the algebraic problems which enable many attacks on RFID protocols. Toward this goal, three emerging types of attacks on RFID protocols, concerning authentication, untraceability, and secrecy are discussed. We demonstrate the types of attacks by exhibiting previously unpublished vulnerabilities in several protocols and referring to various other flawed protocols. ::: ::: The common theme in these attacks is the fact that the algebraic properties of operators employed by the protocols are abused. While the methodology is applicable to any operator with algebraic properties, the protocols considered in this paper make use of xor , modular addition, and elliptic curve point addition.
---

Title: A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols

Section 1: Introduction
Description 1: This section gives an introductory overview of security protocols and the motivation behind establishing their security, contrasting the computational approach with the symbolic approach.

Section 2: What is a cryptographic protocol?
Description 2: This section explains the concept of cryptographic protocols and introduces standard cryptographic primitives, including symmetric and asymmetric encryption, digital signatures, and hash functions.

Section 3: An example: the BAC protocol
Description 3: This section provides details on the Basic Access Control (BAC) protocol used in e-passports and illustrates how it works, including key exchange mechanisms and its reliance on cryptographic primitives.

Section 4: Some logical attacks on the BAC protocol
Description 4: This section describes logical attacks on the BAC protocol, including authentication and unlinkability issues.

Section 5: A variety of security properties
Description 5: This section lists and describes various security properties that cryptographic protocols aim to ensure, such as secrecy, authentication, strong secrecy, anonymity, vote privacy, and unlinkability.

Section 6: Formalising protocols and properties
Description 6: This section covers the formal models used to describe cryptographic protocols and equivalence properties within the symbolic approach.

Section 7: Messages
Description 7: This section explores how messages are represented in symbolic models, including function symbols, equational theory, and rewriting systems.

Section 8: Assembling terms into frames
Description 8: This section discusses how sequences of messages and their order are organized into frames using a symbolic approach.

Section 9: Protocols
Description 9: This section describes how protocols are modeled through processes and the syntax and semantics of these processes.

Section 10: Equivalences
Description 10: This section explains the different notions of equivalence used to define indistinguishability between processes, including trace equivalence, labelled bisimilarity, and diff-equivalence.

Section 11: Methods and tools for verifying equivalence-based properties
Description 11: This section details the various methods and tools used in the symbolic approach to verify equivalence-based properties of cryptographic protocols, covering both bounded and unbounded session approaches.

Section 12: Conclusion
Description 12: This section summarizes the current state of research in the symbolic approach to establishing equivalence-based properties in cryptographic protocols and discusses potential future directions.