FormaCrypt project: meeting January 16, 2007

ENS Cachan, conference room, Pavillon des Jardins (see access map and map of the campus)

11:00 Mathieu Baudet, PhD thesis defense, PhD thesis


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