18 March 2014
|
Stéphanie Delaune |
Download
Slides
|
| APTE: an automatic tool for verifying privacy-type security properties |
|
|
|
|
20 March 2014
|
Lucca Hirschi |
Download
Slides
|
| A reduced semantics for deciding trace
equivalence using constraint systems |
|
|
Many privacy-type properties of security protocols can be modeled
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.
I will show how to make use of Partial Order Redution techniques to
tackle this problem. I thus obtain an optimization in the form of a
reduced symbolic semantics that eliminates redundant interleavings on
the fly. I will also explain how to generalize this first result using
an informal analogy between focused proofs and compressed executions
of protocols.
|
|
1 April 2014
|
Lucca Hirschi |
Download
Slides
|
| A reduced semantics for deciding trace equivalence using
constraint systems |
|
|
Many privacy-type properties of security protocols can be modeled 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.
I will show how to make use of Partial Order Redution ideas to
tackle this problem. I thus obtain an optimization in the form of a
reduced symbolic semantics that eliminates redundant interleavings on
the fly.
|
|
16 April 2014
|
Rémy Chrétien |
Download
Slides
|
| Typing messages for free in security protocols: the case of equivalence properties
|
|
|
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.
Our first main contribution is to reduce the search space for
attacks. Specifically, we show that if
there is an attack then there is one that is well-typed. Our result
holds for a large class of typing systems and a large class of determinate security protocols.
Assuming finitely many nonces and keys,
we can derive from this result that trace equivalence is decidable for
an unbounded
number of sessions for a class of tagged protocols, yielding one of the first decidability results for the unbounded case.
As an intermediate result, we also provide a novel decision procedure in the case of a bounded number of sessions.
|
|
21 May 2014
|
Lucca Hirschi |
Download
Slides
|
| Partial order reduction for the applied pi-calculus |
|
|
Process algebras provide convenient languages for representing
concurrent computation, and they have successfully been used to
define the semantics of complex systems such as security protocols.
However, they do not constitute a good framework for analyzing concurrency
in the sense that their naive interleaving semantics gives rise to many
states that are essentially the same. This is problematic, for instance,
when model-checking security protocols. In this paper, we seek to
combine the nice framework provided by process algebras with truly
concurrent semantics. We do this by defining reduced transition systems that
are still adequate for on-the-fly model-checking of reachability and trace
equivalence properties. Our technique has strong connections with
focusing in proof theory and draws from basic trace theory, relying on a
careful analysis of sequential and data dependencies in process executions.
|
|
19 June 2014
|
Lucca Hirschi |
Download
Slides
|
| Partial order reduction for the applied pi-calculus |
|
|
Process algebras provide convenient languages for representing
concurrent computation, and they have successfully been used to
define the semantics of complex systems such as security protocols.
However, they do not constitute a good framework for analyzing concurrency
in the sense that their naive interleaving semantics gives rise to many
states that are essentially the same. This is problematic, for instance,
when model-checking security protocols. In this paper, we seek to combine
the nice framework provided by process algebras with truly concurrent
semantics. We do this by defining reduced transition systems that
are still adequate for on-the-fly model-checking of reachability and trace
equivalence properties. Our technique has strong connections with focusing
in proof theory and draws from basic trace theory, relying on a careful
analysis of sequential and data dependencies in process executions.
|
|
26 June 2014
|
Stéphanie Delaune |
Download
Slides
|
| Les protocoles cryptographiques: sommes-nous bien protégés ? |
|
|
|
|
2 July 2014
|
Lucca Hirschi |
Download
Slides
|
| Partial order reduction for the applied pi-calculus |
|
|
|
|
Page maintained by
Stéphanie Delaune.
Last modified:
1 January 1970.
