This workshop is co-organized by ANR Projects SCALP and PROSE.
Workshop on Computed-Aided Security
8h15 - 8h30 Welcome.
8h30 - 10h00 Session 1 :
- 8h30 -9h15 Automated verification of equivalence properties of cryptographic protocols by Steve Kremer, LORIA Nancy.
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
- 9h15 -10h00 Game-based Compositional Key-Exchange by Bogdan Warinschi, Bristol UK.
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
10h00 - 10h15 Break.
10h15 - 12h30 Session 2 :
- 10h15 - 11h00 Towards unconditional soundness by Hubert Comon, LSV ENS Cachan.
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
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.
- 11h00 - 11h45 Automatically Verified Mechanized Proof of One-Encryption Key Exchange by Bruno Blanchet, LIENS ENS.
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
- 11h45 - 12h30 Policy Auditing over Incomplete Logs by Anupam Datta, CMU.
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.
12h30 - 14h00 Lunch.
14h00 - 15h30 Session 3 :
- 14h00 - 14h45 Round-Optimal Privacy-Preserving Protocols with Smooth
Projective Hash Functions by David Pointcheval, LIENS ENS.
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
- 14h45 - 15h30 From indifferentiability to cyber-security : threats and needs by Emmanuel Bresson, Emiraje Systems.
15h30 -15h45 Break.
15h45 - 16h55 Session 4 :
- 15h45 - 16h20 Probabilistic Relational Reasoning for Differential Privacy by Gilles Barthe, IMDEA Spain.
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
- 16h20 - 16h55 Characterising Computational Entropy by Bruce Kapron, University of Victoria.
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.
The workshop will take place at VERIMAG Historic