Formal Verification of Advanced Families of Security Protocols: E-Voting and APIs
Identifieur interne : 000809 ( Hal/Checkpoint ); précédent : 000808; suivant : 000810Formal Verification of Advanced Families of Security Protocols: E-Voting and APIs
Auteurs : Cyrille Wiedling [France]Source :
Descripteurs français
English descriptors
- mix :
Abstract
For a long time now, formal methods have been successfully used to analyze security protocols. Several tools have even been developed to tackle automatically different proof techniques and, therefore, to ease the verification of such protocols. However, when it comes to electronic voting and APIs, current tools tend to reach their limits because they can’t handle some cryptographic primitives (e.g. homomorphic encryption), or the security properties (e.g. ballot secrecy), involved in those protocols.In this thesis, we first work on two cases studies of existing and deployed systems: a Norwegian e-voting protocol and a CNRS boardroom voting protocol. These two protocols are analyzed using the applied pi-calculus model and we discuss in details about their security properties, in different corruption scenarios. Even though this part provides several reusable results, it also shows the complexity to prove them by hand and, therefore, underlying a real need for automation in those proofs.The third part of this thesis focuses on a possible lead in direction of this needed automation: type- systems. Indeed, we build upon a recent work describing a new type-system designed to deal with equivalence properties, in order to apply this on the verification of equivalence-based properties in elec- tronic voting like ballot-secrecy. We present an application of this method through the example of Helios, a well-known, web-based, and open-audit, e-voting system.Another family of advanced security protocols are APIs: secure interfaces devoted to allow access to some information stored into a secured trusted hardware without leaking it outside. Such protocols are not immune to attacks; in fact, recent work seems to show the opposite. In the second part of this thesis, we provide a new design for APIs, including a revocation functionality, which is not always considered. In addition, we include a fully formal analysis of this API allowing that a malicious combination of API’s commands does not leak any key, even when the adversary may brute-force some of them.
Url:
Links toward previous steps (curation, corpus...)
Links to Exploration step
Hal:tel-01107718Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Formal Verification of Advanced Families of Security Protocols: E-Voting and APIs</title><title xml:lang="fr">Vérification formelle de familles avancées de protocoles de sécurité : vote électronique et API</title><author><name sortKey="Wiedling, Cyrille" sort="Wiedling, Cyrille" uniqKey="Wiedling C" first="Cyrille" last="Wiedling">Cyrille Wiedling</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2366" status="OLD"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</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"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><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"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</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"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName><placeName><settlement type="city" wicri:auto="siege">Belfort</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de technologie de Belfort-Montbéliard</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:tel-01107718</idno><idno type="halId">tel-01107718</idno><idno type="halUri">https://tel.archives-ouvertes.fr/tel-01107718</idno><idno type="url">https://tel.archives-ouvertes.fr/tel-01107718</idno><date when="2014-11-21">2014-11-21</date><idno type="wicri:Area/Hal/Corpus">002385</idno><idno type="wicri:Area/Hal/Curation">002385</idno><idno type="wicri:Area/Hal/Checkpoint">000809</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000809</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Formal Verification of Advanced Families of Security Protocols: E-Voting and APIs</title><title xml:lang="fr">Vérification formelle de familles avancées de protocoles de sécurité : vote électronique et API</title><author><name sortKey="Wiedling, Cyrille" sort="Wiedling, Cyrille" uniqKey="Wiedling C" first="Cyrille" last="Wiedling">Cyrille Wiedling</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2366" status="OLD"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</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"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><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"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</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"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName><placeName><settlement type="city" wicri:auto="siege">Belfort</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de technologie de Belfort-Montbéliard</orgName></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>APIs</term><term>E-Voting</term><term>Formal Methods</term><term>Protocols</term><term>Security</term><term>Type-Systems</term></keywords><keywords scheme="mix" xml:lang="fr"><term>Méthodes Formelles</term><term>Protocoles</term><term>Sécurité</term><term>Systèmes de Types</term><term>Vote Electronique</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">For a long time now, formal methods have been successfully used to analyze security protocols. Several tools have even been developed to tackle automatically different proof techniques and, therefore, to ease the verification of such protocols. However, when it comes to electronic voting and APIs, current tools tend to reach their limits because they can’t handle some cryptographic primitives (e.g. homomorphic encryption), or the security properties (e.g. ballot secrecy), involved in those protocols.In this thesis, we first work on two cases studies of existing and deployed systems: a Norwegian e-voting protocol and a CNRS boardroom voting protocol. These two protocols are analyzed using the applied pi-calculus model and we discuss in details about their security properties, in different corruption scenarios. Even though this part provides several reusable results, it also shows the complexity to prove them by hand and, therefore, underlying a real need for automation in those proofs.The third part of this thesis focuses on a possible lead in direction of this needed automation: type- systems. Indeed, we build upon a recent work describing a new type-system designed to deal with equivalence properties, in order to apply this on the verification of equivalence-based properties in elec- tronic voting like ballot-secrecy. We present an application of this method through the example of Helios, a well-known, web-based, and open-audit, e-voting system.Another family of advanced security protocols are APIs: secure interfaces devoted to allow access to some information stored into a secured trusted hardware without leaking it outside. Such protocols are not immune to attacks; in fact, recent work seems to show the opposite. In the second part of this thesis, we provide a new design for APIs, including a revocation functionality, which is not always considered. In addition, we include a fully formal analysis of this API allowing that a malicious combination of API’s commands does not leak any key, even when the adversary may brute-force some of them.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="en">Formal Verification of Advanced Families of Security Protocols: E-Voting and APIs</title><title xml:lang="fr">Vérification formelle de familles avancées de protocoles de sécurité : vote électronique et API</title><author role="aut"><persName><forename type="first">Cyrille</forename><surname>Wiedling</surname></persName><email>cyrille.wiedling@inria.fr</email><idno type="halauthor">654073</idno><affiliation ref="#struct-2366"></affiliation></author><editor role="depositor"><persName><forename>Cyrille</forename><surname>Wiedling</surname></persName><email>cyrille.wiedling@inria.fr</email></editor><funder ref="#projeurop-88798"></funder></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2015-01-21 14:16:12</date><date type="whenModified">2016-05-19 01:14:11</date><date type="whenReleased">2015-01-21 16:48:42</date><date type="whenProduced">2014-11-21</date><date type="whenEndEmbargoed">2015-01-21</date><ref type="file" target="https://tel.archives-ouvertes.fr/tel-01107718/document"><date notBefore="2015-01-21"></date></ref><ref type="file" n="1" target="https://tel.archives-ouvertes.fr/tel-01107718/file/these_main.pdf"><date notBefore="2015-01-21"></date></ref></edition><respStmt><resp>contributor</resp><name key="166219"><persName><forename>Cyrille</forename><surname>Wiedling</surname></persName><email>cyrille.wiedling@inria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">tel-01107718</idno><idno type="halUri">https://tel.archives-ouvertes.fr/tel-01107718</idno><idno type="halBibtex">wiedling:tel-01107718</idno><idno type="halRefHtml">Cryptography and Security [cs.CR]. Université de Lorraine, 2014. English</idno><idno type="halRef">Cryptography and Security [cs.CR]. Université de Lorraine, 2014. English</idno></publicationStmt><seriesStmt><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="UNIV-FCOMTE">Université de Franche-Comté</idno><idno type="stamp" n="INPL">Institut National Polytechnique de Lorraine</idno><idno type="stamp" n="OPENAIRE">OpenAIRE</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</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="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="INRIA2">INRIA 2</idno><idno type="stamp" n="LABO-LORIA-SET" p="LORIA">LABO-LORIA-SET</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno><idno type="stamp" n="UNIV-BM">Université de Technologie de Belfort-Montbeliard</idno><idno type="stamp" n="ENSMM">Ecole Nationale Supérieure de Mécanique et des Microtechniques</idno><idno type="stamp" n="FEMTO-ST" p="UNIV-FCOMTE">Franche-Comté Electronique, Mécanique, Thermique et Optique - Sciences et Technologies</idno><idno type="stamp" n="UNIV-BM-THESE">Université de Technologie de Belfort-Montbeliard</idno></seriesStmt><notesStmt></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Formal Verification of Advanced Families of Security Protocols: E-Voting and APIs</title><title xml:lang="fr">Vérification formelle de familles avancées de protocoles de sécurité : vote électronique et API</title><author role="aut"><persName><forename type="first">Cyrille</forename><surname>Wiedling</surname></persName><email>cyrille.wiedling@inria.fr</email><idno type="halAuthorId">654073</idno><affiliation ref="#struct-2366"></affiliation></author></analytic><monogr><imprint><date type="dateDefended">2014-11-21</date></imprint><authority type="institution">Université de Lorraine</authority><authority type="school">IAEM (Informatique, Automatique, Électronique - Électrotechnique, Mathématiques) Lorraine</authority><authority type="supervisor">Véronique Cortier</authority><authority type="jury">Frédéric Cuppens</authority><authority type="jury">Bruno Blanchet</authority><authority type="jury">Cas Cremers</authority><authority type="jury">Ralf Küsters</authority><authority type="jury">Yassine Lakhnech</authority><authority type="jury">Pierre-Etienne Moreau</authority><authority type="jury">Benjamin Morin</authority></monogr></biblStruct></sourceDesc><profileDesc><langUsage><language ident="en">English</language></langUsage><textClass><keywords scheme="author"><term xml:lang="en">Formal Methods</term><term xml:lang="en">Type-Systems</term><term xml:lang="en">E-Voting</term><term xml:lang="en">APIs</term><term xml:lang="en">Protocols</term><term xml:lang="en">Security</term><term xml:lang="fr">Protocoles</term><term xml:lang="fr">Systèmes de Types</term><term xml:lang="fr">Sécurité</term><term xml:lang="fr">Méthodes Formelles</term><term xml:lang="fr">Vote Electronique</term></keywords><classCode scheme="halDomain" n="info.info-cr">Computer Science [cs]/Cryptography and Security [cs.CR]</classCode><classCode scheme="halTypology" n="THESE">Theses</classCode></textClass><abstract xml:lang="en">For a long time now, formal methods have been successfully used to analyze security protocols. Several tools have even been developed to tackle automatically different proof techniques and, therefore, to ease the verification of such protocols. However, when it comes to electronic voting and APIs, current tools tend to reach their limits because they can’t handle some cryptographic primitives (e.g. homomorphic encryption), or the security properties (e.g. ballot secrecy), involved in those protocols.In this thesis, we first work on two cases studies of existing and deployed systems: a Norwegian e-voting protocol and a CNRS boardroom voting protocol. These two protocols are analyzed using the applied pi-calculus model and we discuss in details about their security properties, in different corruption scenarios. Even though this part provides several reusable results, it also shows the complexity to prove them by hand and, therefore, underlying a real need for automation in those proofs.The third part of this thesis focuses on a possible lead in direction of this needed automation: type- systems. Indeed, we build upon a recent work describing a new type-system designed to deal with equivalence properties, in order to apply this on the verification of equivalence-based properties in elec- tronic voting like ballot-secrecy. We present an application of this method through the example of Helios, a well-known, web-based, and open-audit, e-voting system.Another family of advanced security protocols are APIs: secure interfaces devoted to allow access to some information stored into a secured trusted hardware without leaking it outside. Such protocols are not immune to attacks; in fact, recent work seems to show the opposite. In the second part of this thesis, we provide a new design for APIs, including a revocation functionality, which is not always considered. In addition, we include a fully formal analysis of this API allowing that a malicious combination of API’s commands does not leak any key, even when the adversary may brute-force some of them.</abstract><abstract xml:lang="fr">Les méthodes formelles ont depuis longtemps fait leurs preuves dans l’études des protocoles de sécurité. Il existe même plusieurs outils qui permettent d’automatiser la vérification de ces protocoles. Toutefois, ceux-ci se montrent encore parfois dans l’incapacité d’analyser certains protocoles, que ce soit à cause de certaines primitives cryptographiques employées ou des propriétés que l’on cherche à démontrer.Dans la première partie de cette thèse, on étudie deux systèmes existants: un protocole de vote par internet Norvégien et un protocole pour les votes en réunion du CNRS. A l’aide du pi-calcul appliqué, nous analysons des garanties de sécurité qu’ils proposent et ce, au travers de différents scénarios de corruption. Mais malgré les résultats réutilisables obtenus, ces preuves démontrent également la difficulté de les effectuer à la main.C’est pourquoi la troisième partie de cette thèse est consacrée à une nouvelle piste dans l’automatisation de telles preuves: les systèmes de types. En effet, inspirés par le développement récent d’un système de types permettant de traiter des propriétés d’équivalence, nous l’avons utilisé afin de démontrer des propriétés comme l’anonymat dans le vote électronique. Nous avons appliqué cette méthode à un exemple: Helios, un système de vote par internet bien connu.Il existe une autre famille de protocoles de sécurité : les APIs. Ces interfaces permettent l’utilisation d’informations stockées dans des dispositifs sécurisés sans qu’il soit normalement possible de les en extraire. Des travaux récents montrent que de telles interfaces sont également vulnérables. La deuxième partie de cette thèse présente un nouveau design d’API, incluant une fonctionnalité de révocation, rarement présente dans les solutions existantes. Nous démontrons, par une analyse entièrement formelle, qu’aucune combinaison de commandes ne permet de faire fuir des clefs sensées rester secrètes, même si l’adversaire parvient à en brute-forcer certaines.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000809 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Checkpoint/biblio.hfd -nk 000809 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Checkpoint
|type= RBID
|clé= Hal:tel-01107718
|texte= Formal Verification of Advanced Families of Security Protocols: E-Voting and APIs
}}
| This area was generated with Dilib version V0.6.33. |  |