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:
- We present a (stateless) symmetric encryption scheme that is
information-theoretically secure in face of a bounded number and
length of encryptions for which the messages depend in an arbitrary
way on the secret key.
- We present a stateful symmetric encryption scheme that is
computationally secure in face of an arbitrary number of
encryptions for which the messages depend only on the respective
current secret state/key of the scheme. The underlying
computational assumption is minimal: we assume the existence of
one-way functions.
- We give evidence that the only previously known KDM secure
encryption scheme cannot be proven secure in the standard model
(i.e., without random oracles).
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