25 February 2015
Rémy Chrétien Download
Decidability of trace equivalence for protocols with nonces

Privacy properties such as anonymity, unlinkability, 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 nonces. Our class encompasses most symmetric key protocols of the literature, in their tagged variant.
11 March 2015
Stéphanie Delaune
Leakiness is decidable for well-founded protocols

Presentation of the paper "Leakiness is decidable for well-founded protocols" accepted at POST'15. Author: Sibylle Froschle.
1 April 2015
Ivan Gazeau Download
Providing transparent accountability for electronic currencies

Privacy is a core human need, but society sometimes has the requirement to do targeted, proportionate investigations in order to provide security. To reconcile individual privacy and societal security, we develop an electronic currency which simultaneously provides quantifiable privacy guarantees to citizens, and allows law enforcement agencies unfettered access to payment data in order to determine the income of any individual or organization. We prove both anonymity properties and accountability properties for the protocol, using a variant of labeled bisimulation in the applied pi calculus.
3 June 2015
Rémy Chrétien Download
Checking trace equivalence: How to get rid of nonces?

Security protocols can be successfully analysed using formal methods. When proving security in symbolic settings for an unbounded number of sessions, a typical technique consists in abstracting away fresh nonces and keys by a bounded set of constants. While this abstraction is clearly sound in the context of secrecy properties (for protocols without else branches), this is no longer the case for equivalence properties. In this paper, we study how to soundly get rid of nonces in the context of equivalence properties. We show that nonces can be replaced by constants provided that each nonce is associated to two constants (instead of typically one constant for secrecy properties). Our result holds for deterministic (simple) protocols and a large class of primitives that includes e.g. standard primitives, blind signatures, and zero-knowledge proofs.
17 June 2015
Lucca Hirschi Download
Sound Approach to Check Privacy Protection for an Unbounded Number of Sessions

In this talk I will present a new sound approach to check unlinkability and anonymity for an unbounded number of sessions. This is possible for a large class of 2-agents protocols without constraint on the term algebra. I indentify two sufficient conditions implying unlinkability and anonymity. Those two conditions are much easier to prove and, very often, ProVerif is able to check them automatically. This allows for the first proofs for several protocols (e.g., BAC+PA+AA, PACE+PA+AA, LAK, etc.).
8 July 2015
Antoine Dallon Download
Reducing the number of agents in equivalence properties

10 March 2016
Ivan Gazeau
Verification of privacy-type properties for security protocols with XOR

In symbolic verification of security protocols, process equivalences have recently been used extensively to model strong secrecy, anonymity and unlinkability properties. However, tool support for automated verification of equivalence properties is still restricted compared to trace properties, used for modeling authentication and weak notions of secrecy. In this paper, we present a novel procedure that allows to verify equivalence between finite processes, i.e., processes without replication, for protocols that use exclusive or (xor). We have implemented our procedure in the recent tool AKISS, and we have used it to check unlinkability on various RFID protocols. We obtain therefore the first tool that is able to effectively verify equivalence properties of protocols relying on various cryptographic primitives including xor.
14 April 2016
Ioana Boureanu
Automatic Verification of Security Protocols using Temporal Epistemic-Logics

Only few protocol-analysis formalisms lend themselves naturally to the specification and verification of security requirements hinging on privacy and anonymity properties, which are usually not expressible as trace properties. Since the general verification problem is undecidable, even the methodologies amenable to such formulations and analyses must operate modulo some limitations related to the set of cryptographic primitives/messages captured, the size of the models verified, the automation of the underlying methods, the abstraction modelled within, etc. In this talk, we will discuss formalisms based on temporal-epistemic logics which are suited for the specification and automatic verification of security protocols including against privacy-like requirements; we aim to recount the general hurdles, assumptions, advantages and disadvantages of this methodology.
12 May 2016
Antoine Dallon
Verifying protocols using SAT solvers

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