CAS 2012, January 13, Grenoble

Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance to offline guessing attacks, and can be conveniently modeled using process equivalences. We present a novel procedure to verify equivalence properties for bounded number of sessions. Our protocol specification language is parametrized by a first-order term signature and a rewrite system which allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify observational equivalence for determinate cryptographic protocols. When protocols are not determinate our procedure can be used for both under- and over-approximations, which proved successive on examples. The procedure can handle a large set of cryptographic primitives, namely those which can be modeled by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modeling of traces in Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. Although, we were unable to prove termination of the resolution procedure, the procedure has been implemented in a prototype tool and has been effectively tested on examples some of which were outside the scope of existing tools, including checking anonymity of an electronic voting protocol.

In this talk I will describe two approaches towards modular security proofs for the composition of key exchange protocols with arbitrary other cryptographic tasks. While the two approaches differ in their scope and applicability they both rely on a novel framework for based entirely on cryptographic games and avoids the idiosyncrasies of universal composability. If time permits, I will discuss an application to proving the security of the Transport Layer Security protocol.

Formal security proofs require a formal model. Once a proof is completed, it is a proof in this particular model. How confident can we be that there would be no attack if we had modeled the problem differently ? The *computational soundness* results try to answer this question, showing that a model, in which the proof is carried, captures all possible lower level attacks. The computational soundness results are however hard and make a lot of more or less realistic assumptions (for instance an attacker is not allowed to forge his own keys). In this work, we develop another approach, in which we symbolically state what we know of all possible computations (for instance, a ciphertext cannot be confused with a pair) and let an attacker do anything that does not contradict the assumptions. This method has several advantages:

1) If we manage to prove security, then we are sure that there is no attack, whatever model is considered

2) Formal assumptions can be iteratively enriched, in order to rule out the attacks, yielding a minimal set of properties that suffices for the security

3) We do not have to assume the absence of key-cycles, the absence of dynamic corruption etc.

4) The assumptions that allow to derive the security are all formally stated in first-order logic.

Joint work with G. Bana.

We present a mechanized proof of the password-based protocol One-Encryption Key Exchange (OEKE) using the computationally-sound protocol prover CryptoVerif. OEKE is a nontrivial protocol, and thus mechanizing its proof provides additional confidence that it is correct. This case study was also an opportunity to implement several important extensions of CryptoVerif, which are useful for proving many other protocols:

* support for the computational Diffie-Hellman assumption.

* support for proofs that rely on Shoup’s lemma.

* additional game transformations. In particular, it is now possible to insert case distinctions manually and to merge cases that no longer need to be distinguished.

* improvements in the computation of the probability bounds for attacks, providing better reductions. In particular, we improve over the standard computation of probabilities when Shoup’s lemma is used and when secrecy is proved, which allows us to improve the bound given in a previous manual proof of OEKE, and to show that the adversary can test at most one password per session of the protocol.

We present these extensions, with their application to the proof of OEKE. All steps, both automatic and manually guided, are verified by CryptoVerif.

We present the design, implementation and evaluation of an algorithm that checks audit logs for compliance with privacy and security policies. The algorithm, which we name reduce, addresses two fundamental challenges in compliance checking that arise in practice. First, in order to be applicable to realistic policies, reduce operates on policies expressed in a first-order logic that allows restricted quantification over infinite domains. We build on ideas from logic programming to identify the restricted form of quantified formulas. The resulting logic is more expressive than prior logics used for compliance-checking, including propositional temporal logics and metric first-order temporal logic, and, in contrast to these logics, can express all 84 disclosure-related clauses in the HIPAA Privacy Rule. Second, since audit logs are inherently incomplete (they may not contain sufficient information to determine whether a policy is violated or not), reduce proceeds iteratively: in each iteration, it provably checks as much of the policy as possible over the current log and outputs a residual policy that can only be checked when the log is extended with additional information. We prove correctness, termination, time and space complexity results for reduce.We implement reduce and evaluate it by checking simulated audit logs for compliance with the HIPAA Privacy Rule. Our experimental results demonstrate that the algorithm is fast enough to be used in practice.

In 2008, Groth and Sahai proposed a powerful suite of techniques for constructing non-interactive zero-knowledge proofs in bilinear groups. Since their introduction, their proof systems have found numerous applications, including group signature schemes, anonymous voting, and anonymous credentials. In this talk, we demonstrate that the notion of smooth projective hash functions —proposed by Cramer and Shoup in 2002, and later extended by Gennaro and Lindell in 2003— can be useful to design round-optimal privacy-preserving interactive protocols. We show that this approach is suitable for designing schemes that rely on standard security assumptions in the standard model with a common-reference string and are more efficient than those obtained using the Groth-Sahai methodology. As an illustration of our design principle, we construct an efficient oblivious signature-based envelope scheme and a blind signature scheme, both round-optimal. Joint work with Olivier Blazy and Damien Vergnaud

TBA

Differential privacy is a notion of confidentiality that protects the privacy of individuals while allowing useful computations on their private data. Deriving differential privacy guarantees for real programs is a difficult and error-prone task that calls for principled approaches and tool support. Approaches based on linear types and static analysis have recently emerged; however, an increasing number of programs achieve privacy using techniques that cannot be analyzed by these approaches. Examples include programs that aim for weaker, approximate differential privacy guarantees, programs that use the Exponential mechanism, and randomized programs that achieve differential privacy without using any standard mechanism. Providing support for reasoning about the privacy of such programs has been an open problem.We report on CertiPriv, a machine-checked framework for reasoning about differential privacy built on top of the Coq proof assistant. The central component of CertiPriv is a quantitative extension of a probabilistic relational Hoare logic that enables to derive differential privacy guarantees for programs from first principles. We demonstrate the expressiveness of CertiPriv using a number of examples whose formal analysis is out of the reach of previous techniques. In particular, we prove (rather than assume) the correctness of the Laplacian and Exponential mechanisms and analyze the privacy of randomized and streaming algorithms from the recent literature.

Shannon’s entropy, and related notions of randomness, have played an important role in areas including data communication, cryptography, statistics and economics. An appealing aspect of information-theoretic entropy is that it enjoys a variety of equivalent characterisations which are relevant to particular application areas. The study of computational entropy was initiated by Yao in 1982. Since then, various notions of computational entropy have found application in complexity theory and cryptography, particularly with respect to the theory of pseudorandomness. Unlike the information-theoretic setting, the relationship between differing notions of computational entropy largely remains open. In this talk we will review the various notions of computational entropy and what is known about their relationships. We also propose a new notion of computational entropy related to Kelly’s characterisation of mutual information and discuss how it is related to some recent results in the theory of pseudorandom generators.