The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

*** The Joint EasyCrypt-F*-CryptoVerif School ***

Dates: 24-28 November 2014
Place: INRIA office in Paris (23 Avenue d'Italie)
Registration deadline: 1 September
https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014

The school is aimed at teaching participants how to use three
state of the art security verification tools: EasyCrypt, F*, and
CryptoVerif, as well as give participants a glimpse of the
beautiful formal foundations behind these tools.

Participants will attend lectures and hands-on tutorials, under
the guidance of members from the tools' developer teams:
- EasyCrypt: Gilles Barthe, François Dupressoir, Benjamin Grégoire,
Benedikt Schmidt, Pierre-Yves Strub
- F*: Karthik Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet,
Cătălin Hriţcu, Chantal Keller, Alfredo Pironti, Pierre-Yves Strub
- CryptoVerif: Bruno Blanchet

There are no registration fees for participants, and we try to
offer grants covering the travel and/or accommodation costs of
the participants who need it. Registration open until 1 September:
https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014

EasyCrypt (https://www.easycrypt.info) is a toolset for reasoning
about relational properties of probabilistic computations with
adversarial code. Its main application is the construction and
verification of game-based cryptographic proofs. EasyCrypt was used to
prove the security of complex cryptographic constructions, including
the Cramer-Shoup encryption scheme, the Merkle-Damgaard iterative hash
function design, and the ZAEP encryption scheme. More recently, it has
been used for proving the security of protocols based on garbled
circuits, and for the proof of security for authenticated key-exchange
protocols and derived proofs under weaker assumptions.

F* (https://research.microsoft.com/en-us/projects/fstar/) is a new
ML-like functional programming language designed with program
verification in mind. It has a powerful refinement type-checker that
discharges verification conditions using the Z3 SMT solver. F* has
been successfully used to verify nearly 50,000 lines of code, ranging
from cryptographic protocol implementations to web browser extensions,
and from cloud-hosted web applications to key parts of the F* compiler
itself. The newest version on F* erases to both F# and OCaml, on which
it is based. It also compiles securely to JavaScript, enabling safe
interoperability with arbitrary, untrusted JavaScript libraries.

CryptoVerif (http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/)
is an automatic protocol prover sound in the computational model. It
can prove secrecy and correspondences (e.g. authentication). The
generated proofs are by sequences of games, as used by cryptographers.
CryptoVerif was successfully used for security proofs of FDH
signatures, Kerberos, OEKE, and the SSH transport layer protocol.

More details at:
https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014