FormaCrypt project: meeting November 30, 2007

ENS, Amphithéâtre Galois, Nouvel Immeuble Rataud (see access map and map of the campus; the building is marked "Pavillon" on this map)

10:15 - 10:30 Welcome

10:30 - 11:00 Dennis Hofheinz: Towards Key-Dependent Message Security in the Standard Model (joint work with Dominique Unruh) slides

Standard security notions for encryption schemes do not guarantee any security if the encrypted messages depend on the secret key. Yet it is exactly the stronger notion of security in the presence of key-dependent messages (KDM security) that is required in a number of applications: most prominently, KDM security plays an important role in analyzing cryptographic multi-party protocols in a formal calculus. But although often assumed, the mere existence of KDM secure schemes is an open problem. The only previously known construction was proven secure in the random oracle model.

We present symmetric encryption schemes that are KDM secure in the standard model (i.e., without random oracles). The price we pay is that we achieve only a relaxed (but still useful) notion of key-dependent message security. Our work answers (at least partially) an open problem posed by Black, Rogaway, and Shrimpton. More concretely, our contributions are as follows:

11:00 - 11:30 Max Tuengerthal: Joint State Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation (joint work with Ralf Küsters) slides

Composition theorems proved within simulation-based approaches allow to build complex protocols from sub-protocols in a modular way. However, as first pointed out and studied by Canetti and Rabin, this modular approach often leads to impractical implementations. For example, when using a functionality for digital signatures within a more complex protocol, parties have to generate new verification and signing keys for every session of the protocol. This motivates to generalize composition theorems to so-called joint state theorems, where different copies of a functionality may share some state, e.g., the same verification and signing keys.

In this talk, a joint state theorem is presented which is more general than the original theorem of Canetti and Rabin, for which several problems and limitations are pointed out. We apply our theorem to obtain joint state realizations for three functionalities: public-key encryption, replayable public-key encryption, and digital signatures. Unlike most other formulations, our functionalities model that ciphertexts and signatures are computed locally, rather than being provided by the adversary. To obtain the joint state realizations, the functionalities have to be designed carefully. Previous formulations are shown to be unsuitable. Our work is based on a recently proposed, rigorous model for simulation-based security by Kuesters, called the IITM model. Our definitions and results demonstrate the expressivity and simplicity of this model. For example, unlike Canetti's UC model, in the IITM model no explicit joint state operator needs to be defined and the joint state theorem follows immediately from the composition theorem of the IITM model.

11:30 - 12:00 Graham Steel: Formal Security Analysis of PKCS#11 slides

RSA PKCS#11 is a security API widely used in tamper-resistant devices such as smart cards, USB keys and Hardware Security Modules. It is known to have many security vulnerabilities if implemented naively. This talk will describe some recent work aimed at formally modelling different configurations of the API and analysing them for flaws. Cryptographic soundness of the analysis will be discussed.

12:00 - 14:00 Lunch

14:00 - 14:30 Steve Kremer: Composition of Password-based Protocols (joint work with Stéphanie Delaune and Mark Ryan) slides

We investigate the composition of protocols that share a common secret. This situation arises when users employ the same password on different services. More precisely we study whether resistance against guessing attacks composes when a same password is used. We model guessing attacks using a common definition based on static equivalence in a cryptographic process calculus close to the applied pi calculus. We show that resistance against guessing attacks composes in the presence of a passive attacker. However, composition does not preserve resistance against guessing attacks for an active attacker. We therefore propose a simple syntactic criterion under which we show this composition to hold. Finally, we present a protocol transformation that ensures this syntactic criterion and preserves resistance against guessing attacks.

14:30 - 15:00 Cédric Fournet: Cryptographically Sound Implementations for Typed Information-Flow Security (joint work with Tamara Resk) slides

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they can often be verified by typing. However, their enforcement in concrete systems involves delicate compilation issues.

We consider cryptographic enforcement mechanisms for imperative programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. In source programs, security depends on an abstract access-control policy for reading and writing the shared memory. In their implementations, shared memory is unprotected and security depends instead on encryption and signing.

We build a translation from well-typed source programs and policies to cryptographic implementations. To establish its correctness, we develop a type system for the target language. Our typing rules enforce a correct usage of cryptographic primitives against active adversaries; from an information-flow viewpoint, they capture controlled forms of robust declassification and endorsement. We show type soundness for a variant of the non-interference property, then show that our translation preserves typability.

We rely on concrete primitives and hypotheses for cryptography, stated in terms of probabilistic polynomial-time algorithms and games. We model these primitives as commands in our target language. Thus, we develop a uniform language-based model of security, ranging from computational non-interference for probabilistic programs down to standard cryptographic hypotheses.

15:00 - 15:30 Bogdan Warinschi: Non-malleable hash functions (joint work with Alexandra Boldyreba, David Cash, and Marc Fischlin) slides

Non-malleability is an interesting and useful property which ensures that a cryptographic protocol preserves the independence of the underlying values: given for example an encryption enc(m) of some unknown message m it should be hard to transform this ciphertext into one enc(m') of a related message m'. This notion has been studied extensively for primitives like encryption, commitments and zero-knowledge. Non-malleability of one-way functions and hash functions has surfaced as a crucial property in several recent results, however it has not undergone a comprehensive treatment so far. We initiate the study of non-malleable hash functions. We start with the design of an appropriate security definition that, perhaps surprisingly, is not a straightforward extension of existing notions for other primitives. We then show that non-malleability for hash functions can be achieved, via a construction that uses perfectly one-way hash functions and simulation-sound non-interactive zero-knowledge proofs of knowledge (NIZKPoK). We study the usefulness of our definition in cryptographic applications. We show that non-malleability is necessary and sufficient to securely replace random oracles in existing constructions, and that non-malleable hash function immediately give secure message authentication codes. We also discuss the complexity of non-malleable hash functions. Specifically, we show that such hash function imply perfect one-wayness and we give a black-box based separation of non-malleable hash functions from one-way permutations (which our construction bypasses due to the ``non-black-box'' NIZKPoK).

15:30 - 16:00 break

16:00 - 16:15 Véronique Cortier: Proving computational security using Avispa slides

Due to several recent results, it is now possible to deduce computational security of cryptographic protocols from proofs performed in symbolic models where messages are abstracted using terms. One of the advantage of the symbolic models is that proof can often be obtained automatically using tools. However, the symbolic models used in tools differ from the models used for linking symbolic models with computational ones. In particular, relating symbolic models with computational ones requires richer cryptographic primitives (explicit signatures, randomized encryption, ...)

We show how to transfer security properties from symbolic models to simpler ones. As a sub-result, the AVISPA platform can be used to obtain computational security guarantees for cryptographic protocols using the CryptoSec module.

16:15 - 16:45 Bruno Blanchet: Computationally Sound Analysis of Kerberos (joint work with Aaron D. Jaggard, Andre Scedrov, and Joe-Kay Tsay) slides

We present a computationally sound mechanized analysis of Kerberos 5, both with and without its public-key extension PKINIT. We prove authentication and key secrecy properties using the prover CryptoVerif, which works directly in the computational model; these are the first mechanical proofs of a full industrial protocol at the computational level. We also generalize the notion of key usability and use CryptoVerif to prove that this definition is satisfied by keys in Kerberos.

16:45 - 17:XX Discussion on theme 4 "Case studies and comparison of the various approaches" (and on other topics if any)

Page maintained by Bruno Blanchet