FormaCrypt project: meeting January 16, 2007
ENS Cachan, conference room, Pavillon des Jardins
(see access map and
map of the campus)
Buffet
15-15:30 Invited talk: Ralf Küsters,
A Cryptographic Model for Branching Time Security Properties --- the
Case of Contract Signing Protocols (joint work with Véronique Cortier and
Bogdan Warinschi) slides
Some cryptographic tasks, such as contract signing and
other related tasks, need to ensure complex, branching time
security properties. When defining such properties one
needs to deal with subtle problems regarding the scheduling
of non-deterministic decisions, the delivery of messages
sent on resilient (non-adversarially controlled) channels,
fair executions (executions where no party, both honest and
dishonest, is unreasonably precluded to perform its
actions), and defining strategies of adversaries against
all possible non-deterministic choices of parties and
arbitrary delivery of messages via resilient
channels. These problems are typically not, or not all,
addressed in cryptographic models and these models
therefore do not suffice to formalize branching time
properties, such as those required of contract signing
protocols.
In this talk, a cryptographic model that deals with all of
the above problems is proposed. One central feature of this
model is a general definition of fair scheduling which not
only formalizes fair scheduling of resilient channels but
also fair scheduling of actions of honest and dishonest
principals. Based on this model and the notion of fair
scheduling, a definition of a prominent branching time
property of contract signing protocols, namely balance, is
provided, along with the first cryptographic proof that the
Asokan-Shoup-Waidner two-party contract signing protocol is
balanced. The cryptographic models and notions proprosed
here provide a basis for relating cryptographic and formal
definitions of branching time security properties.
15:30-16 Véronique Cortier,
How to protect security protocols against active attackers
(joint work with Bogdan Warinschi and Eugen Zalinescu)
slides
We introduce a generic transformation-based approach for the design of
verifiably secure protocols. The transformation maps a protocol that
is secure against a passive attacker that only observes the messages
exchanged in a single session of the protocol, into a protocol that is
secure against a fully active adversary in full control of the
communication between an unbounded number of protocol sessions. We
prove our results for standard formulations of secrecy and
authentication.
The transformation enables a paradigm for modular protocol development
where designers focus their effort on an extremely simple execution
setting -- security in more complex settings is enforced by our
generic transformation.
The transformation works for any protocol, with any number of
participants, written with usual cryptographic primitives. It
essentially consists in tying each message to the session for which it
is intended via appropriate digital signatures, and hiding the content
of the message under the recipient's public key in order to prevent
replay in other sessions.
16:00-16:30
Bruno Blanchet,
Computationally Sound Automatic Proofs of Correspondence Assertions
slides
We present a new automatic technique for proving correspondence
assertions for cryptographic protocols in the computational model.
Correspondence assertions are useful in particular for establishing
authentication.
Our technique produces proofs by sequences of games, as standard in
cryptography. These proofs are valid for a number of sessions
polynomial in the security parameter, in the presence of an active
adversary. Our technique can handle a wide variety of cryptographic
primitives, including shared- and public-key encryption, signatures,
message authentication codes, and hash functions. It has been
implemented in the tool CryptoVerif and successfully tested on
examples from the literature.
16:30-16:45
Short break
16:45-17:15 Laurent Mazaré,
Adaptive Security of Symbolic Encryption: the Case of Dynamic Corruptions
(joint work with Bogdan Warinschi)
slides
Adaptive security has been defined by Micciancio and Panjwani in 2005. This
work extends the classical computational soundness result from Abadi and
Rogaway to a scenario where the adversary adaptively chooses the sequence of
symbolic terms that he wants to observe, and still only relies on semantic
security of the encryption scheme. However this computational soundness result
suffers from a strong restriction: keys cannot be corrupted in a dynamic way.
In this work, we remove this restriction and allow all the possible forms of
corruptions. This result also solves partly the selective decryption problem
and extends in a non-trivial way to the case of nested encryptions as well as
key emission.
17:15-17:45
Steve Kremer, Adaptive soundness of static equivalence --- work in progress
(joint work with Laurent Mazaré) slides
We define a framework to reason about sound implementations of
equational theories in the presence of an adaptive adversary. In
particular, we focus on soundess of static equivalence. We illustrate
our framework on several equational theories: xor, symmetric encryption,
groups and also joint theories of encryption and groups as well as
encryption and xor. For both examples using joint theories we use a
proof technique that enables us to reuse proofs for the separate
theories. Finally, we define a model for symbolic analysis of dynamic
group key exchange protocols, which we show to be computationally sound.
17:45-18:15 Discussion.
Page maintained by Bruno Blanchet