<?xml version="1.0" encoding="utf-8"?>
<TEI xmlns="http://www.tei-c.org/ns/1.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:hal="http://hal.archives-ouvertes.fr/" xmlns:gml="http://www.opengis.net/gml/3.3/" xmlns:gmlce="http://www.opengis.net/gml/3.3/ce" version="1.1" xsi:schemaLocation="http://www.tei-c.org/ns/1.0 http://api.archives-ouvertes.fr/documents/aofr-sword.xsd">
  <teiHeader>
    <fileDesc>
      <titleStmt>
        <title>HAL TEI export of hal-02974993</title>
      </titleStmt>
      <publicationStmt>
        <distributor>CCSD</distributor>
        <availability status="restricted">
          <licence target="https://creativecommons.org/publicdomain/zero/1.0/">CC0 1.0 - Universal</licence>
        </availability>
        <date when="2026-05-03T17:51:56+02:00"/>
      </publicationStmt>
      <sourceDesc>
        <p part="N">HAL API Platform</p>
      </sourceDesc>
    </fileDesc>
  </teiHeader>
  <text>
    <body>
      <listBibl>
        <biblFull>
          <titleStmt>
            <title xml:lang="en">The Last Mile: High-Assurance and High-Speed Cryptographic Implementations</title>
            <author role="aut">
              <persName>
                <forename type="first">José Bacelar</forename>
                <surname>Almeida</surname>
              </persName>
              <idno type="halauthorid">1743773-0</idno>
              <affiliation ref="#struct-450825"/>
              <affiliation ref="#struct-446063"/>
            </author>
            <author role="aut">
              <persName>
                <forename type="first">Manuel</forename>
                <surname>Barbosa</surname>
              </persName>
              <idno type="idhal" notation="numeric">771995</idno>
              <idno type="halauthorid" notation="string">848666-771995</idno>
              <idno type="ORCID">https://orcid.org/0000-0002-6848-5564</idno>
              <affiliation ref="#struct-450825"/>
              <affiliation ref="#struct-446063"/>
            </author>
            <author role="aut">
              <persName>
                <forename type="first">Gilles</forename>
                <surname>Barthe</surname>
              </persName>
              <idno type="halauthorid">117487-0</idno>
              <affiliation ref="#struct-81272"/>
              <affiliation ref="#struct-576324"/>
            </author>
            <author role="aut">
              <persName>
                <forename type="first">Benjamin</forename>
                <surname>Grégoire</surname>
              </persName>
              <email type="md5">af1754b2f00130c38090482da4c1da5e</email>
              <email type="domain">inria.fr</email>
              <idno type="idhal" notation="string">benjamin-gregoire</idno>
              <idno type="idhal" notation="numeric">1695</idno>
              <idno type="halauthorid" notation="string">11069-1695</idno>
              <idno type="IDREF">https://www.idref.fr/089057058</idno>
              <idno type="ORCID">https://orcid.org/0000-0001-6650-9924</idno>
              <affiliation ref="#struct-573775"/>
            </author>
            <author role="aut">
              <persName>
                <forename type="first">Adrien</forename>
                <surname>Koutsos</surname>
              </persName>
              <email type="md5">4a81970f6aefef377d1522690af14a2a</email>
              <email type="domain">inria.fr</email>
              <idno type="idhal" notation="string">adrien-koutsos</idno>
              <idno type="idhal" notation="numeric">751744</idno>
              <idno type="halauthorid" notation="string">46537-751744</idno>
              <idno type="ARXIV">https://arxiv.org/a/koutsos_a_1</idno>
              <idno type="ORCID">https://orcid.org/0000-0002-5891-154X</idno>
              <affiliation ref="#struct-1042689"/>
            </author>
            <author role="aut">
              <persName>
                <forename type="first">Vincent</forename>
                <surname>Laporte</surname>
              </persName>
              <email type="md5">33e4fbd64fa18c3fc30952bdf41b25cf</email>
              <email type="domain">inria.fr</email>
              <idno type="idhal" notation="string">vincent-laporte</idno>
              <idno type="idhal" notation="numeric">738000</idno>
              <idno type="halauthorid" notation="string">51466-738000</idno>
              <idno type="IDREF">https://www.idref.fr/191832324</idno>
              <affiliation ref="#struct-445522"/>
            </author>
            <author role="aut">
              <persName>
                <forename type="first">Tiago</forename>
                <surname>Oliveira</surname>
              </persName>
              <idno type="halauthorid">387613-0</idno>
              <affiliation ref="#struct-450825"/>
              <affiliation ref="#struct-446063"/>
            </author>
            <author role="aut">
              <persName>
                <forename type="first">Pierre-Yves</forename>
                <surname>Strub</surname>
              </persName>
              <idno type="halauthorid">216463-0</idno>
              <affiliation ref="#struct-2071"/>
            </author>
            <editor role="depositor">
              <persName>
                <forename>Vincent</forename>
                <surname>Laporte</surname>
              </persName>
              <email type="md5">33e4fbd64fa18c3fc30952bdf41b25cf</email>
              <email type="domain">inria.fr</email>
            </editor>
            <funder ref="#projanr-48451"/>
          </titleStmt>
          <editionStmt>
            <edition n="v1" type="current">
              <date type="whenSubmitted">2020-10-22 11:50:56</date>
              <date type="whenModified">2025-11-04 12:00:17</date>
              <date type="whenReleased">2020-10-22 11:50:56</date>
              <date type="whenProduced">2020-05-18</date>
              <ref type="externalLink" target="http://arxiv.org/pdf/1904.04606"/>
            </edition>
            <respStmt>
              <resp>contributor</resp>
              <name key="944155">
                <persName>
                  <forename>Vincent</forename>
                  <surname>Laporte</surname>
                </persName>
                <email type="md5">33e4fbd64fa18c3fc30952bdf41b25cf</email>
                <email type="domain">inria.fr</email>
              </name>
            </respStmt>
          </editionStmt>
          <publicationStmt>
            <distributor>CCSD</distributor>
            <idno type="halId">hal-02974993</idno>
            <idno type="halUri">https://hal.univ-lorraine.fr/hal-02974993</idno>
            <idno type="halBibtex">almeida:hal-02974993</idno>
            <idno type="halRefHtml">&lt;i&gt;SP 2020 - 41st IEEE Symposium on Security and Privacy&lt;/i&gt;, May 2020, San Francisco / Virtual, United States. pp.965-982, &lt;a target="_blank" href="https://dx.doi.org/10.1109/SP40000.2020.00028"&gt;&amp;#x27E8;10.1109/SP40000.2020.00028&amp;#x27E9;&lt;/a&gt;</idno>
            <idno type="halRef">SP 2020 - 41st IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.965-982, &amp;#x27E8;10.1109/SP40000.2020.00028&amp;#x27E9;</idno>
            <availability status="restricted"/>
          </publicationStmt>
          <seriesStmt>
            <idno type="stamp" n="X">École polytechnique</idno>
            <idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno>
            <idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno>
            <idno type="stamp" n="ENS-CACHAN">Ecole Normale Supérieure de Cachan</idno>
            <idno type="stamp" n="INRIA-SOPHIA">INRIA Sophia Antipolis - Méditerranée</idno>
            <idno type="stamp" n="LIX" corresp="X">Laboratoire d'informatique de l'Ecole polytechnique</idno>
            <idno type="stamp" n="LIX-MAX" corresp="LIX">Max</idno>
            <idno type="stamp" n="INRIASO">INRIA-SOPHIA</idno>
            <idno type="stamp" n="X-DEP-INFO">Département d'informatique de l’École polytechnique</idno>
            <idno type="stamp" n="INRIA_TEST">INRIA - Institut National de Recherche en Informatique et en Automatique</idno>
            <idno type="stamp" n="LORIA2">Publications du LORIA</idno>
            <idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno>
            <idno type="stamp" n="TESTALAIN1">TESTALAIN1</idno>
            <idno type="stamp" n="CENTRALESUPELEC">Ecole CentraleSupélec</idno>
            <idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno>
            <idno type="stamp" n="INRIA2">INRIA 2</idno>
            <idno type="stamp" n="LORIA">Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno>
            <idno type="stamp" n="LORIA-FM" corresp="LORIA">Department of Formal methods</idno>
            <idno type="stamp" n="UNIV-PARIS-SACLAY">Université Paris-Saclay</idno>
            <idno type="stamp" n="UNIV-COTEDAZUR">Université Côte d'Azur</idno>
            <idno type="stamp" n="IP_PARIS">Institut Polytechnique de Paris</idno>
            <idno type="stamp" n="TEST-HALCNRS">Collection test HAL CNRS</idno>
            <idno type="stamp" n="UNIVERSITE-PARIS-SACLAY" corresp="UNIV-PARIS-SACLAY">Université Paris-Saclay</idno>
            <idno type="stamp" n="ANR">ANR</idno>
            <idno type="stamp" n="LSV-AUTO">Laboratoire Spécification et Vérification</idno>
            <idno type="stamp" n="FARMAN">Institut Farman</idno>
            <idno type="stamp" n="ENS-PARIS-SACLAY">Ecole Normale Supérieure paris-Saclay</idno>
            <idno type="stamp" n="ENS-PSACLAY">Ecole Normale Supérieure Paris-Saclay</idno>
            <idno type="stamp" n="GS-COMPUTER-SCIENCE">Graduate School Computer Science</idno>
            <idno type="stamp" n="LMF">Laboratoire Méthodes Formelles</idno>
            <idno type="stamp" n="LMF-SECURITY">Sécurité</idno>
            <idno type="stamp" n="INRIA-ALLEMAGNE">INRIA-ALLEMAGNE</idno>
            <idno type="stamp" n="DEPARTEMENT-DE-MATHEMATIQUES">Collection du Département de Mathématiques</idno>
            <idno type="stamp" n="IP-PARIS-INFORMATIQUE-DONNEES-ET-IA">IP Paris Département d'Informatique, de Données et d'IA</idno>
            <idno type="stamp" n="AM2I-UL">Pôle scientifique Automatique, Mathématiques, Informatique et leurs Intéractions de l'Université de Lorraine</idno>
          </seriesStmt>
          <notesStmt>
            <note type="audience" n="2">International</note>
            <note type="invited" n="0">No</note>
            <note type="popular" n="0">No</note>
            <note type="peer" n="1">Yes</note>
            <note type="proceedings" n="1">Yes</note>
          </notesStmt>
          <sourceDesc>
            <biblStruct>
              <analytic>
                <title xml:lang="en">The Last Mile: High-Assurance and High-Speed Cryptographic Implementations</title>
                <author role="aut">
                  <persName>
                    <forename type="first">José Bacelar</forename>
                    <surname>Almeida</surname>
                  </persName>
                  <idno type="halauthorid">1743773-0</idno>
                  <affiliation ref="#struct-450825"/>
                  <affiliation ref="#struct-446063"/>
                </author>
                <author role="aut">
                  <persName>
                    <forename type="first">Manuel</forename>
                    <surname>Barbosa</surname>
                  </persName>
                  <idno type="idhal" notation="numeric">771995</idno>
                  <idno type="halauthorid" notation="string">848666-771995</idno>
                  <idno type="ORCID">https://orcid.org/0000-0002-6848-5564</idno>
                  <affiliation ref="#struct-450825"/>
                  <affiliation ref="#struct-446063"/>
                </author>
                <author role="aut">
                  <persName>
                    <forename type="first">Gilles</forename>
                    <surname>Barthe</surname>
                  </persName>
                  <idno type="halauthorid">117487-0</idno>
                  <affiliation ref="#struct-81272"/>
                  <affiliation ref="#struct-576324"/>
                </author>
                <author role="aut">
                  <persName>
                    <forename type="first">Benjamin</forename>
                    <surname>Grégoire</surname>
                  </persName>
                  <email type="md5">af1754b2f00130c38090482da4c1da5e</email>
                  <email type="domain">inria.fr</email>
                  <idno type="idhal" notation="string">benjamin-gregoire</idno>
                  <idno type="idhal" notation="numeric">1695</idno>
                  <idno type="halauthorid" notation="string">11069-1695</idno>
                  <idno type="IDREF">https://www.idref.fr/089057058</idno>
                  <idno type="ORCID">https://orcid.org/0000-0001-6650-9924</idno>
                  <affiliation ref="#struct-573775"/>
                </author>
                <author role="aut">
                  <persName>
                    <forename type="first">Adrien</forename>
                    <surname>Koutsos</surname>
                  </persName>
                  <email type="md5">4a81970f6aefef377d1522690af14a2a</email>
                  <email type="domain">inria.fr</email>
                  <idno type="idhal" notation="string">adrien-koutsos</idno>
                  <idno type="idhal" notation="numeric">751744</idno>
                  <idno type="halauthorid" notation="string">46537-751744</idno>
                  <idno type="ARXIV">https://arxiv.org/a/koutsos_a_1</idno>
                  <idno type="ORCID">https://orcid.org/0000-0002-5891-154X</idno>
                  <affiliation ref="#struct-1042689"/>
                </author>
                <author role="aut">
                  <persName>
                    <forename type="first">Vincent</forename>
                    <surname>Laporte</surname>
                  </persName>
                  <email type="md5">33e4fbd64fa18c3fc30952bdf41b25cf</email>
                  <email type="domain">inria.fr</email>
                  <idno type="idhal" notation="string">vincent-laporte</idno>
                  <idno type="idhal" notation="numeric">738000</idno>
                  <idno type="halauthorid" notation="string">51466-738000</idno>
                  <idno type="IDREF">https://www.idref.fr/191832324</idno>
                  <affiliation ref="#struct-445522"/>
                </author>
                <author role="aut">
                  <persName>
                    <forename type="first">Tiago</forename>
                    <surname>Oliveira</surname>
                  </persName>
                  <idno type="halauthorid">387613-0</idno>
                  <affiliation ref="#struct-450825"/>
                  <affiliation ref="#struct-446063"/>
                </author>
                <author role="aut">
                  <persName>
                    <forename type="first">Pierre-Yves</forename>
                    <surname>Strub</surname>
                  </persName>
                  <idno type="halauthorid">216463-0</idno>
                  <affiliation ref="#struct-2071"/>
                </author>
              </analytic>
              <monogr>
                <meeting>
                  <title>SP 2020 - 41st IEEE Symposium on Security and Privacy</title>
                  <date type="start">2020-05-18</date>
                  <date type="end">2020-05-21</date>
                  <settlement>San Francisco / Virtual</settlement>
                  <country key="US">United States</country>
                </meeting>
                <imprint>
                  <publisher>IEEE</publisher>
                  <biblScope unit="pp">965-982</biblScope>
                  <date type="datePub">2020-05</date>
                </imprint>
              </monogr>
              <idno type="arxiv">1904.04606</idno>
              <idno type="doi">10.1109/SP40000.2020.00028</idno>
              <ref type="publisher">https://www.ieee-security.org/TC/SP2020/index.html</ref>
            </biblStruct>
          </sourceDesc>
          <profileDesc>
            <langUsage>
              <language ident="en">English</language>
            </langUsage>
            <textClass>
              <classCode scheme="halDomain" n="info.info-pl">Computer Science [cs]/Programming Languages [cs.PL]</classCode>
              <classCode scheme="halDomain" n="info.info-cr">Computer Science [cs]/Cryptography and Security [cs.CR]</classCode>
              <classCode scheme="halTypology" n="COMM">Conference papers</classCode>
              <classCode scheme="halOldTypology" n="COMM">Conference papers</classCode>
              <classCode scheme="halTreeTypology" n="COMM">Conference papers</classCode>
            </textClass>
            <abstract xml:lang="en">
              <p>We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as hand-written assembly. We illustrate our approach using ChaCha20-Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outperform the fastest non-verified code. We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which offers a versatile verification infrastructure that supports proofs of functional correctness and equivalence checking. Neither of these tools had been used for functional correctness before. Taken together, these infrastructures empower programmers to develop efficient and verified implementations by "game hopping", starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking.We also make several contributions of independent interest, including a new and extensible verified compiler for Jasmin, with a richer memory model and support for vectorized instructions, and a new embedding of Jasmin in EasyCrypt.</p>
            </abstract>
          </profileDesc>
        </biblFull>
      </listBibl>
    </body>
    <back>
      <listOrg type="structures">
        <org type="institution" xml:id="struct-450825" status="VALID">
          <idno type="ROR">https://ror.org/05fa8ka61</idno>
          <orgName>Institute for Systems and Computer Engineering, Technology and Science [Porto]</orgName>
          <orgName type="acronym">INESC TEC</orgName>
          <desc>
            <address>
              <addrLine>FEUP campus Rua Dr. Roberto Frias 4200 - 465 Porto Portugal</addrLine>
              <country key="PT"/>
            </address>
            <ref type="url">http://www.inesctec.pt/ip-en</ref>
          </desc>
        </org>
        <org type="institution" xml:id="struct-446063" status="VALID">
          <orgName>Faculdade de Ciências da Universidade do Porto</orgName>
          <orgName type="acronym">FCUP</orgName>
          <desc>
            <address>
              <addrLine>Rua do Campo Alegre, 4169-007 Porto</addrLine>
              <country key="PT"/>
            </address>
            <ref type="url">https://www.fc.up.pt/</ref>
          </desc>
          <listRelation>
            <relation active="#struct-19144" type="direct"/>
          </listRelation>
        </org>
        <org type="institution" xml:id="struct-81272" status="VALID">
          <idno type="ROR">https://ror.org/04xvfkh51</idno>
          <orgName>Institute IMDEA Software [Madrid]</orgName>
          <desc>
            <address>
              <addrLine>Campus de Montegancedo 28223 Pozuelo de Alarcón Madrid</addrLine>
              <country key="ES"/>
            </address>
            <ref type="url">http://software.imdea.org/</ref>
          </desc>
        </org>
        <org type="institution" xml:id="struct-576324" status="VALID">
          <orgName>Max Planck Institute for Security and Privacy [Bochum]</orgName>
          <orgName type="acronym">MPI SP</orgName>
          <desc>
            <address>
              <country key="DE"/>
            </address>
          </desc>
        </org>
        <org type="researchteam" xml:id="struct-573775" status="VALID">
          <idno type="RNSR">201923413W</idno>
          <idno type="ROR">https://ror.org/046v7pr94</idno>
          <orgName>Sûreté du logiciel et Preuves Mathématiques Formalisées</orgName>
          <orgName type="acronym">STAMP</orgName>
          <date type="start">2019-11-01</date>
          <date type="end">2028-12-31</date>
          <desc>
            <address>
              <addrLine>2004 route des Lucioles BP 93 06902 Sophia Antipolis</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">https://www.inria.fr/equipes/stamp</ref>
          </desc>
          <listRelation>
            <relation active="#struct-34586" type="direct"/>
            <relation active="#struct-300009" type="indirect"/>
          </listRelation>
        </org>
        <org type="laboratory" xml:id="struct-1042689" status="OLD">
          <orgName>Laboratoire Spécification et Vérification</orgName>
          <orgName type="acronym">LSV</orgName>
          <date type="start">2020-01-01</date>
          <date type="end">2020-12-31</date>
          <desc>
            <address>
              <addrLine>4, avenue des Sciences, 91190, Gif-sur-Yvette</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.lsv.fr/</ref>
          </desc>
          <listRelation>
            <relation active="#struct-419361" type="direct"/>
            <relation name="UMR8643" active="#struct-441569" type="direct"/>
            <relation active="#struct-523723" type="direct"/>
          </listRelation>
        </org>
        <org type="researchteam" xml:id="struct-445522" status="VALID">
          <idno type="RNSR">201622052E</idno>
          <idno type="ROR">https://ror.org/019yhsq25</idno>
          <orgName>Proof techniques for security protocols</orgName>
          <orgName type="acronym">PESTO</orgName>
          <date type="start">2016-01-01</date>
          <date type="end">2028-10-31</date>
          <desc>
            <address>
              <addrLine>615 Rue du Jardin-Botanique, 54600 Villers-lès-Nancy</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.inria.fr/equipes/pesto</ref>
          </desc>
          <listRelation>
            <relation active="#struct-129671" type="direct"/>
            <relation active="#struct-300009" type="indirect"/>
            <relation active="#struct-423084" type="direct"/>
            <relation active="#struct-206040" type="indirect"/>
            <relation active="#struct-411575" type="indirect"/>
            <relation active="#struct-413289" type="indirect"/>
            <relation name="UMR7503" active="#struct-441569" type="indirect"/>
          </listRelation>
        </org>
        <org type="laboratory" xml:id="struct-2071" status="VALID">
          <idno type="IdRef">196509955</idno>
          <idno type="ISNI">0000000403673665</idno>
          <idno type="RNSR">200519331V</idno>
          <idno type="ROR">https://ror.org/04afed728</idno>
          <idno type="Wikidata">Q16009025</idno>
          <orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName>
          <orgName type="acronym">LIX</orgName>
          <date type="start">2005-01-01</date>
          <desc>
            <address>
              <addrLine>1 Rue Honoré d’Estienne d’Orves, Bâtiment Alain Turing, 91120 Palaiseau</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">https://www.lix.polytechnique.fr/</ref>
          </desc>
          <listRelation>
            <relation active="#struct-300340" type="direct"/>
            <relation active="#struct-563936" type="indirect"/>
            <relation name="UMR7161" active="#struct-441569" type="direct"/>
          </listRelation>
        </org>
        <org type="regroupinstitution" xml:id="struct-19144" status="VALID">
          <orgName>Universidade do Porto = University of Porto</orgName>
          <date type="start">1911-01-01</date>
          <desc>
            <address>
              <addrLine>Praça de Gomes Teixeira, 4099-002 Porto</addrLine>
              <country key="PT"/>
            </address>
            <ref type="url">https://sigarra.up.pt/up/pt/</ref>
          </desc>
        </org>
        <org type="laboratory" xml:id="struct-34586" status="VALID">
          <idno type="RNSR">198318250R</idno>
          <idno type="ROR">https://ror.org/01nzkaw91</idno>
          <orgName>Centre Inria d'Université Côte d'Azur</orgName>
          <desc>
            <address>
              <addrLine>2004 route des Lucioles BP 93 06902 Sophia Antipolis</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.inria.fr/centre/sophia/</ref>
          </desc>
          <listRelation>
            <relation active="#struct-300009" type="direct"/>
          </listRelation>
        </org>
        <org type="institution" xml:id="struct-300009" status="VALID">
          <idno type="ROR">https://ror.org/02kvxyf05</idno>
          <orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
          <orgName type="acronym">Inria</orgName>
          <desc>
            <address>
              <addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.inria.fr/en/</ref>
          </desc>
        </org>
        <org type="institution" xml:id="struct-419361" status="VALID">
          <idno type="IdRef">241345251</idno>
          <idno type="ROR">https://ror.org/03xjwb503</idno>
          <orgName>Université Paris-Saclay</orgName>
          <desc>
            <address>
              <addrLine>Bâtiment Bréguet, 3 Rue Joliot Curie 2e ét, 91190 Gif-sur-Yvette</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">https://www.universite-paris-saclay.fr/fr</ref>
          </desc>
        </org>
        <org type="regroupinstitution" xml:id="struct-441569" status="VALID">
          <idno type="IdRef">02636817X</idno>
          <idno type="ISNI">0000000122597504</idno>
          <idno type="ROR">https://ror.org/02feahw73</idno>
          <orgName>Centre National de la Recherche Scientifique</orgName>
          <orgName type="acronym">CNRS</orgName>
          <date type="start">1939-10-19</date>
          <desc>
            <address>
              <country key="FR"/>
            </address>
            <ref type="url">https://www.cnrs.fr/</ref>
          </desc>
        </org>
        <org type="institution" xml:id="struct-523723" status="VALID">
          <idno type="ROR">https://ror.org/00hx6zz33</idno>
          <orgName>Ecole Normale Supérieure  Paris-Saclay</orgName>
          <orgName type="acronym">ENS Paris Saclay</orgName>
          <desc>
            <address>
              <addrLine>4 avenue des Sciences, 91190 Gif-sur-Yvette</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://ens-paris-saclay.fr/</ref>
          </desc>
        </org>
        <org type="laboratory" xml:id="struct-129671" status="VALID">
          <idno type="RNSR">198618246Y</idno>
          <idno type="ROR">https://ror.org/03fcjvn64</idno>
          <orgName>Centre Inria de l'Université de Lorraine</orgName>
          <desc>
            <address>
              <addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.inria.fr/nancy</ref>
          </desc>
          <listRelation>
            <relation active="#struct-300009" type="direct"/>
          </listRelation>
        </org>
        <org type="department" xml:id="struct-423084" status="VALID">
          <orgName>Department of Formal Methods</orgName>
          <orgName type="acronym">LORIA - FM</orgName>
          <desc>
            <address>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.loria.fr/en/research/departments/formal-methods/</ref>
          </desc>
          <listRelation>
            <relation active="#struct-206040" type="direct"/>
            <relation active="#struct-300009" type="indirect"/>
            <relation active="#struct-411575" type="indirect"/>
            <relation active="#struct-413289" type="indirect"/>
            <relation name="UMR7503" active="#struct-441569" type="indirect"/>
          </listRelation>
        </org>
        <org type="laboratory" xml:id="struct-206040" status="VALID">
          <idno type="IdRef">067077927</idno>
          <idno type="ISNI">0000000121795429</idno>
          <idno type="RNSR">198912571S</idno>
          <idno type="IdUnivLorraine">[UL]RSI--</idno>
          <idno type="ROR">https://ror.org/02vnf0c38</idno>
          <orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
          <orgName type="acronym">LORIA</orgName>
          <date type="start">2012-01-01</date>
          <desc>
            <address>
              <addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.loria.fr</ref>
          </desc>
          <listRelation>
            <relation active="#struct-300009" type="direct"/>
            <relation active="#struct-411575" type="direct"/>
            <relation active="#struct-413289" type="direct"/>
            <relation name="UMR7503" active="#struct-441569" type="direct"/>
          </listRelation>
        </org>
        <org type="institution" xml:id="struct-411575" status="VALID">
          <idno type="IdRef">184443237</idno>
          <idno type="ROR">https://ror.org/019tcpt25</idno>
          <orgName>CentraleSupélec</orgName>
          <desc>
            <address>
              <addrLine>3, rue Joliot Curie,Plateau de Moulon,91192 GIF-SUR-YVETTE Cedex</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.centralesupelec.fr</ref>
          </desc>
        </org>
        <org type="institution" xml:id="struct-413289" status="VALID">
          <idno type="IdRef">157040569</idno>
          <idno type="IdUnivLorraine">[UL]100--</idno>
          <idno type="ROR">https://ror.org/04vfs2w97</idno>
          <orgName>Université de Lorraine</orgName>
          <orgName type="acronym">UL</orgName>
          <date type="start">2012-01-01</date>
          <desc>
            <address>
              <addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">http://www.univ-lorraine.fr/</ref>
          </desc>
        </org>
        <org type="institution" xml:id="struct-300340" status="VALID">
          <idno type="IdRef">027309320</idno>
          <idno type="ISNI">0000000121581279</idno>
          <idno type="ROR">https://ror.org/05hy3tk52</idno>
          <idno type="Wikidata">Q273626</idno>
          <orgName>École polytechnique</orgName>
          <orgName type="acronym">X</orgName>
          <date type="start">1794-03-11</date>
          <desc>
            <address>
              <addrLine>Route de Saclay, 91128 Palaiseau Cedex</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">https://www.polytechnique.edu/</ref>
          </desc>
          <listRelation>
            <relation active="#struct-563936" type="direct"/>
          </listRelation>
        </org>
        <org type="regroupinstitution" xml:id="struct-563936" status="VALID">
          <idno type="IdRef">238327159</idno>
          <idno type="ISNI">0000000502717600</idno>
          <idno type="ROR">https://ror.org/042tfbd02</idno>
          <idno type="Wikidata">Q48759778</idno>
          <orgName>Institut Polytechnique de Paris</orgName>
          <orgName type="acronym">IP Paris</orgName>
          <date type="start">2019-06-02</date>
          <desc>
            <address>
              <addrLine>Route de Saclay, 91120 Palaiseau Cedex, France</addrLine>
              <country key="FR"/>
            </address>
            <ref type="url">https://www.ip-paris.fr</ref>
          </desc>
        </org>
      </listOrg>
      <listOrg type="projects">
        <org type="anrProject" xml:id="projanr-48451" status="VALID">
          <idno type="anr">ANR-18-CE25-0014</idno>
          <idno type="program">APPEL À PROJETS GÉNÉRIQUE 2018</idno>
          <orgName>scrypt</orgName>
          <desc>Compilation sécurisée de primitives cryptographiques</desc>
          <date type="start">2018</date>
        </org>
      </listOrg>
    </back>
  </text>
</TEI>