This workshop is co-organized by ANR Projects SCALP and PROSE.

### Program

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.

#### Abstract

- 9h15 -10h00
**Game-based Compositional Key-Exchange**by*Bogdan Warinschi*, Bristol UK.

#### Abstract

**10h00 - 10h15 Break.**

**10h15 - 12h30 Session 2 : **

- 10h15 - 11h00
**Towards unconditional soundness**by*Hubert Comon*, LSV ENS Cachan.

#### Abstract

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.

#### Abstract

- 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.

- 11h45 - 12h30
**Policy Auditing over Incomplete Logs**by*Anupam Datta*, CMU.

#### Abstract

**12h30 - 14h00 Lunch.**

**14h00 - 15h30 Session 3 :**

- 14h00 - 14h45
**Round-Optimal Privacy-Preserving Protocols with Smooth Projective Hash Functions**by*David Pointcheval*, LIENS ENS.

#### Abstract

- 14h45 - 15h30
**From indifferentiability to cyber-security : threats and needs**by*Emmanuel Bresson*, Emiraje Systems.

#### Abstract

**15h30 -15h45 Break.**

**15h45 - 16h55 Session 4 :**

- 15h45 - 16h20
**Probabilistic Relational Reasoning for Differential Privacy**by*Gilles Barthe*, IMDEA Spain.

#### Abstract

- 16h20 - 16h55
**Characterising Computational Entropy**by*Bruce Kapron*, University of Victoria.

#### Abstract

### Location

The workshop will take place at *VERIMAG Historic*