FCC on Tuesday, July 20th

09:00‑10:00 Invited Talk
Chair: Cédric Fournet
Location: AT 2.12
09:00 Dennis Hofheinz
Public key encryption schemes with special properties
10:30‑12:30 Computational Soundness
Location: AT 2.12
10:30 Catherine Meadows and Dusko Pavlovic
A Framework for Extending Algebraic to Computational Reasoning in Cryptographic Protocol Analysis

Most approaches to marrying formal verification techniques with computational models follow one of two paradigms. Either the computational model is used as a semantics for a higher-level algebraic (or “Dolev-Yao” model), which is analyzed using formal methods, or the formal tools are applied directly to the computational level. Here we present ongoing work on an alternative approach, in which one switches between high-level algebraic and low-level computational models as appropriate. This allows us to take advantage of the simplicity of the algebraic model when we can, but call upon the power of the computational model when needed.

11:00 Dominique Unruh
Computational Soundness of Hash Functions

We investigate the computational soundness of cryptographic (collision-resistant) hash functions. A more detailed abstract is attached as a PDF.

11:30 Steve Kremer, Hubert Comon-Lundh and Joe-Kai Tsay
Modular Soundness Proofs via Deduction Games (work in progress)

We report on a work in progress on a general security game which implies trace mapping. A notable advantage of our work is that we do not rely on parsing to prove our trace mapping. Therefore, it is for instance possible to show a mapping lemma for exclusive or in our framework. A long term objective of our work is to obtain combination techniques that would allow us to combine soundness results of distinct equational theories and obtain a soundness result for the combined theory.

12:00 Ralf Kuesters and Max Tuengerthal
Ideal Key Derivation and Encryption in Simulation-based Security

Many real-world protocols, such as SSL/TLS, SSH, IPsec, IEEE 802.11i, DNSSEC, and Kerberos, derive new keys from other keys. To be able to analyze such protocols in a composable way, in this paper we extend our ideal functionality for symmetric and public-key encryption proposed in previous work by a mechanism for key derivation. We also equip our functionality with message authentication codes (MACs) and ideal nonce generation. We show that our ideal functionality can be realized based on standard cryptographic assumptions and constructions, hence, providing a solid foundation for faithful, composable cryptographic analysis of real-world security protocols.

Based on our functionality, we identify sufficient criteria for protocols to provide universally composable key exchange and secure channels. Since these criteria are based on our ideal functionality, checking the criteria requires merely information-theoretic or even only syntactical arguments, rather than involved reduction arguments.

As a case study, we use our method to analyze two central protocols of the IEEE 802.11i standard, namely the 4-Way Handshake Protocol and the CCM Protocol, proving composable security properties. As to the best of our knowledge, this constitutes the first rigorous cryptographic analysis of these protocols.

14:00‑15:00 Automated Proofs
Chair: Ralf Kuesters
Location: AT 2.12
14:00 Gilles Barthe, Benjamin Gregoire, Daniel Hedin, Sylvain Heraud and Santiago Zanella Béguelin
Towards automating code-based game-based cryptographic proofs

CertiCrypt is a general framework built on top on the Coq proof assistant to certify the security of cryptographic primitives. It has been used to verify the exact security of encryption schemes such as OAEP and signature schemes such as FDH.

CertiCrypt adopts the code-based game-based paradigm of Bellare and Rogaway, in which the security statement, and the hypotheses under which it is proved, are expressed using probabilistic programs. Consequently, many proof steps involve establishing observational equivalence between two programs, or a relational Hoare statement. At present these statements are established formally using an equational theory for observational equivalence or a relational Hoare logic. The talk will report on using standard verification methods (generating verification conditions and sending them to an automatic tool) for establishing these statements automatically.

The long-term goal of this work is to increase the automation of CertiCrypt, to the point that the user can submit a proof sketch of a code-based game-based cryptographic proof, consisting of a sequence of games, and relational invariants, and that CertiCrypt can automatically complete the proof sketch.

14:30 Bruno Blanchet and David Pointcheval
The computational and decisional Diffie-Hellman assumptions in CryptoVerif

