fr
14 January 2013
Rémy Chrétien
Trace equivalence of protocols for an unbounded number of sessions

Secure design of communication protocols in order to ensure the authen- tication of electronic agents or the safety of secret data is known to be difficult and fairly error-prone. Symbolic frameworks such as the Dolev-Yao model and later various process algebra have proven themselves valuable for finding attacks and assessing the security of these protocols. Several tools have thus been developed to answer the need of automated verification: ProVerif, AVISPA and Scyther rely on various formal methods to prove that a range of security properties holds in protocols. The problem of deciding reachability for cryptographic protocols has been thoroughly studied for an unbounded number of sessions and proven to be undecidable in general. Nevertheless some fragments were shown to be decidable, either by tagging or by restricting the number of blind-copies. On the other hand, trace equivalence has only been proven to be decidable for a bounded number of sessions. The objective of this talk is to provide the first results of decidability of trace equivalence for an unbounded number of sessions. Trace equivalence for a first class of protocols was shown undecidable under scarce restrictions one variable and symmetric encryption are indeed enough. Consequently, we restrained our class of protocols a step further by making the protocols deterministic in some sense and preventing it from disclosing secret keys. This tighter class of protocols was then shown to be decidable after reduction to an equivalence between deterministic pushdown automata.
29 January 2013
Géraud Sénizergues
lAlBlC: a program testing the equivalence of dpda's

We present a preliminary version of the program "lAlBlC" (i.e. lA=lB? let us Compute). The equivalence problem for dpda consists in deciding, for two given deterministic pushdown automata A,B, whether they recognize the same language. It was proved in [TCS 2001, G.S.] that this problem is decidable by means of some complete proof systems. The program lAlBlC gives, in some sense, life to the above completeness proof: on an input A,B, the program computes either a proof of their equivalence (w.r.t. to the system D5 of the above reference) or it computes a witness of their non-equivalence (i.e. a word that belongs to the symmetric difference of the two languages). We shall outline the main mathematical objects that are manipulated as well as the main functions performed over these objects. We shall emphasize the functionnal style of the most abstract part of the program (synthesis of strategies from a sequence of tactics, computation of a tactics from a sequence of functions) as well as the algebraic structure that the basic objects are implementing: the groupoid of deterministic rational matrices over some structured alphabet. We shall also explain the experimental results obtained so far (size of dpda's or grammars treated up to now, time and space of the computations, size of the proofs). The talk is based on an ongoing, joint, work with P. Henry.
20 February 2013
David Baelde Download
Slides
AKISS modulo AC

Akiss is a tool that (roughly) checks trace equivalence for applied-pi-calculus processes. It can notably be used to verify anonymity and untracability of security protocols modelled in that setting. Akiss is not restricted to a fixed set of crypto primitives but can work with any theory as long as it admits finite variants. This assumption precludes associative-commutative symbols, which would be necessary to model exclusive or or exponentiation, two primitives frequently used in protocols. In this talk, I will present an ongoing work towards extending Akiss to support AC symbols: some new ideas have allowed us to extend the tool to bring a few successes, though our procedure remains quite slow and fragile. This is work with Stéphanie Delaune and Steve Kremer. The initial work on Akiss is by Stefan Ciobaca, Chadha and Kremer.
6 March 2013
Steve Kremer
Practical everlasting privacy

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. Joint work with Myrto Arapinis, Véronique Cortier and Mark Ryan.
15 Mai 2013
Lucca Hirschi Download
Slides
Différentiation pour l'équivalence de traces

12 Juin 2013
Stéphanie Delaune Download
Slides
Composition issues: from protocols to applications

Security protocols are nowadays used in many of our daily-life applications, and our privacy largely depends on their design. Formal verification techniques have proved their usefulness to analyse these protocols, but they become so complex that modular techniques have to be developed. We propose a generic composition result (in a Dolev-Yao model) to compose protocols with respect to privacy-type properties expressed using a notion of equivalence. We consider arbitrary primitives modeled using an equational theory, and a rich process algebra close to the applied pi calculus. Relying on this generic composition result, we are then able to derive some privacy-type properties (e.g. anonymity, unlinkability) of a whole application from a privacy analysis performed on each sub-protocol individually. As an application, we consider parallel composition and the case of key-exchange protocols. We illustrate our techniques on the mobile telecommunications application.
17 Juin 2013
Rémy Chrétien Download
Slides
Trace equivalence of protocols for an unbounded number of sessions

Formal methods have been very successful in analyzing security protocols 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 unbounded number of sessions. Since replication leads very quickly to undecidability (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 fragment 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 obtained through a characterization of equivalence of protocols in terms of equality of languages of (generalized, real-time) deterministic pushdown automata.
2 Juillet 2013
Lucca Hirschi Download
Slides
Différentiation pour l'équivalence de traces

Ce groupe de travail a permis d'échanger nos points de vue avec plusieurs membres de l'axe MEXICO. La thématique de réduction d'entrelacements n'étant pas spécifique à la vérification de protocoles de sécurité, nous pouvons ainsi bénéficier de l'expertise d'autres membres du laboratoire sur ce sujet.
10 Juillet 2013
David Baelde
Equivalence of security protocols with AC primitives





Page maintained by
Stéphanie Delaune.
Last modified: 1 January 1970.
Valid HTML 4.01! Valid CSS!