CosyProofs 2010
12-16 April 2010

Gilles Barthe Download Slides CertiCrypt: : Formal Proofs for Computational Cryptography As cryptographic proofs have become essentially unverifiable, cryptographers have argued in favor of developing techniques that help tame the complexity of their proofs. Game-based techniques provide a popular approach in which proofs are structured as sequences of games, and in which proof steps establish the validity of transitions between successive games. Code-based techniques form an instance of this approach that takes a code-centric view of games, and that relies on programming language theory to justify proof steps. While code-based techniques contribute to formalize the security statements precisely and to carry out proofs systematically, typical proofs are so long and involved that formal verification is necessary to achieve a high degree of confidence. Certicrypt is a framework that enables the machine-checked construction and verification of code-based proofs. The framework is built upon the general-purpose proof assistant Coq, and draws on many areas, including probability, complexity, algebra, and semantics of programming languages. Certicrypt provides certified tools to reason about the equivalence of probabilistic programs, including a relational Hoare logic, a theory of observational equivalence, verified program transformations, and specific game-based techniques such as reasoning about failure events and lazy sampling. The talk will present the main components of CertiCrypt and some of its applications. Joint work with Benjamin Gregoire, Daniel Hedin, Sylvain Heraud, Federico Olmedo and Santiago Zanella.

Ran Canetti Download Slides Using composability to speed up automated security proofs Rigorously asserting the security properties of today's software systems is a tremendous challenge: Manual analysis is out of the question for even modest size systems, and yet the complexity of automated security analysis grows extremely fast with the complexity of the analyzed system. A natural approach for scalable automated analysis is modularity: Partition the system to many small components, and analyze each component separately. However, when dealing with security properties, deducing the security of the overall system to from the security of the components is very tricky. This talk will review one way for using the concept of composable security to scaling up automated analysis. While some first steps along this path have been taken, much more remains to be explored.

Cédric Fournet Formal/computational verification of protocol implementations by typing Type systems are effective tools for verifying the security of cryptographic protocols and implementations. They provide automation, modularity and scalability, and have been applied to large protocols. In this tutorial, I present and illustrate types for authenticity and secrecy, first using symbolic models, then relying on computational assumptions: We introduce refinement types (that is, types carrying formulas to record invariants) for programs written in F# and verified by F7, an SMT-based type checker. We use types for declaring cryptographic invariants. We develop symbolic libraries for a range of cryptographic primitives, and we review a few case studies of protocol code. We adapt our libraries to rely on standard computational assumptions. For each primitive, computational soundness follows from a code-based game-hopping argument in F#. The tutorial is based on joint work with Karthik Bhargavan, Andy Gordon, and Aslan Askarov. Programming tools and examples are available here.

Steve Kremer Download Slides Computational Soundness of Symbolic Security Proofs We will start with a detailed overview of the seminal result of Abadi and Rogaway: (pattern) equivalence of sequences of symbolic terms implies computational indistinguishability of the distributions corresponding to the concrete implementation of the symbolic sequences. Then we will see a more general framework for soundness of static equivalence which is parametrised by an equational theory. These results were in the presence of a passive adversary. We will show how one can generalise the framework to consider a more powerfull, adaptive adversary. In particular in the presence of an adaptive adversary the problem of selective decommitment arises for symmetric encryption. Finally, if time permits, we briefly sketch a result for symmetric encryption in the active case introducing a trace mapping result and soundness of observational equivalence.

Yassine Lakhnech Download Slides Computational Indistinguishability Logic Computational Indistinguishability Logic (CIL) is a logic to reason about cryptographic primitives in computational models. It captures reasoning patterns that are common in provable security, such as simulations, reductions, and hybrid arguments. CIL is sound for the standard model, but also supports reasoning in the random oracle and other idealized models, using axiomatizations of the models as CIL statements.

Tatsuaki Okamoto Hierarchical Design and Security Proofs If a cryptographic system is highly functional, it is not easy to design the system and analyze its security. It is a natural strategy to design and analize such a complicated system in a modular way. In my talk, I will introduce a type of modular way of design and analysis, hierarchical design and security proof. In our approach, the underlying primitive is bilinear pairing groups, and a higher level of concept is constructed on the primitive, where a highly functional crypto system is directly designed over the higher level of concept. In addition, the security proof can be executed in a hierarchical manner, where the underlying assumption for the security proof is one of the simplest assumptions over the primitive, and higher level assumptions are reduced to the primitive assumption and the top level assumption over the higher level concept is directly employed to prove the security of the crypto system.

Phillip Rogaway Download Slides Reconciling Two Views of Cryptography A decade ago Martin Abadi and I wrote a paper entitled Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). In this talk I will look back on this old paper, reviewing how the result works and why we did it. I will then try to relate this to other work of mine that, almost by accident, likewise seems to straddle this symbolic/computational gap: cryptographic treatments for entity authentication and key distribution; constant-round secure function evaluation; and zero-knowledge proofs for all of IP.

Dominique Unruh Download Slides Composition of cryptographic protocols When designing large systems, one of the most important design principles is modularity: First, one designs and analyses small subsystems individually. Then one produces the overall system by composing the individual subsystems. When applying this principle to cryptographic protocols, a curious effect arises: Although each subsystem is secure individually, the composition of several subsystems can be insecure! In this tutorial, I show how and why the composition of cryptographic protocols can fail to be secure, and present modern techniques for ensuring secure composition, such as the Universal Composability framework.

À propos du LSV