Difference between revisions of "The Joint EasyCrypt-F*-CryptoVerif School 2014"

From prosecco
(Wednesday, November 26th 2014)
 
(12 intermediate revisions by the same user not shown)
Line 4: Line 4:
  
 
= Abstract =
 
= Abstract =
The school takes place 24-28 November in Paris and
+
The school takes place 24-28 November in Paris and
is aimed at teaching participants how to use three state-of-the-art security verification tools: [https://www.easycrypt.info EasyCrypt], [https://research.microsoft.com/en-us/projects/fstar/ F*], and [http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif], as well as give participants a glimpse of the formal foundations behind these tools.
+
is aimed at teaching participants how to use three state-of-the-art security verification tools: [https://www.easycrypt.info EasyCrypt], [https://www.fstar-lang.org F*], and [http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif], as well as give participants a glimpse of the formal foundations behind these tools.  
  
 
'''[https://www.easycrypt.info EasyCrypt]''' 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.
 
'''[https://www.easycrypt.info EasyCrypt]''' 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.
  
'''[https://research.microsoft.com/en-us/projects/fstar/ F*]''' 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 [https://github.com/FStarLang/FStar 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.
+
'''[https://www.fstar-lang.org F*]''' 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 [https://www.fstar-lang.org 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.
  
 
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove
 
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove
Line 22: Line 22:
 
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]]     
 
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]]     
 
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]
 
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]
 +
 +
= Report =
 +
 +
