25 February 2015
|
Rémy Chrétien |
Download
Slides
|
| 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
Slides
|
| 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
Slides
|
| 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
Slides
|
| 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
Slides
|
| 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.
