https://wiki.inria.fr/wikis/prosecco/api.php?action=feedcontributions&user=Pierre-yves2&feedformat=atomprosecco - User contributions [en]2024-03-28T15:42:38ZUser contributionsMediaWiki 1.32.6https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=269The Joint EasyCrypt-F*-CryptoVerif School 20142014-11-27T15:26:27Z<p>Pierre-yves2: /* Tuesday, November 25th 2014 */</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
The presented tools have been developed at<br />
<br />
[[Image:cnrs.png|60px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|60px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea2.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:inria.png|130px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one Wednesday morning and a short one Friday morning.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Unconditional Soundness<br />
* [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]<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Affine Refinement Types for Secure Distributed Programming<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/karthik/ Karthikeyan Bhargavan],<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
Student volunteers: Evmorfia-Iro Bartzia, Benjamin Beurdouche, Antoine Delignat-Lavaud, and Jean Karim Zinzindohoué<br />
<br />
= Registration =<br />
<!--<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
--><br />
* '''The school has filled up completely, we have no space for additional participants'''.<br />
<br />
= Locations =<br />
We have two locations:<br />
* '''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]'''<br />
** 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. <br />
** [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)<br />
** [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)<br />
** 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.<br />
* '''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]'''<br />
** 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.<br />
** [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)<br />
** 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.<br />
<br />
= Schedule =<br />
<br />
=== Monday, November 24th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture1.pdf Introduction (Gilles)]<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture2.pdf An introduction to EasyCrypt (Benjamin)]<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture3.pdf Proving in EasyCrypt and pRHL in practice (Pierre-Yves)]<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/day1.tgz Exercices]<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|}<br />
<br />
=== Tuesday, November 25th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture4.pdf Theories, Cloning and Modules]<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture5.pdf High-level Proof Principles (Benedikt)]<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture6.pdf Overview and perspectives (Gilles)]<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/day2.tgz Exercices]<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|-<br />
| 18.00 - 20:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception Cryptosense Reception]'''<br />
| [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] <br/> ([https://www.google.com/maps/dir/Cité+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/ 25 minutes walk from CiteU])<br />
|}<br />
<br />
=== Wednesday, November 26th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture: High-level introduction (Nikhil)'''<br />
| rowspan="7" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''[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: Type-Based Verification of Electronic Voting Protocols] (Invited Talk)'''<br />
|-<br />
| 10:45 - 11:15<br />
| '''Matteo Maffei: Affine Refinement Types for Secure Distributed Programming (Invited Talk)'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:00<br />
| '''Hubert Comon: Unconditional Soundness (Invited Talk)'''<br />
|-<br />
| 12:00 - 12:30<br />
| '''[http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Wednesday.pdf CryptoVerif lecture: sneak preview (Bruno)]'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14.30 - 19:00<br />
| '''F* tutorial: Basic F*'''<br />
| [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)<br />
|-<br />
| 19:00 - 21:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner Social dinner]'''<br />
| [http://www.bouillon-racine.com/ Bouillon Racine] ([https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ 2 minutes walk])<br />
|}<br />
<br />
=== Thursday, November 27th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 9:00 - 10:00<br />
| '''F* lecture: Advanced F* (Nikhil)'''<br />
| rowspan="6" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''F* lecture: miTLS (Antoine)'''<br />
|-<br />
| 10:45 - 11:00<br />
| ''short break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''F* lecture: Types for Modular Cryptography (Cedric)'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* tutorial: Verifying Simple Cryptography'''<br />
| rowspan="3" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''F* tutorial: Advanced F*'''<br />
|}<br />
<br />
=== Friday, November 28th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09:00 - 10:30<br />
| '''CryptoVerif lecture'''<br />
| rowspan="4" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 10:30 - 11:00<br />
| ''break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''CryptoVerif lecture'''<br />
|-<br />
| 12:30 - 13:00<br />
| '''Dominique Unruh: Computational Soundness for Refinement Types (Invited talk)'''<br />
|-<br />
| 13:00 - 14:30<br />
| ''lunch break''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14:30 - 16:00<br />
| '''CryptoVerif tutorial'''<br />
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''CryptoVerif tutorial'''<br />
|}<br />
<br />
= Hardware and software =<br />
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.<br />
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]<br />
* [https://www.easycrypt.info/trac/wiki/SchoolParis14Install EasyCrypt Installation Instructions]<br />
* [https://github.com/FStarLang/FStar/blob/master/INSTALL.md F* Installation Instructions]<br />
<!--<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* Most of these grants are supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
--><br />
<br />
= Social dinner =<br />
* The social dinner is free for all registered participants and takes place '''Wednesday at 7pm at [http://www.bouillon-racine.com/ Bouillon Racine]'''.<br />
* Bouillon Racine is located at [https://www.google.com/maps/place/Bouillon+Racine 3 rue Racine, 75006 Paris], [https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ a 2 minutes walk from UPMC - Campus des Cordeliers].<br />
* The social dinner is sponsored by the [http://www.msr-inria.fr/ MSR-Inria Joint Centre].<br />
<br />
= Cryptosense reception =<br />
* The [http://cryptosense.com/ Cryptosense] reception takes place '''Tuesday 6-8pm at [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins]'''.<br />
* We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by [http://cryptosense.com/ 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.<br />
* [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] is located at [https://www.google.com/maps/place/69+Rue+Broca,+75013+Paris,+France/ 69 Rue Broca, 75013 Paris]. That's a [https://www.google.com/maps/dir/Cit%C3%A9+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8285824,2.3335993,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a1a98df859:0x1c4282bc491b8270!2m2!1d2.338553!2d48.820237!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 25 minutes walk from Cité Universitaire] ([https://www.google.com/maps/dir/23+Avenue+d'Italie,+75013+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8328814,2.3471811,16z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e6718efd139081:0x30c4a0c3d61b6f55!2m2!1d2.3568972!2d48.8283983!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 15 minutes walk from Place d'Italie]). From Cité Universitaire one can also [https://www.google.com/maps/dir/Cit%C3%A9+Universitaire/69+Rue+Broca,+75013+Paris,+France/@48.8301271,2.3307519,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a19d1b03eb:0xe4752dc769ccc6a8!2m2!1d2.338835!2d48.820371!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e3 take RER B, get off at Port Royal, and then walk for 10 minutes].<br />
<br />
= Travel, food, and accommodation =<br />
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).<br />
<br />
= Sponsors =<br />
This school is financially supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]<br />
with funds from the [http://cordis.europa.eu/project/rcn/96778_en.html ERC Starting Grant CRYSP].<br />
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].<br />
<br />
[[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:Erc-logo3.png|80px|ERC|link=http://erc.europa.eu/]] &nbsp;&nbsp;<br />
[[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=268The Joint EasyCrypt-F*-CryptoVerif School 20142014-11-27T15:26:15Z<p>Pierre-yves2: /* Monday, November 24th 2014 */</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
The presented tools have been developed at<br />
<br />
[[Image:cnrs.png|60px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|60px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea2.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:inria.png|130px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one Wednesday morning and a short one Friday morning.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Unconditional Soundness<br />
* [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]<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Affine Refinement Types for Secure Distributed Programming<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/karthik/ Karthikeyan Bhargavan],<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
Student volunteers: Evmorfia-Iro Bartzia, Benjamin Beurdouche, Antoine Delignat-Lavaud, and Jean Karim Zinzindohoué<br />
<br />
= Registration =<br />
<!--<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
--><br />
* '''The school has filled up completely, we have no space for additional participants'''.<br />
<br />
= Locations =<br />
We have two locations:<br />
* '''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]'''<br />
** 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. <br />
** [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)<br />
** [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)<br />
** 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.<br />
* '''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]'''<br />
** 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.<br />
** [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)<br />
** 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.<br />
<br />
= Schedule =<br />
<br />
=== Monday, November 24th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture1.pdf Introduction (Gilles)]<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture2.pdf An introduction to EasyCrypt (Benjamin)]<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture3.pdf Proving in EasyCrypt and pRHL in practice (Pierre-Yves)]<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/day1.tgz Exercices]<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|}<br />
<br />
=== Tuesday, November 25th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture4.pdf Theories, Cloning and Modules]<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture5.pdf High-level Proof Principles (Benedikt)]<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture6.pdf Overview and perspectives (Gilles)]<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|-<br />
| 18.00 - 20:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception Cryptosense Reception]'''<br />
| [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] <br/> ([https://www.google.com/maps/dir/Cité+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/ 25 minutes walk from CiteU])<br />
|}<br />
<br />
=== Wednesday, November 26th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture: High-level introduction (Nikhil)'''<br />
| rowspan="7" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''[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: Type-Based Verification of Electronic Voting Protocols] (Invited Talk)'''<br />
|-<br />
| 10:45 - 11:15<br />
| '''Matteo Maffei: Affine Refinement Types for Secure Distributed Programming (Invited Talk)'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:00<br />
| '''Hubert Comon: Unconditional Soundness (Invited Talk)'''<br />
|-<br />
| 12:00 - 12:30<br />
| '''[http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Wednesday.pdf CryptoVerif lecture: sneak preview (Bruno)]'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14.30 - 19:00<br />
| '''F* tutorial: Basic F*'''<br />
| [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)<br />
|-<br />
| 19:00 - 21:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner Social dinner]'''<br />
| [http://www.bouillon-racine.com/ Bouillon Racine] ([https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ 2 minutes walk])<br />
|}<br />
<br />
=== Thursday, November 27th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 9:00 - 10:00<br />
| '''F* lecture: Advanced F* (Nikhil)'''<br />
| rowspan="6" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''F* lecture: miTLS (Antoine)'''<br />
|-<br />
| 10:45 - 11:00<br />
| ''short break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''F* lecture: Types for Modular Cryptography (Cedric)'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* tutorial: Verifying Simple Cryptography'''<br />
| rowspan="3" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''F* tutorial: Advanced F*'''<br />
|}<br />
<br />
=== Friday, November 28th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09:00 - 10:30<br />
| '''CryptoVerif lecture'''<br />
| rowspan="4" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 10:30 - 11:00<br />
| ''break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''CryptoVerif lecture'''<br />
|-<br />
| 12:30 - 13:00<br />
| '''Dominique Unruh: Computational Soundness for Refinement Types (Invited talk)'''<br />
|-<br />
| 13:00 - 14:30<br />
| ''lunch break''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14:30 - 16:00<br />
| '''CryptoVerif tutorial'''<br />
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''CryptoVerif tutorial'''<br />
|}<br />
<br />
= Hardware and software =<br />
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.<br />
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]<br />
* [https://www.easycrypt.info/trac/wiki/SchoolParis14Install EasyCrypt Installation Instructions]<br />
* [https://github.com/FStarLang/FStar/blob/master/INSTALL.md F* Installation Instructions]<br />
<!--<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* Most of these grants are supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
--><br />
<br />
= Social dinner =<br />
* The social dinner is free for all registered participants and takes place '''Wednesday at 7pm at [http://www.bouillon-racine.com/ Bouillon Racine]'''.<br />
* Bouillon Racine is located at [https://www.google.com/maps/place/Bouillon+Racine 3 rue Racine, 75006 Paris], [https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ a 2 minutes walk from UPMC - Campus des Cordeliers].<br />
* The social dinner is sponsored by the [http://www.msr-inria.fr/ MSR-Inria Joint Centre].<br />
<br />
= Cryptosense reception =<br />
* The [http://cryptosense.com/ Cryptosense] reception takes place '''Tuesday 6-8pm at [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins]'''.<br />
* We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by [http://cryptosense.com/ 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.<br />
* [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] is located at [https://www.google.com/maps/place/69+Rue+Broca,+75013+Paris,+France/ 69 Rue Broca, 75013 Paris]. That's a [https://www.google.com/maps/dir/Cit%C3%A9+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8285824,2.3335993,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a1a98df859:0x1c4282bc491b8270!2m2!1d2.338553!2d48.820237!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 25 minutes walk from Cité Universitaire] ([https://www.google.com/maps/dir/23+Avenue+d'Italie,+75013+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8328814,2.3471811,16z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e6718efd139081:0x30c4a0c3d61b6f55!2m2!1d2.3568972!2d48.8283983!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 15 minutes walk from Place d'Italie]). From Cité Universitaire one can also [https://www.google.com/maps/dir/Cit%C3%A9+Universitaire/69+Rue+Broca,+75013+Paris,+France/@48.8301271,2.3307519,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a19d1b03eb:0xe4752dc769ccc6a8!2m2!1d2.338835!2d48.820371!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e3 take RER B, get off at Port Royal, and then walk for 10 minutes].<br />
<br />
= Travel, food, and accommodation =<br />
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).<br />
<br />
= Sponsors =<br />
This school is financially supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]<br />
with funds from the [http://cordis.europa.eu/project/rcn/96778_en.html ERC Starting Grant CRYSP].<br />
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].<br />
<br />
[[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:Erc-logo3.png|80px|ERC|link=http://erc.europa.eu/]] &nbsp;&nbsp;<br />
[[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=267The Joint EasyCrypt-F*-CryptoVerif School 20142014-11-27T15:25:07Z<p>Pierre-yves2: /* Tuesday, November 25th 2014 */</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
The presented tools have been developed at<br />
<br />
[[Image:cnrs.png|60px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|60px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea2.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:inria.png|130px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one Wednesday morning and a short one Friday morning.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Unconditional Soundness<br />
* [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]<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Affine Refinement Types for Secure Distributed Programming<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/karthik/ Karthikeyan Bhargavan],<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
Student volunteers: Evmorfia-Iro Bartzia, Benjamin Beurdouche, Antoine Delignat-Lavaud, and Jean Karim Zinzindohoué<br />
<br />
= Registration =<br />
<!--<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
--><br />
* '''The school has filled up completely, we have no space for additional participants'''.<br />
<br />
= Locations =<br />
We have two locations:<br />
* '''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]'''<br />
** 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. <br />
** [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)<br />
** [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)<br />
** 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.<br />
* '''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]'''<br />
** 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.<br />
** [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)<br />
** 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.<br />
<br />
= Schedule =<br />
<br />
=== Monday, November 24th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture1.pdf Introduction (Gilles)]<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture2.pdf An introduction to EasyCrypt (Benjamin)]<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture3.pdf Proving in EasyCrypt and pRHL in practice (Pierre-Yves)]<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|}<br />
<br />
=== Tuesday, November 25th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture4.pdf Theories, Cloning and Modules]<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture5.pdf High-level Proof Principles (Benedikt)]<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture6.pdf Overview and perspectives (Gilles)]<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|-<br />
| 18.00 - 20:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception Cryptosense Reception]'''<br />
| [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] <br/> ([https://www.google.com/maps/dir/Cité+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/ 25 minutes walk from CiteU])<br />
|}<br />
<br />
=== Wednesday, November 26th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture: High-level introduction (Nikhil)'''<br />
| rowspan="7" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''[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: Type-Based Verification of Electronic Voting Protocols] (Invited Talk)'''<br />
|-<br />
| 10:45 - 11:15<br />
| '''Matteo Maffei: Affine Refinement Types for Secure Distributed Programming (Invited Talk)'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:00<br />
| '''Hubert Comon: Unconditional Soundness (Invited Talk)'''<br />
|-<br />
| 12:00 - 12:30<br />
| '''[http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Wednesday.pdf CryptoVerif lecture: sneak preview (Bruno)]'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14.30 - 19:00<br />
| '''F* tutorial: Basic F*'''<br />
| [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)<br />
|-<br />
| 19:00 - 21:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner Social dinner]'''<br />
| [http://www.bouillon-racine.com/ Bouillon Racine] ([https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ 2 minutes walk])<br />
|}<br />
<br />
=== Thursday, November 27th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 9:00 - 10:00<br />
| '''F* lecture: Advanced F* (Nikhil)'''<br />
| rowspan="6" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''F* lecture: miTLS (Antoine)'''<br />
|-<br />
| 10:45 - 11:00<br />
| ''short break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''F* lecture: Types for Modular Cryptography (Cedric)'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* tutorial: Verifying Simple Cryptography'''<br />
| rowspan="3" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''F* tutorial: Advanced F*'''<br />
|}<br />
<br />
=== Friday, November 28th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09:00 - 10:30<br />
| '''CryptoVerif lecture'''<br />
| rowspan="4" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 10:30 - 11:00<br />
| ''break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''CryptoVerif lecture'''<br />
|-<br />
| 12:30 - 13:00<br />
| '''Dominique Unruh: Computational Soundness for Refinement Types (Invited talk)'''<br />
|-<br />
| 13:00 - 14:30<br />
| ''lunch break''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14:30 - 16:00<br />
| '''CryptoVerif tutorial'''<br />
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''CryptoVerif tutorial'''<br />
|}<br />
<br />
= Hardware and software =<br />
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.<br />
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]<br />
* [https://www.easycrypt.info/trac/wiki/SchoolParis14Install EasyCrypt Installation Instructions]<br />
* [https://github.com/FStarLang/FStar/blob/master/INSTALL.md F* Installation Instructions]<br />
<!--<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* Most of these grants are supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
--><br />
<br />
= Social dinner =<br />
* The social dinner is free for all registered participants and takes place '''Wednesday at 7pm at [http://www.bouillon-racine.com/ Bouillon Racine]'''.<br />
* Bouillon Racine is located at [https://www.google.com/maps/place/Bouillon+Racine 3 rue Racine, 75006 Paris], [https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ a 2 minutes walk from UPMC - Campus des Cordeliers].<br />
* The social dinner is sponsored by the [http://www.msr-inria.fr/ MSR-Inria Joint Centre].<br />
<br />
= Cryptosense reception =<br />
* The [http://cryptosense.com/ Cryptosense] reception takes place '''Tuesday 6-8pm at [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins]'''.<br />
* We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by [http://cryptosense.com/ 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.<br />
* [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] is located at [https://www.google.com/maps/place/69+Rue+Broca,+75013+Paris,+France/ 69 Rue Broca, 75013 Paris]. That's a [https://www.google.com/maps/dir/Cit%C3%A9+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8285824,2.3335993,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a1a98df859:0x1c4282bc491b8270!2m2!1d2.338553!2d48.820237!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 25 minutes walk from Cité Universitaire] ([https://www.google.com/maps/dir/23+Avenue+d'Italie,+75013+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8328814,2.3471811,16z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e6718efd139081:0x30c4a0c3d61b6f55!2m2!1d2.3568972!2d48.8283983!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 15 minutes walk from Place d'Italie]). From Cité Universitaire one can also [https://www.google.com/maps/dir/Cit%C3%A9+Universitaire/69+Rue+Broca,+75013+Paris,+France/@48.8301271,2.3307519,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a19d1b03eb:0xe4752dc769ccc6a8!2m2!1d2.338835!2d48.820371!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e3 take RER B, get off at Port Royal, and then walk for 10 minutes].<br />
<br />
= Travel, food, and accommodation =<br />
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).<br />
<br />
= Sponsors =<br />
This school is financially supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]<br />
with funds from the [http://cordis.europa.eu/project/rcn/96778_en.html ERC Starting Grant CRYSP].<br />
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].<br />
<br />
[[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:Erc-logo3.png|80px|ERC|link=http://erc.europa.eu/]] &nbsp;&nbsp;<br />
[[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=266The Joint EasyCrypt-F*-CryptoVerif School 20142014-11-27T15:24:26Z<p>Pierre-yves2: /* Monday, November 24th 2014 */</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
The presented tools have been developed at<br />
<br />
[[Image:cnrs.png|60px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|60px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea2.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:inria.png|130px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one Wednesday morning and a short one Friday morning.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Unconditional Soundness<br />
* [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]<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Affine Refinement Types for Secure Distributed Programming<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/karthik/ Karthikeyan Bhargavan],<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
Student volunteers: Evmorfia-Iro Bartzia, Benjamin Beurdouche, Antoine Delignat-Lavaud, and Jean Karim Zinzindohoué<br />
<br />
= Registration =<br />
<!--<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
--><br />
* '''The school has filled up completely, we have no space for additional participants'''.<br />
<br />
= Locations =<br />
We have two locations:<br />
* '''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]'''<br />
** 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. <br />
** [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)<br />
** [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)<br />
** 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.<br />
* '''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]'''<br />
** 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.<br />
** [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)<br />
** 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.<br />
<br />
= Schedule =<br />
<br />
=== Monday, November 24th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture1.pdf Introduction (Gilles)]<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture2.pdf An introduction to EasyCrypt (Benjamin)]<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14/lecture3.pdf Proving in EasyCrypt and pRHL in practice (Pierre-Yves)]<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|}<br />
<br />
=== Tuesday, November 25th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14Install/lecture4.pdf Theories, Cloning and Modules]<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - [https://www.easycrypt.info/trac/raw-attachment/wiki/SchoolParis14Install/lecture5.pdf High-level Proof Principles (Benedikt)]<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - EasyCrypt in the Real-World<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|-<br />
| 18.00 - 20:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception Cryptosense Reception]'''<br />
| [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] <br/> ([https://www.google.com/maps/dir/Cité+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/ 25 minutes walk from CiteU])<br />
|}<br />
<br />
=== Wednesday, November 26th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture: High-level introduction (Nikhil)'''<br />
| rowspan="7" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''[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: Type-Based Verification of Electronic Voting Protocols] (Invited Talk)'''<br />
|-<br />
| 10:45 - 11:15<br />
| '''Matteo Maffei: Affine Refinement Types for Secure Distributed Programming (Invited Talk)'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:00<br />
| '''Hubert Comon: Unconditional Soundness (Invited Talk)'''<br />
|-<br />
| 12:00 - 12:30<br />
| '''[http://prosecco.gforge.inria.fr/personal/bblanche/talks/CV-School14-Wednesday.pdf CryptoVerif lecture: sneak preview (Bruno)]'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14.30 - 19:00<br />
| '''F* tutorial: Basic F*'''<br />
| [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)<br />
|-<br />
| 19:00 - 21:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner Social dinner]'''<br />
| [http://www.bouillon-racine.com/ Bouillon Racine] ([https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ 2 minutes walk])<br />
|}<br />
<br />
=== Thursday, November 27th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 9:00 - 10:00<br />
| '''F* lecture: Advanced F* (Nikhil)'''<br />
| rowspan="6" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Amphitheatre Gustave Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''F* lecture: miTLS (Antoine)'''<br />
|-<br />
| 10:45 - 11:00<br />
| ''short break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''F* lecture: Types for Modular Cryptography (Cedric)'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* tutorial: Verifying Simple Cryptography'''<br />
| rowspan="3" | [https://wiki.inria.fr/wikis/prosecco/images/3/35/UpmcCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''F* tutorial: Advanced F*'''<br />
|}<br />
<br />
=== Friday, November 28th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09:00 - 10:30<br />
| '''CryptoVerif lecture'''<br />
| rowspan="4" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 10:30 - 11:00<br />
| ''break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''CryptoVerif lecture'''<br />
|-<br />
| 12:30 - 13:00<br />
| '''Dominique Unruh: Computational Soundness for Refinement Types (Invited talk)'''<br />
|-<br />
| 13:00 - 14:30<br />
| ''lunch break''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14:30 - 16:00<br />
| '''CryptoVerif tutorial'''<br />
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''CryptoVerif tutorial'''<br />
|}<br />
<br />
= Hardware and software =<br />
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.<br />
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]<br />
* [https://www.easycrypt.info/trac/wiki/SchoolParis14Install EasyCrypt Installation Instructions]<br />
* [https://github.com/FStarLang/FStar/blob/master/INSTALL.md F* Installation Instructions]<br />
<!--<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* Most of these grants are supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
--><br />
<br />
= Social dinner =<br />
* The social dinner is free for all registered participants and takes place '''Wednesday at 7pm at [http://www.bouillon-racine.com/ Bouillon Racine]'''.<br />
* Bouillon Racine is located at [https://www.google.com/maps/place/Bouillon+Racine 3 rue Racine, 75006 Paris], [https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ a 2 minutes walk from UPMC - Campus des Cordeliers].<br />
* The social dinner is sponsored by the [http://www.msr-inria.fr/ MSR-Inria Joint Centre].<br />
<br />
= Cryptosense reception =<br />
* The [http://cryptosense.com/ Cryptosense] reception takes place '''Tuesday 6-8pm at [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins]'''.<br />
* We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by [http://cryptosense.com/ 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.<br />
* [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] is located at [https://www.google.com/maps/place/69+Rue+Broca,+75013+Paris,+France/ 69 Rue Broca, 75013 Paris]. That's a [https://www.google.com/maps/dir/Cit%C3%A9+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8285824,2.3335993,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a1a98df859:0x1c4282bc491b8270!2m2!1d2.338553!2d48.820237!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 25 minutes walk from Cité Universitaire] ([https://www.google.com/maps/dir/23+Avenue+d'Italie,+75013+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8328814,2.3471811,16z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e6718efd139081:0x30c4a0c3d61b6f55!2m2!1d2.3568972!2d48.8283983!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 15 minutes walk from Place d'Italie]). From Cité Universitaire one can also [https://www.google.com/maps/dir/Cit%C3%A9+Universitaire/69+Rue+Broca,+75013+Paris,+France/@48.8301271,2.3307519,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a19d1b03eb:0xe4752dc769ccc6a8!2m2!1d2.338835!2d48.820371!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e3 take RER B, get off at Port Royal, and then walk for 10 minutes].<br />
<br />
= Travel, food, and accommodation =<br />
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).<br />
<br />
= Sponsors =<br />
This school is financially supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]<br />
with funds from the [http://cordis.europa.eu/project/rcn/96778_en.html ERC Starting Grant CRYSP].<br />
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].<br />
<br />
[[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:Erc-logo3.png|80px|ERC|link=http://erc.europa.eu/]] &nbsp;&nbsp;<br />
[[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=189The Joint EasyCrypt-F*-CryptoVerif School 20142014-11-14T20:00:54Z<p>Pierre-yves2: /* Tuesday, November 25th 2014 */</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Place: Paris =<br />
Because the interest was so big, the school location has '''changed'''; we now have two locations:<br />
* Monday, Tuesday, and Friday are at: Maison Internationale, Salon David Weill, Cité internationale universitaire de Paris (Cite Universitaire), [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris 17 Boulevard Jourdan, 75014 Paris]<br />
* Wednesday and Thursday we are at: UPMC - Campus des Cordeliers, Amphitheatre 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]<br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
The presented tools have been developed at<br />
<br />
[[Image:cnrs.png|60px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|60px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea2.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:inria.png|130px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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://alfredo.pironti.eu/research/ Alfredo Pironti], [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]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one Wednesday morning and a short one Friday morning.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Computationally Complete Symbolic Attacker<br />
* [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]<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Affine Refinement Types for Secure Distributed Programming<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
= Registration =<br />
<!--<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
--><br />
* '''The school has filled up completely, we have no space for additional participants'''.<br />
<br />
= Schedule =<br />
<br />
=== Monday, November 24th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - Introduction to Game-Based Proofs<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - Introduction to EasyCrypt<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - Probabilistic Relational Hoare Logic and the EasyCrypt proof engine<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|}<br />
<br />
=== Tuesday, November 25th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - Theories, Cloning and Modules<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - High-Level Cryptographic Proof Principles<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - EasyCrypt in the Real-World<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|-<br />
| 18.00 - 20:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception Cryptosense Reception]'''<br />
| [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] <br/> ([https://www.google.com/maps/dir/Cité+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/ 25 minutes walk from CiteU])<br />
|}<br />
<br />
=== Wednesday, November 26th 2014 (Tentative!) ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture: High-level introduction (Nikhil)'''<br />
| rowspan="10" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''[http://www.loria.fr/~cortier/ 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)'''<br />
|-<br />
| 10:45 - 11:15<br />
| '''Matteo Maffei: Affine Refinement Types for Secure Distributed Programming (Invited Talk)'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:00<br />
| '''Hubert Comon: Computationally Complete Symbolic Attacker (Invited Talk)'''<br />
|-<br />
| 12:00 - 12:30<br />
| '''CryptoVerif lecture: sneak preview (Bruno)'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* lecture: Basics'''<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 19:00<br />
| '''F* lecture and/or tutorial (TBD)'''<br />
| [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br/> + [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Rooms Déjerine and Leroux]<br/> &nbsp;&nbsp;&nbsp;(35 people each)<br />
|-<br />
| 19:00 - 21:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner Social dinner]'''<br />
| [http://www.bouillon-racine.com/ Bouillon Racine] ([https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ 2 minutes walk])<br />
|}<br />
<br />
=== Thursday, November 27th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture'''<br />
| rowspan="5" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 11:15<br />
| '''F* lecture'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:30<br />
| '''F* lecture'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* tutorial'''<br />
| rowspan="3" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''F* tutorial'''<br />
|}<br />
<br />
=== Friday, November 28th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09:00 - 10:30<br />
| '''CryptoVerif lecture'''<br />
| rowspan="4" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 10:30 - 11:00<br />
| ''break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''CryptoVerif lecture'''<br />
|-<br />
| 12:30 - 13:00<br />
| '''Dominique Unruh: Computational Soundness for Refinement Types (Invited talk)'''<br />
|-<br />
| 13:00 - 14:30<br />
| ''lunch break''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14:30 - 16:00<br />
| '''CryptoVerif tutorial'''<br />
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''CryptoVerif tutorial'''<br />
|}<br />
<br />
= Hardware and software =<br />
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.<br />
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]<br />
* [https://www.easycrypt.info/trac/wiki/SchoolParis14Install EasyCrypt Installation Instructions]<br />
<br />
<!--<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* Most of these grants are supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
--><br />
<br />
= Social dinner =<br />
* The social dinner is free for all registered participants and takes place '''Wednesday at 7pm at [http://www.bouillon-racine.com/ Bouillon Racine]'''.<br />
* Bouillon Racine is located at [https://www.google.com/maps/place/Bouillon+Racine 3 rue Racine, 75006 Paris], [https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ a 2 minutes walk from UPMC - Campus des Cordeliers].<br />
* The social dinner is sponsored by the [http://www.msr-inria.fr/ MSR-Inria Joint Centre].<br />
<br />
= Cryptosense reception =<br />
* The [http://cryptosense.com/ Cryptosense] reception takes place '''Tuesday 6-8pm at [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins]'''.<br />
* We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by [http://cryptosense.com/ 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.<br />
* [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] is located at [https://www.google.com/maps/place/69+Rue+Broca,+75013+Paris,+France/ 69 Rue Broca, 75013 Paris]. That's a [https://www.google.com/maps/dir/Cit%C3%A9+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8285824,2.3335993,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a1a98df859:0x1c4282bc491b8270!2m2!1d2.338553!2d48.820237!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 25 minutes walk from Cité Universitaire] ([https://www.google.com/maps/dir/23+Avenue+d'Italie,+75013+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8328814,2.3471811,16z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e6718efd139081:0x30c4a0c3d61b6f55!2m2!1d2.3568972!2d48.8283983!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 15 minutes walk from Place d'Italie]). From Cité Universitaire one can also [https://www.google.com/maps/dir/Cit%C3%A9+Universitaire/69+Rue+Broca,+75013+Paris,+France/@48.8301271,2.3307519,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a19d1b03eb:0xe4752dc769ccc6a8!2m2!1d2.338835!2d48.820371!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e3 take RER B, get off at Port Royal, and then walk for 10 minutes].<br />
<br />
= Travel, food, and accommodation =<br />
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 (see financial support above), and for the social dinner (see above).<br />
<br />
= Sponsors =<br />
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].<br />
<br />
[[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] &nbsp;<br />
[[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=188The Joint EasyCrypt-F*-CryptoVerif School 20142014-11-14T20:00:22Z<p>Pierre-yves2: /* Monday, November 24th 2014 */</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Place: Paris =<br />
Because the interest was so big, the school location has '''changed'''; we now have two locations:<br />
* Monday, Tuesday, and Friday are at: Maison Internationale, Salon David Weill, Cité internationale universitaire de Paris (Cite Universitaire), [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris 17 Boulevard Jourdan, 75014 Paris]<br />
* Wednesday and Thursday we are at: UPMC - Campus des Cordeliers, Amphitheatre 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]<br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
The presented tools have been developed at<br />
<br />
[[Image:cnrs.png|60px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|60px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea2.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:inria.png|130px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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://alfredo.pironti.eu/research/ Alfredo Pironti], [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]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one Wednesday morning and a short one Friday morning.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Computationally Complete Symbolic Attacker<br />
* [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]<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Affine Refinement Types for Secure Distributed Programming<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
= Registration =<br />
<!--<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
--><br />
* '''The school has filled up completely, we have no space for additional participants'''.<br />
<br />
= Schedule =<br />
<br />
=== Monday, November 24th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture''' - Introduction to Game-Based Proofs<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture''' - Introduction to EasyCrypt<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture''' - Probabilistic Relational Hoare Logic and the EasyCrypt proof engine<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|}<br />
<br />
=== Tuesday, November 25th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture'''<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|-<br />
| 18.00 - 20:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception Cryptosense Reception]'''<br />
| [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] <br/> ([https://www.google.com/maps/dir/Cité+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/ 25 minutes walk from CiteU])<br />
|}<br />
<br />
=== Wednesday, November 26th 2014 (Tentative!) ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture: High-level introduction (Nikhil)'''<br />
| rowspan="10" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''[http://www.loria.fr/~cortier/ 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)'''<br />
|-<br />
| 10:45 - 11:15<br />
| '''Matteo Maffei: Affine Refinement Types for Secure Distributed Programming (Invited Talk)'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:00<br />
| '''Hubert Comon: Computationally Complete Symbolic Attacker (Invited Talk)'''<br />
|-<br />
| 12:00 - 12:30<br />
| '''CryptoVerif lecture: sneak preview (Bruno)'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* lecture: Basics'''<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 19:00<br />
| '''F* lecture and/or tutorial (TBD)'''<br />
| [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br/> + [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Rooms Déjerine and Leroux]<br/> &nbsp;&nbsp;&nbsp;(35 people each)<br />
|-<br />
| 19:00 - 21:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner Social dinner]'''<br />
| [http://www.bouillon-racine.com/ Bouillon Racine] ([https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ 2 minutes walk])<br />
|}<br />
<br />
=== Thursday, November 27th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture'''<br />
| rowspan="5" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 11:15<br />
| '''F* lecture'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:30<br />
| '''F* lecture'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* tutorial'''<br />
| rowspan="3" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''F* tutorial'''<br />
|}<br />
<br />
=== Friday, November 28th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09:00 - 10:30<br />
| '''CryptoVerif lecture'''<br />
| rowspan="4" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 10:30 - 11:00<br />
| ''break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''CryptoVerif lecture'''<br />
|-<br />
| 12:30 - 13:00<br />
| '''Dominique Unruh: Computational Soundness for Refinement Types (Invited talk)'''<br />
|-<br />
| 13:00 - 14:30<br />
| ''lunch break''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14:30 - 16:00<br />
| '''CryptoVerif tutorial'''<br />
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''CryptoVerif tutorial'''<br />
|}<br />
<br />
= Hardware and software =<br />
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.<br />
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]<br />
* [https://www.easycrypt.info/trac/wiki/SchoolParis14Install EasyCrypt Installation Instructions]<br />
<br />
<!--<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* Most of these grants are supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
--><br />
<br />
= Social dinner =<br />
* The social dinner is free for all registered participants and takes place '''Wednesday at 7pm at [http://www.bouillon-racine.com/ Bouillon Racine]'''.<br />
* Bouillon Racine is located at [https://www.google.com/maps/place/Bouillon+Racine 3 rue Racine, 75006 Paris], [https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ a 2 minutes walk from UPMC - Campus des Cordeliers].<br />
* The social dinner is sponsored by the [http://www.msr-inria.fr/ MSR-Inria Joint Centre].<br />
<br />
= Cryptosense reception =<br />
* The [http://cryptosense.com/ Cryptosense] reception takes place '''Tuesday 6-8pm at [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins]'''.<br />
* We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by [http://cryptosense.com/ 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.<br />
* [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] is located at [https://www.google.com/maps/place/69+Rue+Broca,+75013+Paris,+France/ 69 Rue Broca, 75013 Paris]. That's a [https://www.google.com/maps/dir/Cit%C3%A9+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8285824,2.3335993,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a1a98df859:0x1c4282bc491b8270!2m2!1d2.338553!2d48.820237!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 25 minutes walk from Cité Universitaire] ([https://www.google.com/maps/dir/23+Avenue+d'Italie,+75013+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8328814,2.3471811,16z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e6718efd139081:0x30c4a0c3d61b6f55!2m2!1d2.3568972!2d48.8283983!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 15 minutes walk from Place d'Italie]). From Cité Universitaire one can also [https://www.google.com/maps/dir/Cit%C3%A9+Universitaire/69+Rue+Broca,+75013+Paris,+France/@48.8301271,2.3307519,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a19d1b03eb:0xe4752dc769ccc6a8!2m2!1d2.338835!2d48.820371!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e3 take RER B, get off at Port Royal, and then walk for 10 minutes].<br />
<br />
= Travel, food, and accommodation =<br />
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 (see financial support above), and for the social dinner (see above).<br />
<br />
= Sponsors =<br />
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].<br />
<br />
[[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] &nbsp;<br />
[[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=187The Joint EasyCrypt-F*-CryptoVerif School 20142014-11-14T18:11:13Z<p>Pierre-yves2: /* Hardware and software */</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Place: Paris =<br />
Because the interest was so big, the school location has '''changed'''; we now have two locations:<br />
* Monday, Tuesday, and Friday are at: Maison Internationale, Salon David Weill, Cité internationale universitaire de Paris (Cite Universitaire), [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris 17 Boulevard Jourdan, 75014 Paris]<br />
* Wednesday and Thursday we are at: UPMC - Campus des Cordeliers, Amphitheatre 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]<br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
The presented tools have been developed at<br />
<br />
[[Image:cnrs.png|60px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|60px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea2.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:inria.png|130px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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://alfredo.pironti.eu/research/ Alfredo Pironti], [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]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one Wednesday morning and a short one Friday morning.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Computationally Complete Symbolic Attacker<br />
* [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]<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Affine Refinement Types for Secure Distributed Programming<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
= Registration =<br />
<!--<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
--><br />
* '''The school has filled up completely, we have no space for additional participants'''.<br />
<br />
= Schedule =<br />
<br />
=== Monday, November 24th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture'''<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|}<br />
<br />
=== Tuesday, November 25th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture'''<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|-<br />
| 18.00 - 20:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception Cryptosense Reception]'''<br />
| [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] <br/> ([https://www.google.com/maps/dir/Cité+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/ 25 minutes walk from CiteU])<br />
|}<br />
<br />
=== Wednesday, November 26th 2014 (Tentative!) ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture: High-level introduction (Nikhil)'''<br />
| rowspan="10" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''[http://www.loria.fr/~cortier/ 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)'''<br />
|-<br />
| 10:45 - 11:15<br />
| '''Matteo Maffei: Affine Refinement Types for Secure Distributed Programming (Invited Talk)'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:00<br />
| '''Hubert Comon: Computationally Complete Symbolic Attacker (Invited Talk)'''<br />
|-<br />
| 12:00 - 12:30<br />
| '''CryptoVerif lecture: sneak preview (Bruno)'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* lecture: Basics'''<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 19:00<br />
| '''F* lecture and/or tutorial (TBD)'''<br />
| [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br/> + [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Rooms Déjerine and Leroux]<br/> &nbsp;&nbsp;&nbsp;(35 people each)<br />
|-<br />
| 19:00 - 21:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner Social dinner]'''<br />
| [http://www.bouillon-racine.com/ Bouillon Racine] ([https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ 2 minutes walk])<br />
|}<br />
<br />
=== Thursday, November 27th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture'''<br />
| rowspan="5" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 11:15<br />
| '''F* lecture'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:30<br />
| '''F* lecture'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* tutorial'''<br />
| rowspan="3" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''F* tutorial'''<br />
|}<br />
<br />
=== Friday, November 28th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09:00 - 10:30<br />
| '''CryptoVerif lecture'''<br />
| rowspan="4" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 10:30 - 11:00<br />
| ''break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''CryptoVerif lecture'''<br />
|-<br />
| 12:30 - 13:00<br />
| '''Dominique Unruh: Computational Soundness for Refinement Types (Invited talk)'''<br />
|-<br />
| 13:00 - 14:30<br />
| ''lunch break''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14:30 - 16:00<br />
| '''CryptoVerif tutorial'''<br />
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''CryptoVerif tutorial'''<br />
|}<br />
<br />
= Hardware and software =<br />
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.<br />
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]<br />
* [https://www.easycrypt.info/trac/wiki/SchoolParis14Install EasyCrypt Installation Instructions]<br />
<br />
<!--<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* Most of these grants are supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
--><br />
<br />
= Social dinner =<br />
* The social dinner is free for all registered participants and takes place '''Wednesday at 7pm at [http://www.bouillon-racine.com/ Bouillon Racine]'''.<br />
* Bouillon Racine is located at [https://www.google.com/maps/place/Bouillon+Racine 3 rue Racine, 75006 Paris], [https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ a 2 minutes walk from UPMC - Campus des Cordeliers].<br />
* The social dinner is sponsored by the [http://www.msr-inria.fr/ MSR-Inria Joint Centre].<br />
<br />
= Cryptosense reception =<br />
* The [http://cryptosense.com/ Cryptosense] reception takes place '''Tuesday 6-8pm at [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins]'''.<br />
* We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by [http://cryptosense.com/ 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.<br />
* [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] is located at [https://www.google.com/maps/place/69+Rue+Broca,+75013+Paris,+France/ 69 Rue Broca, 75013 Paris]. That's a [https://www.google.com/maps/dir/Cit%C3%A9+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8285824,2.3335993,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a1a98df859:0x1c4282bc491b8270!2m2!1d2.338553!2d48.820237!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 25 minutes walk from Cité Universitaire] ([https://www.google.com/maps/dir/23+Avenue+d'Italie,+75013+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8328814,2.3471811,16z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e6718efd139081:0x30c4a0c3d61b6f55!2m2!1d2.3568972!2d48.8283983!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 15 minutes walk from Place d'Italie]). From Cité Universitaire one can also [https://www.google.com/maps/dir/Cit%C3%A9+Universitaire/69+Rue+Broca,+75013+Paris,+France/@48.8301271,2.3307519,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a19d1b03eb:0xe4752dc769ccc6a8!2m2!1d2.338835!2d48.820371!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e3 take RER B, get off at Port Royal, and then walk for 10 minutes].<br />
<br />
= Travel, food, and accommodation =<br />
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 (see financial support above), and for the social dinner (see above).<br />
<br />
= Sponsors =<br />
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].<br />
<br />
[[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] &nbsp;<br />
[[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=186The Joint EasyCrypt-F*-CryptoVerif School 20142014-11-14T18:02:08Z<p>Pierre-yves2: /* Tuesday, November 25th 2014 */</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Place: Paris =<br />
Because the interest was so big, the school location has '''changed'''; we now have two locations:<br />
* Monday, Tuesday, and Friday are at: Maison Internationale, Salon David Weill, Cité internationale universitaire de Paris (Cite Universitaire), [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris 17 Boulevard Jourdan, 75014 Paris]<br />
* Wednesday and Thursday we are at: UPMC - Campus des Cordeliers, Amphitheatre 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]<br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
The presented tools have been developed at<br />
<br />
[[Image:cnrs.png|60px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|60px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea2.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:inria.png|130px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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://alfredo.pironti.eu/research/ Alfredo Pironti], [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]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one Wednesday morning and a short one Friday morning.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Computationally Complete Symbolic Attacker<br />
* [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]<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Affine Refinement Types for Secure Distributed Programming<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
= Registration =<br />
<!--<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
--><br />
* '''The school has filled up completely, we have no space for additional participants'''.<br />
<br />
= Schedule =<br />
<br />
=== Monday, November 24th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture'''<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|}<br />
<br />
=== Tuesday, November 25th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture'''<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|-<br />
| 18.00 - 20:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception Cryptosense Reception]'''<br />
| [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] <br/> ([https://www.google.com/maps/dir/Cité+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/ 25 minutes walk from CiteU])<br />
|}<br />
<br />
=== Wednesday, November 26th 2014 (Tentative!) ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture: High-level introduction (Nikhil)'''<br />
| rowspan="10" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''[http://www.loria.fr/~cortier/ 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)'''<br />
|-<br />
| 10:45 - 11:15<br />
| '''Matteo Maffei: Affine Refinement Types for Secure Distributed Programming (Invited Talk)'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:00<br />
| '''Hubert Comon: Computationally Complete Symbolic Attacker (Invited Talk)'''<br />
|-<br />
| 12:00 - 12:30<br />
| '''CryptoVerif lecture: sneak preview (Bruno)'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* lecture: Basics'''<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 19:00<br />
| '''F* lecture and/or tutorial (TBD)'''<br />
| [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br/> + [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Rooms Déjerine and Leroux]<br/> &nbsp;&nbsp;&nbsp;(35 people each)<br />
|-<br />
| 19:00 - 21:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner Social dinner]'''<br />
| [http://www.bouillon-racine.com/ Bouillon Racine] ([https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ 2 minutes walk])<br />
|}<br />
<br />
=== Thursday, November 27th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture'''<br />
| rowspan="5" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 11:15<br />
| '''F* lecture'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:30<br />
| '''F* lecture'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* tutorial'''<br />
| rowspan="3" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''F* tutorial'''<br />
|}<br />
<br />
=== Friday, November 28th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09:00 - 10:30<br />
| '''CryptoVerif lecture'''<br />
| rowspan="4" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 10:30 - 11:00<br />
| ''break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''CryptoVerif lecture'''<br />
|-<br />
| 12:30 - 13:00<br />
| '''Dominique Unruh: Computational Soundness for Refinement Types (Invited talk)'''<br />
|-<br />
| 13:00 - 14:30<br />
| ''lunch break''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14:30 - 16:00<br />
| '''CryptoVerif tutorial'''<br />
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''CryptoVerif tutorial'''<br />
|}<br />
<br />
= Hardware and software =<br />
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.<br />
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]<br />
<!--<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* Most of these grants are supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
--><br />
<br />
= Social dinner =<br />
* The social dinner is free for all registered participants and takes place '''Wednesday at 7pm at [http://www.bouillon-racine.com/ Bouillon Racine]'''.<br />
* Bouillon Racine is located at [https://www.google.com/maps/place/Bouillon+Racine 3 rue Racine, 75006 Paris], [https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ a 2 minutes walk from UPMC - Campus des Cordeliers].<br />
* The social dinner is sponsored by the [http://www.msr-inria.fr/ MSR-Inria Joint Centre].<br />
<br />
= Cryptosense reception =<br />
* The [http://cryptosense.com/ Cryptosense] reception takes place '''Tuesday 6-8pm at [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins]'''.<br />
* We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by [http://cryptosense.com/ 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.<br />
* [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] is located at [https://www.google.com/maps/place/69+Rue+Broca,+75013+Paris,+France/ 69 Rue Broca, 75013 Paris]. That's a [https://www.google.com/maps/dir/Cit%C3%A9+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8285824,2.3335993,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a1a98df859:0x1c4282bc491b8270!2m2!1d2.338553!2d48.820237!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 25 minutes walk from Cité Universitaire] ([https://www.google.com/maps/dir/23+Avenue+d'Italie,+75013+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8328814,2.3471811,16z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e6718efd139081:0x30c4a0c3d61b6f55!2m2!1d2.3568972!2d48.8283983!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 15 minutes walk from Place d'Italie]). From Cité Universitaire one can also [https://www.google.com/maps/dir/Cit%C3%A9+Universitaire/69+Rue+Broca,+75013+Paris,+France/@48.8301271,2.3307519,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a19d1b03eb:0xe4752dc769ccc6a8!2m2!1d2.338835!2d48.820371!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e3 take RER B, get off at Port Royal, and then walk for 10 minutes].<br />
<br />
= Travel, food, and accommodation =<br />
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 (see financial support above), and for the social dinner (see above).<br />
<br />
= Sponsors =<br />
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].<br />
<br />
[[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] &nbsp;<br />
[[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=185The Joint EasyCrypt-F*-CryptoVerif School 20142014-11-14T18:01:19Z<p>Pierre-yves2: /* Monday, November 24th 2014 */</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Place: Paris =<br />
Because the interest was so big, the school location has '''changed'''; we now have two locations:<br />
* Monday, Tuesday, and Friday are at: Maison Internationale, Salon David Weill, Cité internationale universitaire de Paris (Cite Universitaire), [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris 17 Boulevard Jourdan, 75014 Paris]<br />
* Wednesday and Thursday we are at: UPMC - Campus des Cordeliers, Amphitheatre 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]<br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
The presented tools have been developed at<br />
<br />
[[Image:cnrs.png|60px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|60px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea2.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:inria.png|130px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:msresearch.png|140px|Microsoft Research|link=http://research.microsoft.com/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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://alfredo.pironti.eu/research/ Alfredo Pironti], [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]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one Wednesday morning and a short one Friday morning.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Computationally Complete Symbolic Attacker<br />
* [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]<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Affine Refinement Types for Secure Distributed Programming<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
= Registration =<br />
<!--<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
--><br />
* '''The school has filled up completely, we have no space for additional participants'''.<br />
<br />
= Schedule =<br />
<br />
=== Monday, November 24th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.15<br />
| '''EasyCrypt lecture'''<br />
| rowspan="5" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.15 - 10.30<br />
| ''break''<br />
|-<br />
| 10.30 - 11.30<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 11.30 - 11.45<br />
| ''break''<br />
|-<br />
| 11.45 - 12.45<br />
| '''EasyCrypt lecture'''<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|}<br />
<br />
=== Tuesday, November 25th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09.15 - 10.45<br />
| '''EasyCrypt lecture''' - TBA<br />
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon David Weill]<br />
|-<br />
| 10.45 - 11.15<br />
| ''break''<br />
|-<br />
| 11.15 - 12.45<br />
| '''EasyCrypt lecture''' - TBA<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
| [http://www.ciup.fr/restaurant/ Restaurant Universitaire]<br />
|-<br />
| 14.15 - 15.45<br />
| '''EasyCrypt tutorial'''<br />
| 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/> &nbsp;&nbsp;&nbsp;([https://www.google.com/maps/dir/17+Boulevard+Jourdan,+75014+Paris,+France/23+Avenue+d'Italie,+Paris,+France/ 25 minutes walk])<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''EasyCrypt tutorial'''<br />
|-<br />
| 18.00 - 20:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Cryptosense_reception Cryptosense Reception]'''<br />
| [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] <br/> ([https://www.google.com/maps/dir/Cité+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/ 25 minutes walk from CiteU])<br />
|}<br />
<br />
=== Wednesday, November 26th 2014 (Tentative!) ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture: High-level introduction (Nikhil)'''<br />
| rowspan="10" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 10:45<br />
| '''[http://www.loria.fr/~cortier/ 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)'''<br />
|-<br />
| 10:45 - 11:15<br />
| '''Matteo Maffei: Affine Refinement Types for Secure Distributed Programming (Invited Talk)'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:00<br />
| '''Hubert Comon: Computationally Complete Symbolic Attacker (Invited Talk)'''<br />
|-<br />
| 12:00 - 12:30<br />
| '''CryptoVerif lecture: sneak preview (Bruno)'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* lecture: Basics'''<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 19:00<br />
| '''F* lecture and/or tutorial (TBD)'''<br />
| [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br/> + [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Rooms Déjerine and Leroux]<br/> &nbsp;&nbsp;&nbsp;(35 people each)<br />
|-<br />
| 19:00 - 21:00<br />
| '''[https://wiki.inria.fr/prosecco/The_Joint_EasyCrypt-F*-CryptoVerif_School_2014#Social_dinner Social dinner]'''<br />
| [http://www.bouillon-racine.com/ Bouillon Racine] ([https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ 2 minutes walk])<br />
|}<br />
<br />
=== Thursday, November 27th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/15+Rue+de+l'%C3%89cole+de+M%C3%A9decine,+75005+Paris UPMC - Campus des Cordeliers]<br />
! Room<br />
|-<br />
| 09:00 - 10:00<br />
| '''F* lecture'''<br />
| rowspan="5" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Amphitheatre Roussy]<br />
|-<br />
| 10:00 - 10:15<br />
| ''short break''<br />
|-<br />
| 10:15 - 11:15<br />
| '''F* lecture'''<br />
|-<br />
| 11:15 - 11:30<br />
| ''short break''<br />
|-<br />
| 11:30 - 12:30<br />
| '''F* lecture'''<br />
|-<br />
| 12:30 - 14:30<br />
| ''lunch break'' <br />
|-<br />
| 14:30 - 16:00<br />
| '''F* tutorial'''<br />
| rowspan="3" | [http://www.fp7-helena.org/CONFERENCE2011/bookletCordeliers.pdf Rooms Déjerine and Leroux]<br/> (35 people each)<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''F* tutorial'''<br />
|}<br />
<br />
=== Friday, November 28th 2014 ===<br />
<br />
{| class="wikitable"<br />
! Time<br />
! style="min-width: 400px;" | [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris Maison Internationale, Cite Universitaire]<br />
! Room<br />
|-<br />
| 09:00 - 10:30<br />
| '''CryptoVerif lecture'''<br />
| rowspan="4" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 10:30 - 11:00<br />
| ''break''<br />
|-<br />
| 11:00 - 12:30<br />
| '''CryptoVerif lecture'''<br />
|-<br />
| 12:30 - 13:00<br />
| '''Dominique Unruh: Computational Soundness for Refinement Types (Invited talk)'''<br />
|-<br />
| 13:00 - 14:30<br />
| ''lunch break''<br />
| [http://www.ciup.fr/restaurant/le-restaurant-universitaire-2/ Restaurant Universitaire]<br />
|-<br />
| 14:30 - 16:00<br />
| '''CryptoVerif tutorial'''<br />
| rowspan="3" | [http://www.ciup.fr/salon-david-weill/ Salon Salon David Weill]<br />
|-<br />
| 16:00 - 16:30<br />
| ''break''<br />
|-<br />
| 16.30 - 18:00<br />
| '''CryptoVerif tutorial'''<br />
|}<br />
<br />
= Hardware and software =<br />
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.<br />
* [[CryptoVerif Installation|CryptoVerif Installation Instructions]]<br />
<!--<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* Most of these grants are supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
--><br />
<br />
= Social dinner =<br />
* The social dinner is free for all registered participants and takes place '''Wednesday at 7pm at [http://www.bouillon-racine.com/ Bouillon Racine]'''.<br />
* Bouillon Racine is located at [https://www.google.com/maps/place/Bouillon+Racine 3 rue Racine, 75006 Paris], [https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ a 2 minutes walk from UPMC - Campus des Cordeliers].<br />
* The social dinner is sponsored by the [http://www.msr-inria.fr/ MSR-Inria Joint Centre].<br />
<br />
= Cryptosense reception =<br />
* The [http://cryptosense.com/ Cryptosense] reception takes place '''Tuesday 6-8pm at [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins]'''.<br />
* We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by [http://cryptosense.com/ 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.<br />
* [http://gobelins.vqd.fr/fr/ Le Vin Qui Danse, Gobelins] is located at [https://www.google.com/maps/place/69+Rue+Broca,+75013+Paris,+France/ 69 Rue Broca, 75013 Paris]. That's a [https://www.google.com/maps/dir/Cit%C3%A9+internationale+universitaire+de+Paris,+17+Boulevard+Jourdan,+75014+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8285824,2.3335993,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a1a98df859:0x1c4282bc491b8270!2m2!1d2.338553!2d48.820237!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 25 minutes walk from Cité Universitaire] ([https://www.google.com/maps/dir/23+Avenue+d'Italie,+75013+Paris,+France/69+Rue+Broca,+75013+Paris,+France/@48.8328814,2.3471811,16z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e6718efd139081:0x30c4a0c3d61b6f55!2m2!1d2.3568972!2d48.8283983!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e2 15 minutes walk from Place d'Italie]). From Cité Universitaire one can also [https://www.google.com/maps/dir/Cit%C3%A9+Universitaire/69+Rue+Broca,+75013+Paris,+France/@48.8301271,2.3307519,15z/data=!3m1!4b1!4m14!4m13!1m5!1m1!1s0x47e671a19d1b03eb:0xe4752dc769ccc6a8!2m2!1d2.338835!2d48.820371!1m5!1m1!1s0x47e671eb47426d69:0xb102905c6c1acf5d!2m2!1d2.3471351!2d48.8369049!3e3 take RER B, get off at Port Royal, and then walk for 10 minutes].<br />
<br />
= Travel, food, and accommodation =<br />
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 (see financial support above), and for the social dinner (see above).<br />
<br />
= Sponsors =<br />
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].<br />
<br />
[[Image:prosecco1.png|160px|CNRS|link=http://prosecco.gforge.inria.fr/]] &nbsp;<br />
[[Image:inria.png|120px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:cryptoforma2.png|150px|CryptoForma|link=http://www.cryptoforma.org.uk/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:cryptosense.png|180px|Cryptosense|link=http://cryptosense.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=106The Joint EasyCrypt-F*-CryptoVerif School 20142014-11-04T09:30:21Z<p>Pierre-yves2: /* Schedule */ EasyCrypt preliminary schedule</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Place: Paris =<br />
Because the interest was so big, the school location has '''changed'''; we now have two locations:<br />
* Monday, Tuesday, and Friday are at: Maison Internationale, Salon David Weill, Cité internationale universitaire de Paris (Cite Universitaire), [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris 17 Boulevard Jourdan, 75014 Paris]<br />
* Wednesday and Thursday we are at: UPMC - Campus des Cordeliers, Amphitheatre 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]<br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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://alfredo.pironti.eu/research/ Alfredo Pironti], [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]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one on Wednesday afternoon and a short one on Friday morning.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Computationally Complete Symbolic Attacker<br />
* [http://www.loria.fr/~cortier/ Véronique Cortier] (CNRS & LORIA Nancy) - Using F* to Verify E-Voting Protocols<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Linear Refinement Type Systems<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
= Schedule =<br />
<br />
== Monday, Novembre 24th 2014 ==<br />
<br />
{| class="wikitable"<br />
|+ EasyCrypt<br />
! Schedule<br />
! style="min-width: 400px;" | Event<br />
|-<br />
| 09.15 - 10.45<br />
| '''lecture''' - TBA<br />
|-<br />
| 10.45 - 11.15<br />
| ''break''<br />
|-<br />
| 11.15 - 12.45<br />
| '''lecture''' - TBA<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
|-<br />
| 14.15 - 15.45<br />
| '''tutorial'''<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''tutorial'''<br />
|}<br />
<br />
== Tuesday, Novembre 25th 2014 ==<br />
<br />
{| class="wikitable"<br />
|+ EasyCrypt<br />
! Schedule<br />
! style="min-width: 400px;" | Event<br />
|-<br />
| 09.15 - 10.45<br />
| '''lecture''' - TBA<br />
|-<br />
| 10.45 - 11.15<br />
| ''break''<br />
|-<br />
| 11.15 - 12.45<br />
| '''lecture''' - TBA<br />
|-<br />
| 12.45 - 14.15<br />
| ''lunch''<br />
|-<br />
| 14.15 - 15.45<br />
| '''tutorial'''<br />
|-<br />
| 15.45 - 16.15<br />
| ''break''<br />
|-<br />
| 16.00 - 17.30<br />
| '''tutorial'''<br />
|}<br />
<br />
== Wednesday, Novembre 26th 2014 ==<br />
<br />
F* lectures and tutorial + Invited speakers: Cortier & Comon & Maffei (afternoon)<br />
<br />
== Thursday, Novembre 27th 2014 ==<br />
<br />
Lectures on F* + CryptoVerif (morning) + F* tutorial (afternoon)<br />
<br />
== Friday, Novembre 28th 2014 ==<br />
<br />
Invited speakers: Unruh (morning) + CryptoVerif lecture + tutorial<br />
<br />
= Hardware and software =<br />
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.<br />
<br />
= Registration =<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
* '''The school has filled up completely, we have no space for additional participants'''.<br />
<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* Most of these grants are supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
<br />
= Social dinner =<br />
* We organized a social dinner that is free for all registered participants.<br />
* The social dinner takes place '''Wednesday at 7pm at [http://www.bouillon-racine.com/ Bouillon Racine]'''.<br />
* Bouillon Racine is located at [https://www.google.com/maps/place/Bouillon+Racine 3 rue Racine, 75006 Paris], [https://www.google.com/maps/dir/UPMC+-+Campus+des+Cordeliers/Bouillon+Racine,+3+Rue+Racine,+75006+Paris,+France/ a 2 minutes walk from UPMC - Campus des Cordeliers].<br />
* This social dinner is sponsored by the [http://www.msr-inria.fr/ MSR-Inria Joint Centre].<br />
<br />
= Travel, food, and accommodation =<br />
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 (see financial support above), and for the social dinner (see above).<br />
<br />
= Sponsors =<br />
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 grants for UK attendees. The [http://www.msr-inria.fr/ MSR-Inria Joint Centre] sponsors the social dinner.<br />
<br />
= Institutions =<br />
<br />
The presented tools have been developed at<br />
<br />
[[Image:cnrs.png|60px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|60px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea2.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;<br />
[[Image:inria.png|130px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;<br />
[[Image:msr.jpg|140px|Microsoft Research|link=http://research.microsoft.com/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:MSR-INRIA_UK_CMYK.png|180px|Microsoft Research Inria Joint Centre|link=http://www.msr-inria.fr/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=75The Joint EasyCrypt-F*-CryptoVerif School 20142014-09-21T16:02:28Z<p>Pierre-yves2: Add logos for all involved institutions (bis).</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Place: Paris =<br />
Because the interest was so big, the school location has '''changed'''; we now have two locations:<br />
* Monday, Tuesday, and Friday are at: Maison Internationale, Salon David Weill, Cité internationale universitaire de Paris (Cite Universitaire), [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris 17 Boulevard Jourdan, 75014 Paris]<br />
* Wednesday and Thursday we are at: UPMC - Campus des Cordeliers, Amphitheatre 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]<br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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://alfredo.pironti.eu/research/ Alfredo Pironti], [http://pierre-yves.strub.nu/ Pierre-Yves Strub], [http://research.microsoft.com/en-us/people/nswamy/ Nikhil Swamy]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one on Wednesday and a short one on Friday.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Computationally Complete Symbolic Attacker<br />
* [http://www.loria.fr/~cortier/ Véronique Cortier] (CNRS & LORIA Nancy) - Using F* to Verify E-Voting Protocols<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Linear Refinement Type Systems<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
= Schedule =<br />
* Monday, 24 November: EasyCrypt<br />
* Tuesday, 25 November: EasyCrypt<br />
* Wednesday, 26 November: F* lectures and tutorial + Invited speakers: Cortier & Comon & Maffei (afternoon)<br />
* Thursday, 27 November: Lectures on F* + CryptoVerif (morning) + F* tutorial (afternoon)<br />
* Friday, 28 November: Invited speakers: Unruh (morning) + CryptoVerif lecture + tutorial<br />
<br />
= Hardware and software =<br />
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 by email to the participants.<br />
<br />
= Registration =<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
<br />
= Social events =<br />
We will organize a social dinner and a social lunch that are free for all registered participants.<br />
<br />
= Travel, food, and accommodation =<br />
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 (see financial support above), and for the social events (see above).<br />
<br />
= Sponsors =<br />
This school is financially supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. [http://www.cryptoforma.org.uk/ The EPSRC CryptoForma network on formal methods and cryptography] sponsors a number of grants for UK attendees.<br />
<br />
= Tools Institutions =<br />
<br />
All the presented tools have been developed at &nbsp;<br />
[[Image:cnrs.png|75px|CNRS|link=http://www.cnrs.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ens.png|75px|ENS|link=http://www.ens.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:inria.png|100px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ms.png|100px|Microsoft Research|link=http://research.microsoft.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=File:Cnrs.png&diff=74File:Cnrs.png2014-09-21T16:00:14Z<p>Pierre-yves2: CNRS Logo</p>
<hr />
<div>CNRS Logo</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=File:Ens.png&diff=73File:Ens.png2014-09-21T15:59:06Z<p>Pierre-yves2: ENS Logo</p>
<hr />
<div>ENS Logo</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=72The Joint EasyCrypt-F*-CryptoVerif School 20142014-09-19T16:26:07Z<p>Pierre-yves2: Add logos for all involved institutions.</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Place: Paris =<br />
Because the interest was so big, the school location has '''changed'''; we now have two locations:<br />
* Monday, Tuesday, and Friday are at: Maison Internationale, Salon David Weill, Cité internationale universitaire de Paris (Cite Universitaire), [https://www.google.fr/maps/place/17+Boulevard+Jourdan,+75014+Paris 17 Boulevard Jourdan, 75014 Paris]<br />
* Wednesday and Thursday we are at: UPMC - Campus des Cordeliers, Amphitheatre 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]<br />
<br />
= Abstract =<br />
The school 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.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
= Lecturers and tutorial aides =<br />
<br />
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:<br />
<br />
* '''[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]<br />
<br />
* '''[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://alfredo.pironti.eu/research/ Alfredo Pironti], [http://pierre-yves.strub.nu/ Pierre-Yves Strub], [http://research.microsoft.com/en-us/people/nswamy/ Nikhil Swamy]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited<br />
talks, a longer one on Wednesday and a short one on Friday.<br />
* [http://www.lsv.ens-cachan.fr/~comon/ Hubert Comon] (LSV, CNRS & ENS de Cachan) - Computationally Complete Symbolic Attacker<br />
* [http://www.loria.fr/~cortier/ Véronique Cortier] (CNRS & LORIA Nancy) - Using F* to Verify E-Voting Protocols<br />
* [http://www.sps.cs.uni-saarland.de/maffei/ Matteo Maffei] (Saarland University) - Linear Refinement Type Systems<br />
* [http://www.cs.ut.ee/~unruh/ Dominique Unruh] (University of Tartu) - Computational Soundness for Refinement Types<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu] ([mailto:catalin.hritcu@gmail.com contact]),<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
= Schedule =<br />
* Monday, 24 November: EasyCrypt<br />
* Tuesday, 25 November: EasyCrypt<br />
* Wednesday, 26 November: F* lectures and tutorial + Invited speakers: Cortier & Comon & Maffei (afternoon)<br />
* Thursday, 27 November: Lectures on F* + CryptoVerif (morning) + F* tutorial (afternoon)<br />
* Friday, 28 November: Invited speakers: Unruh (morning) + CryptoVerif lecture + tutorial<br />
<br />
= Hardware and software =<br />
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 by email to the participants.<br />
<br />
= Registration =<br />
* There are no registration fees for participants.<br />
* Registration deadline has passed (1 September, 2014).<br />
* The number of participants is limited.<br />
* Registrants were informed of the outcome of the selection process on 16 September, 2014.<br />
<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
* A number of the grants for UK attendees are subsidized by [http://www.cryptoforma.org.uk/ CryptoForma]; the application process is the same for all grants (part of the normal registration form above).<br />
<br />
= Social events =<br />
We will organize a social dinner and a social lunch that are free for all registered participants.<br />
<br />
= Travel, food, and accommodation =<br />
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 (see financial support above), and for the social events (see above).<br />
<br />
= Sponsors =<br />
This school is financially supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt]. [http://www.cryptoforma.org.uk/ The EPSRC CryptoForma network on formal methods and cryptography] sponsors a number of grants for UK attendees.<br />
<br />
= Tools Institutions =<br />
<br />
All the presented tools have been developed at &nbsp;<br />
[[Image:inria.png|100px|INRIA|link=http://www.inria.fr/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:imdea.png|100px|IMDEA|link=http://software.imdea.org/]] &nbsp;&nbsp;&nbsp;&nbsp;<br />
[[Image:ms.png|100px|Microsoft Research|link=http://research.microsoft.com/]]</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=File:Ms.png&diff=71File:Ms.png2014-09-19T16:17:58Z<p>Pierre-yves2: MS Logo</p>
<hr />
<div>MS Logo</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=File:Inria.png&diff=70File:Inria.png2014-09-19T16:17:10Z<p>Pierre-yves2: INRIA Logo</p>
<hr />
<div>INRIA Logo</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=File:Imdea.png&diff=69File:Imdea.png2014-09-19T16:16:44Z<p>Pierre-yves2: </p>
<hr />
<div></div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=29The Joint EasyCrypt-F*-CryptoVerif School 20142014-07-16T15:49:38Z<p>Pierre-yves2: </p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Place: INRIA office in Paris =<br />
[https://maps.google.com/maps?q=23+Avenue+d%27Italie,+75013+Paris,+France 23 Avenue d'Italie, 75013 Paris (map)]<br />
<br />
= Abstract =<br />
Formal security verification tools are slowly reaching maturity. The school 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 beautiful foundations behind these tools.<br />
<br />
'''[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.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
= Lecturers and tutorial aides:=<br />
* '''[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]<br />
<br />
* '''[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://alfredo.pironti.eu/research/ Alfredo Pironti], [http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
TBA<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu],<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
= Schedule =<br />
* Monday, 24 November: EasyCrypt<br />
* Tuesday, 25 November: EasyCrypt<br />
* Wednesday, 26 November: F*<br />
* Thursday, 27 November: Lectures on F* + CryptoVerif (morning) + F* tutorial (afternoon)<br />
* Friday, 28 November: Invited speakers (morning) + CryptoVerif lecture + tutorial<br />
<br />
= Hardware and software =<br />
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 by email to the registered participants.<br />
<br />
= Registration =<br />
* There are no registration fees for participants.<br />
* Registration deadline: 1 September, 2014<br />
* Please fill in [https://docs.google.com/forms/d/17c1wJgCLkJz2y4GH1o5ZKiB5d_Dlzmh-xQNr8zOUnhg/viewform this registration form]<br />
<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
<br />
= Social events =<br />
We will organize a social dinner and a social lunch that are free for all registered participants.<br />
<br />
= Travel, food, and accommodation =<br />
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 (see financial support above), and for the social events (see above).<br />
<br />
= Sponsors =<br />
This school is financially supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt].</div>Pierre-yves2https://wiki.inria.fr/wikis/prosecco/index.php?title=The_Joint_EasyCrypt-F*-CryptoVerif_School_2014&diff=28The Joint EasyCrypt-F*-CryptoVerif School 20142014-07-16T15:43:36Z<p>Pierre-yves2: Update EasyCrypt lecturers with the current official ones.</p>
<hr />
<div> {|align=right<br />
|__TOC__<br />
|}<br />
<br />
= Dates: 24-28 November = <br />
<br />
= Place: INRIA office in Paris =<br />
[https://maps.google.com/maps?q=23+Avenue+d%27Italie,+75013+Paris,+France 23 Avenue d'Italie, 75013 Paris (map)]<br />
<br />
= Abstract =<br />
Formal security verification tools are slowly reaching maturity. The school 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 beautiful foundations behind these tools.<br />
<br />
'''[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, and more recently the formalization of secure function evaluation, verifiable computation and key-exchange protocols.<br />
<br />
'''[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.<br />
<br />
'''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''' is an automatic protocol prover sound in the computational model. It can prove<br />
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.<br />
<br />
= Lecturers and tutorial aides:=<br />
* '''[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]<br />
<br />
* '''[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://alfredo.pironti.eu/research/ Alfredo Pironti], [http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
* '''[http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/ CryptoVerif]''': [http://prosecco.gforge.inria.fr/personal/bblanche/index-eng.html Bruno Blanchet]<br />
<br />
= Invited speakers =<br />
TBA<br />
<br />
= Organization =<br />
Anna Bednarik,<br />
[http://prosecco.gforge.inria.fr/personal/hritcu/ Cătălin Hriţcu],<br />
[http://pierre-yves.strub.nu/ Pierre-Yves Strub]<br />
<br />
= Schedule =<br />
* Monday, 24 November: EasyCrypt<br />
* Tuesday, 25 November: EasyCrypt<br />
* Wednesday, 26 November: F*<br />
* Thursday, 27 November: Lectures on F* + CryptoVerif (morning) + F* tutorial (afternoon)<br />
* Friday, 28 November: Invited speakers (morning) + CryptoVerif lecture + tutorial<br />
<br />
= Hardware and software =<br />
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 by email to the registered participants.<br />
<br />
= Registration =<br />
* There are no registration fees for participants.<br />
* Registration deadline: 1 September, 2014<br />
* Please fill in [https://docs.google.com/forms/d/17c1wJgCLkJz2y4GH1o5ZKiB5d_Dlzmh-xQNr8zOUnhg/viewform this registration form]<br />
<br />
= Financial support =<br />
* We try to offer grants covering the travel and/or accommodation costs of the participants who need it.<br />
* The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.<br />
* The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.<br />
* Participants can apply for financial support via the registration form above.<br />
<br />
= Social events =<br />
We will organize a social dinner and a social lunch that are free for all registered participants.<br />
<br />
= Travel, food, and accommodation =<br />
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 (see financial support above), and for the social events (see above).<br />
<br />
= Sponsors =<br />
This school is financially supported by the [http://prosecco.gforge.inria.fr/ Prosecco team at INRIA Paris-Rocquencourt].</div>Pierre-yves2