Verification of Indistinguishability Properties (VIP)

19 January 2012	Stéphanie Delaune	Download Slides
	Analysing routing protocols: four nodes topologies are sufficient

Routing protocols aim at establishing a route between nodes on a network. Secured versions of routing protocols have been proposed in order to provide more guarantees on the resulting routes. Formal methods have proved their usefulness when analysing standard security protocols such as confidentiality or authentication protocols. However, existing results and tools do not apply to routing protocols. This is due in particular to the fact that all possible topologies (infinitely many) have to be considered. In this paper, we propose a simple reduction result: when looking for attacks on properties such as the validity of the route, it is sufficient to consider topologies with only four nodes, resulting in a number of just five distinct topologies to consider. As an application, we analyse the SRP applied to DSR and the SDMSR protocols using the ProVerif tool.

23 February 2012	Vincent Cheval	Download Slides
	Proving More Observational Equivalences with ProVerif

This talk will describe work in progress on expanding the scope of the ProVerif tool in order to provide reasoning about further equivalences.

5 April 2012	Graham Steel	Download Slides
	Formal analysis of Yubikey and the YubiHSM

This talk will describe work in progress on the analysis of the Yubikey protocol (http://www.yubico.com) and the YubiHSM API (joint work with Loredana Vamanu and Robert Künnemann).

26 April 2012	Myrto Arapinis	Download Slides
	Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity

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.

3 Mai 2012	Rohit Chadha	Download Slides
	Automated verification of equivalence properties of cryptographic protocols

Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance to offline guessing attacks, and can be conveniently modeled using process equivalences. We present a novel procedure to verify equivalence properties for bounded number of sessions. 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 which can be modeled by an optimally reducing convergent rewrite system. Although, we were unable to prove its termination, it has been implemented in a prototype tool and has been effectively tested on examples, some of which were outside the scope of existing tools.

24 Mai 2012	Vincent Cheval
	Verifying privacy-type properties in a modular way

Formal methods have proved their usefulness for analysing the security of protocols. In this setting, privacy-type security properties (e.g. vote-privacy, anonymity, unlinkability) that play an important role in many modern applications are formalised using a notion of equivalence. In this paper, we study the notion of trace equivalence and we show how to establish such an equivalence relation in a modular way. It is well-known that composition works well when the processes do not share secrets. However, there is no result allowing us to compose processes that rely on some shared secrets such as long term keys. We show that composition works even when the processes share secrets provided that they satisfy some reasonable conditions. Our composition result allows us to prove various equivalence-based properties in a modular way, and works in a quite general setting. In particular, we consider arbitrary cryptographic primitives and processes that use non-trivial else branches. As an example, we consider the ICAO e-passport standard, and we show how the privacy guarantees of the whole application can be derived from the privacy guarantees of its sub-protocols.

11 Octobre 2012	Stéphanie Delaune	Download Slides
	Presentation of the VIP Project

The Internet is a large common space, accessible to everyone around the world. As in any public space, people should take appropriate precautions to protect themselves against fraudulent people and processes. It is therefore essential to obtain as much confidence as possible in the correctness of the applications that we use. Because security protocols are notoriously difficult to design and analyse, formal verification techniques are extremely important. Formal verification of security protocols has known significant success during the two last decades. The techniques have become mature and several tools for protocol verification are nowadays available. However, nearly all studies focus on trace-based security properties, and thus do not allow one to analyse privacy-type properties that play an important role in many modern applications.

7 Novembre 2012	Rémy Chrétien	Download Slides
	Trace equivalence of protocols for an unbounded number of sessions

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 equivalenc 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 by lifting the approach followed by Comon-Lundh and Cortier to trace equivalence. 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.

21 Novembre 2012	David Baelde	Download Slides
	An introduction to Bedwyr: logic programming for protocol verification

Bedwyr is a logic programming language that it particularly well suited for animating and model-checking syntax-driven specification, e.g. type systems, operational semantics, behavior equivalences. Roughly, it extends the traditional logic programming paradigm by performing proof search in a rich logic featuring fixed points and generic quantification. Bedwyr has been used to implement various algorithms, the most striking use of it being the spi-calculus bisimulation checker SPEC of Alwen Tiu. I will give a short introduction to the tool, highlighting and motivating its logical foundations, but also covering practical considerations relevant for Bedwyr programmers. Then, depending on the time and demand, I will cover a case study either in pi or spi calculus.

4 Décembre 2012	Alwen Tiu
	Towards Generating Compact Proof Certificates for Observational Equivalence

Observational equivalence, in the context of process calculi, is a notion of behavioral equivalence defined via observable actions of processes. It is commonly defined co-inductively using the transitions of the processes, and, more importantly, it needs to be closed under arbitrary process contexts. Due to the latter requirement, it is difficult to mechanise observational equivalence checking directly, and various methods for approximating observational equivalence have been proposed in the literature. In this talk I will consider an approximation of observational equivalence, for the spi-calculus, based on labelled bisimulation, and present a procedure for checking this notion of bisimulation. This procedure has been implemented in a logical framework called Bedwyr. As the procedure and its implementation are quite complex, to increase confidence in the result of the implemention, the prover (called SPEC) needs to produce an explicit proof object, in terms of a bisimulation set, that can be checked independently outside the prover. Initial experiments suggest that often such a set can be very large, even for simple processes. I will discuss several simplifications to reduce the size of the bisimulation set that are currently implemented in SPEC, exploiting the so-called 'bisimulation-up-to' techniques, originally developed by Milner, Sangiorgi and others for the pi-calculus. I will then discuss some directions for future work, in particular incorporating more general up-to techniques as logical theories in a logical framework.

Page maintained by Stéphanie Delaune.
Last modified: 1 January 1970.