A [http://prosecco.gforge.inria.fr/personal/hritcu/publications/school2014-siglog.pdf report on the school] appeared in the
 +
[http://siglog.hosting.acm.org/?attachment_id=77 SIGLOG Newsletter, Volume 2, Number 1] from January 2015.
  
 
= Lecturers and tutorial aides =
 
= Lecturers and tutorial aides =
Line 29: Line 34:
 
* '''[https://www.easycrypt.info EasyCrypt]''': [http://software.imdea.org/people/gilles.barthe/ Gilles Barthe], [http://fdupress.net/ François Dupressoir], [http://www-sop.inria.fr/members/Benjamin.Gregoire/ Benjamin Grégoire], [http://www.software.imdea.org/people/benedikt.schmidt/index.html Benedikt Schmidt], [http://pierre-yves.strub.nu/ Pierre-Yves Strub]
 
* '''[https://www.easycrypt.info EasyCrypt]''': [http://software.imdea.org/people/gilles.barthe/ Gilles Barthe], [http://fdupress.net/ François Dupressoir], [http://www-sop.inria.fr/members/Benjamin.Gregoire/ Benjamin Grégoire], [http://www.software.imdea.org/people/benedikt.schmidt/index.html Benedikt Schmidt], [http://pierre-yves.strub.nu/ Pierre-Yves Strub]
  
* '''[https://research.microsoft.com/en-us/projects/fstar/ F*]''': [http://prosecco.gforge.inria.fr/personal/karthik/ Karthik Bhargavan], [http://antoine.delignat-lavaud.fr/ Antoine Delignat-Lavaud], [https://research.microsoft.com/en-us/um/people/fournet/ Cédric Fournet], [http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu], [http://prosecco.gforge.inria.fr/personal/ckeller/index-en.html Chantal Keller], [http://research.microsoft.com/en-us/people/markulf/ Markulf Kohlweiss], [http://www.cs.umd.edu/~aseem/ Aseem Rastogi], [http://pierre-yves.strub.nu/ Pierre-Yves Strub], [http://research.microsoft.com/en-us/people/nswamy/ Nikhil Swamy]
+
* '''[https://www.fstar-lang.org F*]''': [http://prosecco.gforge.inria.fr/personal/karthik/ Karthik Bhargavan], [http://antoine.delignat-lavaud.fr/ Antoine Delignat-Lavaud], [https://research.microsoft.com/en-us/um/people/fournet/ Cédric Fournet], [http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu], [http://prosecco.gforge.inria.fr/personal/ckeller/index-en.html Chantal Keller], [http://research.microsoft.com/en-us/people/markulf/ Markulf Kohlweiss], [http://www.cs.umd.edu/~aseem/ Aseem Rastogi], [http://pierre-yves.strub.nu/ Pierre-Yves Strub], [http://research.microsoft.com/en-us/people/nswamy/ Nikhil Swamy]
  
 
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''':  [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]
 
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''':  [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]
Line 38: Line 43:
 
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Unconditional Soundness
 
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Unconditional Soundness
 
* [http://www.loria.fr/~cortier/ Véronique Cortier] (CNRS & LORIA Nancy) - [https://wiki.inria.fr/prosecco/Abstracts_of_Invited_Talks_-_Joint_School_2014#Type-Based_Verification_of_Electronic_Voting_Protocols_.28V.C3.A9ronique_Cortier.2C_CNRS_.26_LORIA_Nancy.29 Type-Based Verification of Electronic Voting Protocols]
 
* [http://www.loria.fr/~cortier/ Véronique Cortier] (CNRS & LORIA Nancy) - [https://wiki.inria.fr/prosecco/Abstracts_of_Invited_Talks_-_Joint_School_2014#Type-Based_Verification_of_Electronic_Voting_Protocols_.28V.C3.A9ronique_Cortier.2C_CNRS_.26_LORIA_Nancy.29 Type-Based Verification of Electronic Voting Protocols]
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Affine Refinement Types for Secure Distributed Programming
+
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - [https://wiki.inria.fr/prosecco/Invited_Talks_-_Joint_School_2014#Logical_Foundations_of_Secure_Resource_Management_in_Protocol_Implementations_.28Matteo_Maffei.2C_Saarland_University.29 Logical Foundations of Secure Resource Management in Protocol Implementations]
 
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types
 
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types
  
Line 124: Line 129:
 
  |-
 
  |-
 
  | 09.15 - 10.15
 
  | 09.15 - 10.15
  | '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture4.pdf Theories, Cloning and Modules]
+
  | '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture4.pdf Theories, Cloning and Modules (François)]
 
  | rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]
 
  | rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]
 
  |-
 
  |-
Line 173: Line 178:
 
  |-
 
  |-
 
  | 10:15 - 10:45
 
  | 10:15 - 10:45
  | '''Véronique Cortier:''' [https://wiki.inria.fr/prosecco/Abstracts_of_Invited_Talks_-_Joint_School_2014#Type-Based_Verification_of_Electronic_Voting_Protocols_.28V.C3.A9ronique_Cortier.2C_CNRS_.26_LORIA_Nancy.29 Type-Based Verification of Electronic Voting Protocols] (Invited Talk)
+
  | '''Véronique Cortier:''' [https://wiki.inria.fr/prosecco/Abstracts_of_Invited_Talks_-_Joint_School_2014#Type-Based_Verification_of_Electronic_Voting_Protocols_.28V.C3.A9ronique_Cortier.2C_CNRS_.26_LORIA_Nancy.29 Type-Based Verification<br/> of Electronic Voting Protocols] (Invited Talk)
 
  |-
 
  |-
 
  | 10:45 - 11:15
 
  | 10:45 - 11:15
  | '''Matteo Maffei:''' Affine Refinement Types for Secure Distributed Programming (Invited Talk)
+
  | '''Matteo Maffei:''' [https://wiki.inria.fr/prosecco/Invited_Talks_-_Joint_School_2014#Logical_Foundations_of_Secure_Resource_Management_in_Protocol_Implementations_.28Matteo_Maffei.2C_Saarland_University.29 Logical Foundations of Secure Resource<br/> Management in Protocol Implementations] (Invited Talk)
 
  |-
 
  |-
 
  | 11:15 - 11:30
 
  | 11:15 - 11:30
Line 185: Line 190:
 
  |-
 
  |-
 
  | 12:00 - 12:30
 
  | 12:00 - 12:30
  | '''CryptoVerif lecture:''' [http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Wednesday.pdf sneak preview (Bruno)]
+
  | '''CryptoVerif lecture:''' [http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Wednesday.pdf sneak preview] (Bruno)
 
  |-
 
  |-
 
  | 12:30 - 14:30
 
  | 12:30 - 14:30
Line 207: Line 212:
 
  |-
 
  |-
 
  | 9:00 - 9:30
 
  | 9:00 - 9:30
  | [http://prosecco.gforge.inria.fr/tutorial.html#sec-state-and-other-effects '''F* lecture:''' Advanced F*] (Nikhil)
+
  | '''F* lecture:''' [http://prosecco.gforge.inria.fr/tutorial.html#sec-state-and-other-effects Advanced F*] (Nikhil)
 
  | rowspan="6" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]
 
  | rowspan="6" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]
 
  |-
 
  |-
 
  | 9:30 - 10:00
 
  | 9:30 - 10:00
  | '''F* lecture:''' miTLS (Antoine)
+
  | '''F* lecture:''' [https://wiki.inria.fr/wikis/prosecco/images/2/28/Mitls.pdf miTLS] (Antoine)
 
  |-
 
  |-
 
  | 10:00 - 10:15
 
  | 10:00 - 10:15
Line 217: Line 222:
 
  |-
 
  |-
 
  | 10:15 - 11:15
 
  | 10:15 - 11:15
  | '''F* lecture:''' Types for Modular Cryptography (Cedric)
+
  | '''F* lecture:''' [https://wiki.inria.fr/wikis/prosecco/images/8/86/CryptoTyping.pdf Types for Modular Cryptography] (Cedric)
 
  |-
 
  |-
 
  | 11:15 - 11:30
 
  | 11:15 - 11:30
Line 223: Line 228:
 
  |-
 
  |-
 
  | 11:30 - 12:30
 
  | 11:30 - 12:30
  | '''F* lecture:''' Types for Modular Cryptography (Cedric)
+
  | '''F* lecture:''' [https://wiki.inria.fr/wikis/prosecco/images/8/86/CryptoTyping.pdf Types for Modular Cryptography] (Cedric)
 
  |-
 
  |-
 
  | 12:30 - 14:30
 
  | 12:30 - 14:30
Line 229: Line 234:
 
  |-
 
  |-
 
  | 14:30 - 16:30
 
  | 14:30 - 16:30
  | [http://prosecco.gforge.inria.fr/tutorial.html#sec-security-examples '''F* tutorial:''' Verifying Simple Cryptography] (Cedric, Markulf, Nikhil)
+
  | '''F* tutorial:''' [http://prosecco.gforge.inria.fr/tutorial.html#sec-security-examples Verifying Simple Cryptography] (Cedric, Markulf, Nikhil)
 
  | rowspan="3" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)
 
  | rowspan="3" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)
 
  |-
 
  |-
Line 236: Line 241:
 
  |-
 
  |-
 
  | 17.00 - 18:00
 
  | 17.00 - 18:00
  | [http://prosecco.gforge.inria.fr/tutorial.html#sec-case-study--simply-typed-lambda-calculus '''F* tutorial:''' Simply Typed Lambda Calculus] (Catalin, Chantal)
+
  | '''F* tutorial:''' [http://prosecco.gforge.inria.fr/tutorial.html#sec-case-study--simply-typed-lambda-calculus Simply Typed Lambda Calculus] (Catalin, Chantal)
 
  |}
 
  |}
  
Line 285: Line 290:
  
 
= Hardware and software =
 
= Hardware and software =
Roughly half of the time of the school is devoted to hands-on exercise sessions and tutorials. Participants are expected to bring their own laptop with [https://www.easycrypt.info EasyCrypt], [https://research.microsoft.com/en-us/projects/fstar/ F*], and [http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif] installed. More details e.g. about precise versions and setup will be communicated on the participants' mailing list.
+
Roughly half of the time of the school is devoted to hands-on exercise sessions and tutorials. Participants are expected to bring their own laptop with [https://www.easycrypt.info EasyCrypt], [https://www.fstar-lang.org F*], and [http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif] installed. More details e.g. about precise versions and setup will be communicated on the participants' mailing list.
 
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]
 
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]
 
* [https://www.easycrypt.info/trac/wiki/SchoolParis14Install EasyCrypt Installation Instructions]
 
* [https://www.easycrypt.info/trac/wiki/SchoolParis14Install EasyCrypt Installation Instructions]
Line 309: Line 314:
  
 
= Travel, food, and accommodation =
 
= Travel, food, and accommodation =
Participants are expected to make their own travel, food, and accommodation arrangements. Paris offers many good alternatives. The only exceptions are for invited speakers, for the shared hotel rooms (financial support), and for the social dinner (see above).
+
Participants are expected to make their own travel, food, and accommodation arrangements. Paris offers many great alternatives. The only exceptions are for invited speakers, for the shared hotel rooms (financial support), and for the social dinner (see above).
  
 
= Sponsors =
 
= Sponsors =

Latest revision as of 18:27, 17 February 2019

Abstract

The school takes place 24-28 November in Paris and 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 formal foundations behind these tools.

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

The presented tools have been developed at

CNRS        ENS        IMDEA      INRIA    Microsoft Research      Microsoft Research Inria Joint Centre

Report

A report on the school appeared in the SIGLOG Newsletter, Volume 2, Number 1 from January 2015.

Lecturers and tutorial aides

Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:

Invited speakers

While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited talks, a longer one Wednesday morning and a short one Friday morning.

Organization

Anna Bednarik, Karthikeyan Bhargavan, Cătălin Hriţcu (contact), Pierre-Yves Strub

Student volunteers: Evmorfia-Iro Bartzia, Benjamin Beurdouche, Antoine Delignat-Lavaud, and Jean Karim Zinzindohoué

Materials

Registration

  • The school has filled up completely, we have no space for additional participants.

Locations

We have two locations:

Schedule

Monday, November 24th 2014

Time Maison Internationale, Cite Universitaire Room
09.15 - 10.15 EasyCrypt lecture - Introduction (Gilles) Salon David Weill
10.15 - 10.30 break
10.30 - 11.30 EasyCrypt lecture - An introduction to EasyCrypt (Benjamin)
11.30 - 11.45 break
11.45 - 12.45 EasyCrypt lecture - Proving in EasyCrypt and pRHL in practice (Pierre-Yves)
12.45 - 14.15 lunch Restaurant Universitaire
14.15 - 15.45 EasyCrypt tutorial - Exercices Salon David Weill
+ Salle Orange at INRIA
   (25 minutes walk)
15.45 - 16.15 break
16.00 - 17.30 EasyCrypt tutorial

Tuesday, November 25th 2014

Time Maison Internationale, Cite Universitaire Room
09.15 - 10.15 EasyCrypt lecture - Theories, Cloning and Modules (François) Salon David Weill
10.15 - 10.30 break
10.30 - 11.30 EasyCrypt lecture - High-level Proof Principles (Benedikt)
11.30 - 11.45 break
11.45 - 12.45 EasyCrypt lecture - Overview and perspectives (Gilles)
12.45 - 14.15 lunch Restaurant Universitaire
14.15 - 15.45 EasyCrypt tutorial - Exercices Salon David Weill
+ Salle Orange at INRIA
   (25 minutes walk)
15.45 - 16.15 break
16.00 - 17.30 EasyCrypt tutorial
18.00 - 20:00 Cryptosense Reception Le Vin Qui Danse, Gobelins
(25 minutes walk from CiteU)

Wednesday, November 26th 2014

Time UPMC - Campus des Cordeliers Room
09:00 - 10:00 F* lecture: High-level introduction (Nikhil) Amphitheatre Gustave Roussy
10:00 - 10:15 short break
10:15 - 10:45 Véronique Cortier: Type-Based Verification
of Electronic Voting Protocols
(Invited Talk)
10:45 - 11:15 Matteo Maffei: Logical Foundations of Secure Resource
Management in Protocol Implementations
(Invited Talk)
11:15 - 11:30 short break
11:30 - 12:00 Hubert Comon: Unconditional Soundness (Invited Talk)
12:00 - 12:30 CryptoVerif lecture: sneak preview (Bruno)
12:30 - 14:30 lunch break
14.30 - 19:00 F* tutorial: Basic F* Amphitheatre Gustave Roussy
+ Room Déjerine (35 people)
19:00 - 21:00 Social dinner Bouillon Racine (2 minutes walk)

Thursday, November 27th 2014

Time UPMC - Campus des Cordeliers Room
9:00 - 9:30 F* lecture: Advanced F* (Nikhil) Amphitheatre Gustave Roussy
9:30 - 10:00 F* lecture: miTLS (Antoine)
10:00 - 10:15 short break
10:15 - 11:15 F* lecture: Types for Modular Cryptography (Cedric)
11:15 - 11:30 short break
11:30 - 12:30 F* lecture: Types for Modular Cryptography (Cedric)
12:30 - 14:30 lunch break
14:30 - 16:30 F* tutorial: Verifying Simple Cryptography (Cedric, Markulf, Nikhil) Rooms Déjerine and Leroux
(35 people each)
16:30 - 17:00 break
17.00 - 18:00 F* tutorial: Simply Typed Lambda Calculus (Catalin, Chantal)

Friday, November 28th 2014

Time Maison Internationale, Cite Universitaire Room
09:00 - 10:30 CryptoVerif lecture (Bruno) Salon Salon David Weill
10:30 - 11:00 break
11:00 - 12:30 CryptoVerif lecture (Bruno)
13:00 - 14:30 lunch break Restaurant Universitaire
14:30 - 16:00 CryptoVerif tutorial Salon Salon David Weill
16:00 - 16:30 break
16.30 - 18:00 CryptoVerif tutorial

Photos

Download

Hardware and software

Roughly half of the time of the school is devoted to hands-on exercise sessions and tutorials. Participants are expected to bring their own laptop with EasyCrypt, F*, and CryptoVerif installed. More details e.g. about precise versions and setup will be communicated on the participants' mailing list.

Social dinner

Cryptosense reception

Travel, food, and accommodation

Participants are expected to make their own travel, food, and accommodation arrangements. Paris offers many great alternatives. The only exceptions are for invited speakers, for the shared hotel rooms (financial support), and for the social dinner (see above).

Sponsors

This school is financially supported by the Prosecco team at INRIA Paris-Rocquencourt with funds from the ERC Starting Grant CRYSP. The EPSRC CryptoForma network on formal methods and cryptography sponsors a number of grants for UK attendees. The MSR-Inria Joint Centre sponsors the social dinner. Cryptosense organizes and sponsors the reception.

CNRS    INRIA    ERC    CryptoForma      Microsoft Research Inria Joint Centre      Cryptosense