We present an extension of CryptoVerif to Diffie-Hellman key agreements. CryptoVerif~\cite{Blanchet07c} is a security protocol verifier sound in the computational model, which produces proofs by sequences of games. CryptoVerif provides a generic method for specifying security assumptions on primitives. However, this method did not support the Diffie-Hellman computational and decisional assumptions. We have extended it to support these assumptions. We apply this extension to a simple signed Diffie-Hellman protocol and to a variant of the password-based key exchange EKE. It also opens the possibility of verifying many important protocols in CryptoVerif (IPSec, SSH, and some modes of TLS and Kerberos).

15:30‑16:30 Protocol Logics
Chair: Dominique Unruh
Location: AT 2.12
15:30 Gergei Bana, Koji Hasebe and Mitsuhiro Okada
Secrecy-Oriended, Computationally Sound First-Order Logical Analysis of Cryptographic Protocols

We present a computationally sound first-order system for security-analysis of protocols that places secrecy of nonces and keys in its center. Even trace properties are proven via a non-trace property, namely, secrecy. As usual in a logical system, the desired security properties (secrecy, agreement and authentication) are derived directly from a set of computationally sound axioms. The system has a number of advantages:

- The proofs are very intuitive. We do not yet have automation, but even by hand the proofs are not too difficult. We have so far the Needham-Schroeder-Lowe protocol, the amended Needham-Schroeder shared key protocol and the Otway-Rees protocol, all for unbounded parallel sessions. - Computational soundness does not require any idealizations about parsing bitstrings or any tagging. To our knowledge, all other systems that are intended to be computationally sound, use (sometimes tacitly) idealized parsing properties for their soundness proofs. But, as others, we assume that the encryptions are CCA-2 secure. - The fact that key cycles may leak information is taken into account in a very simple way, without the need of talking about different levels of keys. - As far as we know, this system provides the first verifications for the above mentioned protocols that is computationally sound without the assumption of idealized parsing. Along the verification, we also found some parsing conditions that are necessary for the protocols to be correct.

In this system, the first thing to prove (inductively) is that no send action of the honest parties corrupt certain nonces and keys, and hence they remain uncorrupted. This is then used to show authentication and agreement.

An interesting aspect of this system is that for sound axioms, we need to formalize non-negligible subsets of traces, but a theorem tells us that proving certain properties (authentication, agreement and secrecy are such), we can omit these sets from the argument, and use unsound axioms, but the result will still be sound. In this talk, we would like to put special emphasis on this peculiarity.

16:00 Pedro Adao and Gergei Bana
Logical Proofs of Authentication Protocols and Type-Flaw Attacks

In this work we apply the logical system introduced by Bana et al. to the proof of authentication protocols, namely Needham-Schroeder-Lowe protocol, the amended Needham-Schroeder shared key protocol, and the Otway-Rees protocol. We have proven agreement and authentication properties of these protocols, up to their known weaknesses, for an unbounded number of sessions. The computational soundness of the logical system ensures us the soundness of the security results.

The security proof method is very intuitive and relies on the specification of a property expressing the uncorrupted nature of keys and nonces. We verify that for critical nonces and keys this property is an invariant, that is, no send action of honest agents corrupts them, and then derive the agreement and authentication properties of the protocol.

With this direct proof one does not need to show that the non existence of a symbolic adversary implies the non-existence of a computational adversary. This is implied by the fact that our logic only allows us to derive facts that are true in the computational model. Moreover, we do not need any condition on the parsing of terms.

We put particular emphasis on detection of type-flaw attacks with this proof system, and how adjustments of the axioms can reflect which type-flaw attacks can be \emph{a priori} excluded. All three protocols have weaknesses, and we show how during the course of the proof axioms that are necessary but not present in our system, as they are not necessarily sound, can be used to mount attacks against the protocol. Adding the missing axioms and the conditions in which they are sound allow us to show the security results.

For example, there is a known attack on NSL that relies on equating an arbitrary string $n$ paired with a principal name chosen by the adversary $Q$, that is, $\langle n,Q\rangle$, with a fresh value $N$. Without an axiom expressing $\overline{\langle n,Q\rangle}\neq N$, the NSL protocol is not possible to prove secure. This axiom may be added as long as we are certain \emph{a priori} that the two sides cannot be equal except with negligible probability. If agents match the length of the strings that they think are nonces received from others to a pre-specified nonce-length, then such equality is excluded and the axiom is necessarily sound.

We also discuss the extent to which the Otway-Rees protocol can be verified and how the known attacks to this protocol can be easily revealed in the course of the proof.