Difference between revisions of "The Joint EasyCrypt-F*-CryptoVerif School 2014"
m (→Locations) |
|||
(65 intermediate revisions by 2 users not shown) | |||
Line 2: | Line 2: | ||
|__TOC__ | |__TOC__ | ||
|} | |} | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
= Abstract = | = Abstract = | ||
− | The school is aimed at teaching participants how to use three state-of-the-art security verification tools: [https://www.easycrypt.info EasyCrypt], [https:// | + | 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://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:// | + | '''[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 34: | 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 41: | 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:// | + | * '''[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 48: | Line 41: | ||
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited | 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. | talks, a longer one Wednesday morning and a short one Friday morning. | ||
− | * [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - | + | * [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) - | + | * [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 | ||
= Organization = | = Organization = | ||
Anna Bednarik, | Anna Bednarik, | ||
+ | [http://prosecco.gforge.inria.fr/personal/karthik/ Karthikeyan Bhargavan], | ||
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]), | [http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]), | ||
[http://pierre-yves.strub.nu/ Pierre-Yves Strub] | [http://pierre-yves.strub.nu/ Pierre-Yves Strub] | ||
+ | |||
+ | Student volunteers: Evmorfia-Iro Bartzia, Benjamin Beurdouche, Antoine Delignat-Lavaud, and Jean Karim Zinzindohoué | ||
+ | |||
+ | = Materials = | ||
+ | * [https://www.easycrypt.info/trac/wiki/SchoolParis14 EasyCrypt] | ||
+ | * [https://wiki.inria.fr/prosecco/F*_Materials_-_Joint_School_2014 F*] | ||
+ | * [https://wiki.inria.fr/prosecco/CryptoVerif_Installation#Teaching_material CryptoVerif] | ||
+ | * [https://wiki.inria.fr/prosecco/Abstracts_of_Invited_Talks_-_Joint_School_2014 Invited talks] | ||
= Registration = | = Registration = | ||
Line 66: | Line 68: | ||
--> | --> | ||
* '''The school has filled up completely, we have no space for additional participants'''. | * '''The school has filled up completely, we have no space for additional participants'''. | ||
+ | |||
+ | = Locations = | ||
+ | We have two locations: | ||
+ | * '''Monday, Tuesday, and Friday are at: [http://www.ciup.fr/maison-internationale/ Maison Internationale], [http://www.ciup.fr/salon-david-weill/ Salon David Weill], [http://www.ciup.fr/ Cité internationale universitaire de Paris (Cite Universitaire)], [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris 17 Boulevard Jourdan, 75014 Paris]''' | ||
+ | ** The best ways to reach Cite Universitaire are by [https://en.wikipedia.org/wiki/RER_B RER B] or by [https://en.wikipedia.org/wiki/%C3%8Ele-de-France_tramway_Line_3#T3a Tram T3a]. The RER/tram station is called Cite Universitaire. By metro you will need to change to one of these two or walk a kilometer or two (e.g. [https://en.wikipedia.org/wiki/Paris_M%C3%A9tro_Line_4#mediaviewer/File:Plan_m%C3%A9tro_4_Paris.svg M4] goes to [https://goo.gl/maps/JGMrL Porte d'Orleans]). You can in principle also take the bus to stations Cité Universitaire or Stade Charléty (lines 21, 67, or 216), although that's a bit harder for people without some experience of Paris. | ||
+ | ** [https://wiki.inria.fr/wikis/prosecco/images/1/14/Reaching-maison-internationale.pdf Some information and maps for reaching Maison Internationale] (warning: on the 2nd page north is up, but on the 3rd north is down) | ||
+ | ** [https://wiki.inria.fr/wikis/prosecco/images/f/fc/Reaching-salon-david-weill.pdf Some information and maps for finding Salon David Weill within Maison Internationale] (warning: on these plans north is down, and ouest means West; there will also be signs guiding you there) | ||
+ | ** We will have lunch at the [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire of Maison Internationale]. The menu (entrée, plat, dessert) is about 6-10€. There are [https://goo.gl/maps/H4mxj few restaurants around and they are quite far] for a 1h30mins break. | ||
+ | * '''Wednesday and Thursday we are at: [http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/cordeliers.html UPMC - Campus des Cordeliers], [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy], [https://www.google.fr/maps/place/15+Rue+de+l'École+de+Médecine,+75005+Paris 15 Rue de l'École de Médecine, 75006 Paris]''' | ||
+ | ** The easiest way to reach [http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/cordeliers.html UPMC - Campus des Cordeliers] is either by [https://en.wikipedia.org/wiki/RER_B RER B] (station [https://goo.gl/maps/PjYQY Saint-Michel - Notre-Dame]), or by metro (station [http://goo.gl/maps/M5avz Odéon] for lines [https://en.wikipedia.org/wiki/Paris_M%C3%A9tro_Line_4#mediaviewer/File:Plan_m%C3%A9tro_4_Paris.svg M4] and [https://en.wikipedia.org/wiki/Paris_M%C3%A9tro_Line_10#Route_and_stations M10]). You can in principle also take the bus (lines 58, 63, 70, 86, 87, or 96), although that's a bit harder for people without some experience of Paris. | ||
+ | ** [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf A plan for finding Amphitheatre Gustave Roussy (the orange dot) within UPMC Cordeliers]; (the entrance to UPMC is marked "accueil"; the amphitheater is on the 2nd floor, staircase B; there will also be signs guiding you there) | ||
+ | ** You are on your own for lunch, but [https://goo.gl/maps/4y6Yt there are plenty of good options around] and the break is 2h long. | ||
= Schedule = | = Schedule = | ||
Line 77: | Line 91: | ||
|- | |- | ||
| 09.15 - 10.15 | | 09.15 - 10.15 | ||
− | | '''EasyCrypt lecture''' - Introduction | + | | '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture1.pdf Introduction (Gilles)] |
| 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 84: | Line 98: | ||
|- | |- | ||
| 10.30 - 11.30 | | 10.30 - 11.30 | ||
− | | '''EasyCrypt lecture''' - | + | | '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture2.pdf An introduction to EasyCrypt (Benjamin)] |
|- | |- | ||
| 11.30 - 11.45 | | 11.30 - 11.45 | ||
Line 90: | Line 104: | ||
|- | |- | ||
| 11.45 - 12.45 | | 11.45 - 12.45 | ||
− | | '''EasyCrypt lecture''' - | + | | '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture3.pdf Proving in EasyCrypt and pRHL in practice (Pierre-Yves)] |
|- | |- | ||
| 12.45 - 14.15 | | 12.45 - 14.15 | ||
Line 97: | Line 111: | ||
|- | |- | ||
| 14.15 - 15.45 | | 14.15 - 15.45 | ||
− | | '''EasyCrypt tutorial''' | + | | '''EasyCrypt tutorial''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/day1.tgz Exercices] |
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill] <br/> + [https://www.google.com/maps/place/23+Avenue+d'Italie,+75013+Paris,+France/ Salle Orange at INRIA] <br/> ([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk]) | | rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill] <br/> + [https://www.google.com/maps/place/23+Avenue+d'Italie,+75013+Paris,+France/ Salle Orange at INRIA] <br/> ([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk]) | ||
|- | |- | ||
Line 115: | Line 129: | ||
|- | |- | ||
| 09.15 - 10.15 | | 09.15 - 10.15 | ||
− | | '''EasyCrypt lecture''' - 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 122: | Line 136: | ||
|- | |- | ||
| 10.30 - 11.30 | | 10.30 - 11.30 | ||
− | | '''EasyCrypt lecture''' - High- | + | | '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture5.pdf High-level Proof Principles (Benedikt)] |
|- | |- | ||
| 11.30 - 11.45 | | 11.30 - 11.45 | ||
Line 128: | Line 142: | ||
|- | |- | ||
| 11.45 - 12.45 | | 11.45 - 12.45 | ||
− | | '''EasyCrypt lecture''' - | + | | '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture6.pdf Overview and perspectives (Gilles)] |
|- | |- | ||
| 12.45 - 14.15 | | 12.45 - 14.15 | ||
Line 135: | Line 149: | ||
|- | |- | ||
| 14.15 - 15.45 | | 14.15 - 15.45 | ||
− | | '''EasyCrypt tutorial''' | + | | '''EasyCrypt tutorial''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/day2.tgz Exercices] |
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill] <br/> + [https://www.google.com/maps/place/23+Avenue+d'Italie,+75013+Paris,+France/ Salle Orange at INRIA] <br/> ([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk]) | | rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill] <br/> + [https://www.google.com/maps/place/23+Avenue+d'Italie,+75013+Paris,+France/ Salle Orange at INRIA] <br/> ([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk]) | ||
|- | |- | ||
Line 157: | Line 171: | ||
|- | |- | ||
| 09:00 - 10:00 | | 09:00 - 10:00 | ||
− | | '''F* lecture: High-level introduction (Nikhil) | + | | '''F* lecture:''' [https://wiki.inria.fr/wikis/prosecco/images/f/f0/Fstar-school-Nov26-2014.pdf High-level introduction] (Nikhil) |
− | | rowspan=" | + | | rowspan="7" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy] |
|- | |- | ||
| 10:00 - 10:15 | | 10:00 - 10:15 | ||
Line 164: | Line 178: | ||
|- | |- | ||
| 10:15 - 10:45 | | 10:15 - 10:45 | ||
− | | '''[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 | + | | '''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: | + | | '''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 173: | Line 187: | ||
|- | |- | ||
| 11:30 - 12:00 | | 11:30 - 12:00 | ||
− | | '''Hubert Comon: | + | | '''Hubert Comon:''' Unconditional Soundness (Invited Talk) |
|- | |- | ||
| 12:00 - 12:30 | | 12:00 - 12:30 | ||
− | | '''CryptoVerif lecture: 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 | ||
| ''lunch break'' | | ''lunch break'' | ||
|- | |- | ||
− | | 14 | + | | 14.30 - 19:00 |
− | | '''F* | + | | '''F* tutorial:''' [http://prosecco.gforge.inria.fr/tutorial.html#sec-introduction Basic F*] |
− | + | | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]<br/> + [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Room Déjerine] (35 people) | |
− | |||
− | |||
− | |||
− | |||
− | |||
− | | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]<br/> + [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf | ||
|- | |- | ||
| 19:00 - 21:00 | | 19:00 - 21:00 | ||
Line 203: | Line 211: | ||
! Room | ! Room | ||
|- | |- | ||
− | | | + | | 9:00 - 9:30 |
− | | '''F* lecture''' | + | | '''F* lecture:''' [http://prosecco.gforge.inria.fr/tutorial.html#sec-state-and-other-effects Advanced F*] (Nikhil) |
− | | rowspan=" | + | | rowspan="6" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy] |
+ | |- | ||
+ | | 9:30 - 10:00 | ||
+ | | '''F* lecture:''' [https://wiki.inria.fr/wikis/prosecco/images/2/28/Mitls.pdf miTLS] (Antoine) | ||
|- | |- | ||
| 10:00 - 10:15 | | 10:00 - 10:15 | ||
Line 211: | Line 222: | ||
|- | |- | ||
| 10:15 - 11:15 | | 10:15 - 11:15 | ||
− | | '''F* lecture''' | + | | '''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 217: | Line 228: | ||
|- | |- | ||
| 11:30 - 12:30 | | 11:30 - 12:30 | ||
− | | '''F* lecture''' | + | | '''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 | ||
| ''lunch break'' | | ''lunch break'' | ||
|- | |- | ||
− | | 14:30 - 16: | + | | 14:30 - 16:30 |
− | | '''F* tutorial''' | + | | '''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) | ||
|- | |- | ||
− | | 16: | + | | 16:30 - 17:00 |
| ''break'' | | ''break'' | ||
|- | |- | ||
− | | | + | | 17.00 - 18:00 |
− | | '''F* tutorial''' | + | | '''F* tutorial:''' [http://prosecco.gforge.inria.fr/tutorial.html#sec-case-study--simply-typed-lambda-calculus Simply Typed Lambda Calculus] (Catalin, Chantal) |
|} | |} | ||
Line 241: | Line 252: | ||
|- | |- | ||
| 09:00 - 10:30 | | 09:00 - 10:30 | ||
− | | '''CryptoVerif lecture''' | + | | '''[http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Course.pdf CryptoVerif lecture]''' (Bruno) |
− | | rowspan=" | + | | rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill] |
|- | |- | ||
| 10:30 - 11:00 | | 10:30 - 11:00 | ||
Line 248: | Line 259: | ||
|- | |- | ||
| 11:00 - 12:30 | | 11:00 - 12:30 | ||
− | | '''CryptoVerif lecture''' | + | | '''[http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Course.pdf CryptoVerif lecture]''' (Bruno) |
− | |||
− | |||
− | |||
|- | |- | ||
| 13:00 - 14:30 | | 13:00 - 14:30 | ||
Line 267: | Line 275: | ||
| '''CryptoVerif tutorial''' | | '''CryptoVerif tutorial''' | ||
|} | |} | ||
+ | |||
+ | = Photos = | ||
+ | [https://wiki.inria.fr/wikis/prosecco/images/b/b3/2014-11-26-School.zip Download] | ||
+ | <gallery> | ||
+ | IMG_6593.JPG| | ||
+ | IMG_6594.JPG| | ||
+ | IMG_6595.JPG| | ||
+ | IMG_6600.JPG| | ||
+ | IMG_6602.JPG| | ||
+ | IMG_6605.JPG| | ||
+ | IMG_6607.JPG| | ||
+ | IMG_6609.JPG| | ||
+ | </gallery> | ||
= 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:// | + | 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] | ||
+ | * [https://github.com/FStarLang/FStar/blob/master/INSTALL.md F* Installation Instructions] | ||
<!-- | <!-- | ||
= Financial support = | = Financial support = | ||
Line 292: | 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 | + | 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 = | ||
− | This school is financially supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. The [http://www.cryptoforma.org.uk/ EPSRC CryptoForma network on formal methods and cryptography] sponsors a number of [https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Financial_support grants] for UK attendees. The [http://www.msr-inria.fr/ MSR-Inria Joint Centre] sponsors the [https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner social dinner]. [http://cryptosense.com/ Cryptosense] organizes and sponsors the [https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception reception]. | + | This school is financially supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt] |
+ | with funds from the [http://cordis.europa.eu/project/rcn/96778_en.html ERC Starting Grant CRYSP]. | ||
+ | The [http://www.cryptoforma.org.uk/ EPSRC CryptoForma network on formal methods and cryptography] sponsors a number of [https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Financial_support grants] for UK attendees. The [http://www.msr-inria.fr/ MSR-Inria Joint Centre] sponsors the [https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner social dinner]. [http://cryptosense.com/ Cryptosense] organizes and sponsors the [https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception reception]. | ||
− | [[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] | + | [[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] |
[[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] | [[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] | ||
+ | [[Image:Erc-logo3.png|80px|ERC|link=http://erc.europa.eu/]] | ||
[[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] | [[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] | ||
[[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/]] | ||
[[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]] | [[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]] |
Latest revision as of 19: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
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:
- 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, Markulf Kohlweiss, Aseem Rastogi, Pierre-Yves Strub, Nikhil Swamy
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.
- Hubert Comon (LSV, CNRS & ENS de Cachan) - Unconditional Soundness
- Véronique Cortier (CNRS & LORIA Nancy) - Type-Based Verification of Electronic Voting Protocols
- Matteo Maffei (Saarland University) - Logical Foundations of Secure Resource Management in Protocol Implementations
- Dominique Unruh (University of Tartu) - Computational Soundness for Refinement Types
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:
- Monday, Tuesday, and Friday are at: Maison Internationale, Salon David Weill, Cité internationale universitaire de Paris (Cite Universitaire), 17 Boulevard Jourdan, 75014 Paris
- The best ways to reach Cite Universitaire are by RER B or by Tram T3a. The RER/tram station is called Cite Universitaire. By metro you will need to change to one of these two or walk a kilometer or two (e.g. M4 goes to Porte d'Orleans). You can in principle also take the bus to stations Cité Universitaire or Stade Charléty (lines 21, 67, or 216), although that's a bit harder for people without some experience of Paris.
- Some information and maps for reaching Maison Internationale (warning: on the 2nd page north is up, but on the 3rd north is down)
- Some information and maps for finding Salon David Weill within Maison Internationale (warning: on these plans north is down, and ouest means West; there will also be signs guiding you there)
- We will have lunch at the Restaurant Universitaire of Maison Internationale. The menu (entrée, plat, dessert) is about 6-10€. There are few restaurants around and they are quite far for a 1h30mins break.
- Wednesday and Thursday we are at: UPMC - Campus des Cordeliers, Amphitheatre Gustave Roussy, 15 Rue de l'École de Médecine, 75006 Paris
- The easiest way to reach UPMC - Campus des Cordeliers is either by RER B (station Saint-Michel - Notre-Dame), or by metro (station Odéon for lines M4 and M10). You can in principle also take the bus (lines 58, 63, 70, 86, 87, or 96), although that's a bit harder for people without some experience of Paris.
- A plan for finding Amphitheatre Gustave Roussy (the orange dot) within UPMC Cordeliers; (the entrance to UPMC is marked "accueil"; the amphitheater is on the 2nd floor, staircase B; there will also be signs guiding you there)
- You are on your own for lunch, but there are plenty of good options around and the break is 2h long.
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
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.
- CryptoVerif Installation Instructions
- EasyCrypt Installation Instructions
- F* Installation Instructions
Social dinner
- The social dinner is free for all registered participants and takes place Wednesday at 7pm at Bouillon Racine.
- Bouillon Racine is located at 3 rue Racine, 75006 Paris, a 2 minutes walk from UPMC - Campus des Cordeliers.
- The social dinner is sponsored by the MSR-Inria Joint Centre.
Cryptosense reception
- The Cryptosense reception takes place Tuesday 6-8pm at Le Vin Qui Danse, Gobelins.
- We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by Cryptosense, and the possibility of buying beer or cocktails at the bar. Afterwards it's a reasonable area for people to split up and go for dinner in smaller groups.
- Le Vin Qui Danse, Gobelins is located at 69 Rue Broca, 75013 Paris. That's a 25 minutes walk from Cité Universitaire (15 minutes walk from Place d'Italie). From Cité Universitaire one can also take RER B, get off at Port Royal, and then walk for 10 minutes.
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.