. De-cette-thèse-pour-voir-le-fonctionnement-du-protocole-en-détail, D'un point de vue informel, B va recueillir le vote du votant et R va fournir une preuve au votant que son vote a bel et bien été pris en compte. La spécificité de ce protocole est qu'il fournit deux confirmations au votant permettant de s'assurer qu'il n'y a pas de problème. La première, que son vote a été pris en compte, via un retour sur son ordinateur. La seconde, que c'est le bon vote qui a été enregistré

. Durant-la-phase-de-décompte, ou non) le déchiffrement et la publication des résultats par D. Afin d'étudier ce protocole, ce dernier est modélisé à l'aide du pi-calcul appliqué. Les différentes modélisations peuvent être trouvées dans la section 2.2. On y trouvera l'ensemble des primitives cryptographiques et leurs propriétés

. Cette-partie-est-dédiée, étude d'une API de sécurité pour la gestion de clefs symétriques stockées sur des composants sécurisés. L'intérêt de cette interface est qu'elle propose une fonction de révocation, une fonctionnalité souvent difficile à mettre en place tout en garantissant un niveau de sécurité optimal [EG02, Kar09, MM11]. Le design de l'API se base sur une hiérarchie de niveaux entre les différentes clefs qui forme un ordre partiel

B. Théorème, Si une clef est valide (c.-à-d. sa date de validité n'a pas expiré) et telle que son niveau n'est pas inférieur au niveau d'une clef perdue (connue de l'attaquant) alors cette clef est non déductible par l'attaquant

B. Théorème, Si le système est compromis à un niveau l et que l'intrus ne parvient pas à corrompre de clefs d'un niveau strictement supérieur à l,a l o r s ,a ub o u td ' u nc e r t a i nt e m p s ,l e système ne sera plus compromis que jusqu

L. Enfin and . Dernier-résultat-concerne-la-révocation, En effet, plutôt que d'attendre que le système se répare de lui-même, on peut procéder à une révocation et ainsi sécuriser immédiatement le système en

[. Bibliography, B. Abadi, C. Blanchet, and . Fournet, Just Fast Keying in the Pi Calculus, ACM Transactions on Information and System Security, 2007.

M. Arnaud, V. Cortier, and C. Wiedling, Analysis of an Electronic Boardroom Voting System, 4th International Conference on E-Voting and Identify
DOI : 10.1007/978-3-642-39185-9_7

URL : https://hal.archives-ouvertes.fr/hal-00881011

B. Adida, Helios: Web-based Open-Audit Voting, 17th USENIX Security Symposium

M. Abadi and C. Fournet, Mobile Values, New names, and Secure Communication, 28th ACM Symposium on Principles of Programming Languages (POPL)
URL : https://hal.archives-ouvertes.fr/hal-01423924

E. Y. Peter and . Akayla, RFC 6818: Public Key Infrastructure Certificate and Certificate Revocation List (CRL) Profile, 2013.

R. Aditya, B. Lee, C. Boyd, and E. Dawson, An Efficient Mixnet-Based Voting Scheme Providing Receipt-Freeness, First International Conference of Trust and Privacy in Digital Busines
DOI : 10.1007/978-3-540-30079-3_16

M. Abadi and P. Rogaway, Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption), First International Conference of Theoretical Computer Science (IFIP)

[. Arapinis, E. Ritter, and M. Ryan, StatVerif: Verification of Stateful Processes, 24th IEEE Computer Security Foundations Symposium (CSF), 2011.

M. Bond and R. Anderson, API-level attacks on embedded systems, Computer, vol.34, issue.10
DOI : 10.1109/2.955101

[. Blanchet, M. Abadi, and C. Fournet, Automated Verification of Selected Equivalences for Security Protocols, J. Log. Algebr. Program

M. Baudet, Deciding security of protocols against off-line guessing attacks, Proceedings of the 12th ACM conference on Computer and communications security , CCS '05
DOI : 10.1145/1102120.1102125

B. Blanchet and A. Chaudhuri, Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage, 2008 IEEE Symposium on Security and Privacy (sp 2008)
DOI : 10.1109/SP.2008.12

M. Bortolozzo, M. Centenaro, R. Focardi, and G. Steel, Attacking and fixing PKCS#11 security tokens, Proceedings of the 17th ACM conference on Computer and communications security, CCS '10
DOI : 10.1145/1866307.1866337

D. Bernhard, V. Cortier, O. Pereira, B. Smyth, and B. Warinschi, Adapting Helios for Provable Ballot Secrecy, 16th European Symposium on Research in Computer Security (ESORICS)
URL : https://hal.archives-ouvertes.fr/inria-00638554

M. Backes, M. Dürmuth, and R. Küsters, On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography, 27th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
DOI : 10.1007/978-3-540-77050-3_9

J. Benaloh, Simple verifiable elections, USENIX/ACCURATE Electronic Voting Technology Workshop

C. Gilles-barthe, B. Fournet, P. Grégoire, N. Strub, S. Z. Swamy et al., Probabilistic Relational Verification for Cryptographic Implementations, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, 31st Annual Cryptology Conference on Advances in Cryptology (CRYPTO)
DOI : 10.1007/978-3-642-22792-9_5

URL : https://hal.archives-ouvertes.fr/hal-01112075

B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001.
DOI : 10.1109/CSFW.2001.930138

B. Blanchet, An Automatic Security Protocol Verifier based on Resolution Theorem Proving (invited tutorial), 20th International Conference on Automated Deduction (CADE)

B. Blanchet, Vérification Automatique de Protocoles Cryptographiques: Modèle Formel et Modèle Calculatoire Mémoire d'habilitation à diriger des recherches, 2008.

[. Bernhard, O. Pereira, and B. Warinschi, How Not to Prove Yourself: Pitfalls of the Fiat-Shamir Heuristic and Applications to Helios, International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT)
DOI : 10.1007/978-3-642-34961-4_38

N. [. Cachin and . Chandran, A Secure Cryptographic Token Interface, 2009 22nd IEEE Computer Security Foundations Symposium
DOI : 10.1109/CSF.2009.7

[. Chrétien, V. Cortier, and S. Delaune, From Security Protocols to Pushdown Automata, 40th International Colloquium on Automata, Languages, and Programming (ICALP)

R. Chrétien, V. Cortier, and S. Delaune, Typing Messages for Free in Security Protocols: The Case of Equivalence Properties, 25th International Conference on Concurrency Theory (CONCUR)
DOI : 10.1007/978-3-662-44584-6_26

V. Cheval, H. Comon-lundh, and S. Delaune, Trace equivalence decision, Proceedings of the 18th ACM conference on Computer and communications security, CCS '11
DOI : 10.1145/2046707.2046744

URL : http://kar.kent.ac.uk/46878/1/CCD-ccs11.pdf

R. Michael, S. Clarkson, A. C. Chong, and . Myers, Civitas: Toward a Secure Voting System, IEEE Symposium on Security and Privacy (S&P)

V. Cortier and S. Delaune, A Method for Proving Observational Equivalence, 2009 22nd IEEE Computer Security Foundations Symposium
DOI : 10.1109/CSF.2009.9

URL : https://hal.archives-ouvertes.fr/inria-00426622

V. Cortier, D. Galindo, S. Glondu, and M. Izabachène, A Generic Construction for Voting Correctness at Minimum Cost -Application to Helios, IACR Cryptology ePrint Archive
URL : https://hal.archives-ouvertes.fr/hal-00881079

[. Cramer, R. Gennaro, and B. Schoenmakers, A Secure and Optimally Efficient Multi-Authority Election Scheme, International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt), pp.9-9

V. Cheval, APTE: An Algorithm for Proving Trace Equivalence, 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
DOI : 10.1007/978-3-642-54862-8_50

[. Cortier, G. Keighren, and G. Steel, Automatic Analysis of the Security of XOR-Based Key Management Schemes, Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
DOI : 10.1007/978-3-540-71209-1_42

URL : https://hal.archives-ouvertes.fr/inria-00181616

H. Comon-lundh and V. Cortier, New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols, 14th International Conference on Rewriting Techniques and Applications (RTA)
DOI : 10.1007/3-540-44881-0_12

H. Comon-lundh and V. Cortier, Computational soundness of observational equivalence, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08
DOI : 10.1145/1455770.1455786

URL : https://hal.archives-ouvertes.fr/inria-00323195

H. Comon-lundh and V. Shmatikov, Intruder Deductions, Constraint Solving and Insecurity Decisionin Presence of Exclusive Or, 18th IEEE Symposium on Logic in Computer Science (LICS)

J. Clulow, On the Security of PKCS #11, Cryptographic Hardware and Embedded Systems (CHES)
DOI : 10.1007/978-3-540-45238-6_32

J. [. Courant and . Monin, Defending the Bank with a Proof Assistant, 6th International Workshop on Issues in the Theory of Security (WITS)

[. Chevalier and M. Rusinowitch, Combining Intruder Theories, 32nd International Colloquium on Automata, Languages and Programming (ICALP), 2005.
DOI : 10.1007/11523468_52

URL : https://hal.archives-ouvertes.fr/inria-00070512

J. F. Cas and . Cremers, Unbounded Verification, Falsification, and Characterization of Security Protocols by Pattern Refinement, ACM Conference on Computer and Communications Security

[. Chaum, Y. A. Peter, S. A. Ryan, and . Schneider, A Practical Voter-Verifiable Election Scheme, 10th European Symposium on Research in Computer Security (ESORICS)
DOI : 10.1007/11555827_8

V. Cortier and G. Steel, A Generic Security API for Symmetric Key Management on Cryptographic Devices, 14th European Symposium on Research in Computer Security (ESORICS)
URL : https://hal.archives-ouvertes.fr/inria-00426621

V. Cortier and B. Smyth, Attacking and fixing Helios: An analysis of ballot secrecy, Journal of Computer Security
URL : https://hal.archives-ouvertes.fr/hal-00732899

[. Cortier, G. Steel, and C. Wiedling, Revoke and let live, Proceedings of the 2012 ACM conference on Computer and communications security, CCS '12
DOI : 10.1145/2382196.2382293

URL : https://hal.archives-ouvertes.fr/hal-00732902

C. [. Cortier and . Wiedling, A formal analysis of the Norwegian E-voting protocol, First International Conference on Principles of Security and Trust (POST), 2012.
URL : https://hal.archives-ouvertes.fr/hal-00732907

[. Delaune, S. Kremer, and M. Ryan, Verifying privacy-type properties of electronic voting protocols, Journal of Computer Security, vol.17, issue.4
DOI : 10.3233/JCS-2009-0340

[. Delaune, S. Kremer, and G. Steel, Formal Analysis of PKCS#11, 2008 21st IEEE Computer Security Foundations Symposium, 2008.
DOI : 10.1109/CSF.2008.16

P. [. Durgin, J. Lincoln, A. Mitchell, and . Scedrov, Undecidability of Bounded Security Protocols, Proceedings of the Workshop on Formal Methods and Security Protocols, pp.9-9

[. Daubignard, D. Lubicz, and G. Steel, A Secure Key Management Interface with Asymmetric Cryptography, Third International Conference on Principles of Security and Trust (POST)
DOI : 10.1007/978-3-642-54792-8_4

URL : https://hal.archives-ouvertes.fr/hal-00805987

L. Eschenauer and V. D. Gligor, A key-management scheme for distributed sensor networks, Proceedings of the 9th ACM conference on Computer and communications security , CCS '02
DOI : 10.1145/586110.586117

F. Eigner, Type-Based Verification of Electronic Voting Systems, 2009.

A. [. Feldman, E. Halderman, and . Felten, Security Analysis of the Diebold AccuVote-TS Voting Machine, USENIX/ACCURATE Electronic Voting Technology Workshop (EVT)

A. Fujioka, T. Okamoto, and K. Ohta, A practical secret voting scheme for large scale elections, Workshop on the Theory and Application of Cryptographic Techniques: Advances in Cryptology, pp.9-9
DOI : 10.1007/3-540-57220-1_66

S. Fröschle and G. Steel, Analysing PKCS#11 Key Management APIs with Unbounded Fresh Data, Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS)
DOI : 10.1109/CSF.2007.32

[. Gjøsteen, Analysis of an Internet Voting Protocol, Cryptology ePrint Archive Report, vol.380, 2010.

. Gov-]-norwegian and . Government, Web Page of the Norwegian Government on the Deployment of E-voting

S. Gurchetan, M. Grewal, S. Dermot-ryan, P. Y. Bursuc, and . Ryan, Caveat Coercitor: Coercion-Evidence in Electronic Voting, IEEE Symposium on Security and Privacy (S&P)

J. Groth, Efficient Maximal Privacy in Boardroom Voting and Anonymous Broadcast, Financial Cryptography
DOI : 10.1007/978-3-540-27809-2_10

[. Hao, Y. A. Peter, P. Ryan, and . Zielinski, Anonymous voting by two-round public discussion, IET Information Security, vol.4, issue.2
DOI : 10.1049/iet-ifs.2008.0127

H. Hüttel, Deciding Framed Bisimilarity, Electr. Notes Theor. Comput. Sci, 2002.

A. Juels, D. Catalano, and M. Jakobsson, Coercion-Resistant Electronic Elections, ACM Workshop on Privacy in the Electronic Society

[. Juang, C. Lei, and P. Yu, A Verifiable Multi-Authorities Secret Election Allowing Abstaining from Voting, International Computer Symposium, vol.1, pp.9-9

W. Douglas, B. Jones, and . Simons, Broken Ballots: Will Your Vote Count? Center For The Study Of Language And Information, 2012.

D. Kahn, The Codebreakers : the Story of Secret Writing, 1996.

]. F. Kar09 and . Kargl, Sevecom Baseline Architecture. Deliverable D2.1-App.A for EU Project Sevecom, 2009.

S. Kremer and M. Ryan, Analysis of an Electronic Voting Protocol in the Applied Pi Calculus, 14th European Symposium on Programming (ESOP)
DOI : 10.1007/978-3-540-31987-0_14

S. Kremer, M. Ryan, and B. Smyth, Election Verifiability in Electronic Voting Protocols, 15th European Symposium on Research in Computer Security (ESORICS)
DOI : 10.1007/978-3-642-15497-3_24

[. Klus, B. Smyth, and M. D. Ryan, ProSwapper: Improved equivalence verifier for ProVerif

R. Küsters and T. Truderung, Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach

T. [. Küsters and . Truderung, An Epistemic Approach to Coercion-Resistance for Electronic Voting Protocols, 2009 30th IEEE Symposium on Security and Privacy, 2012.
DOI : 10.1109/SP.2009.13

[. Küsters, T. Truderung, and A. Vogt, Accountability: Definition and Relationship to Verifiability, ACM Conference on Computer and Communications Security (CCS)

[. Küsters, T. Truderung, and A. Vogt, Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study, 2011 IEEE Symposium on Security and Privacy
DOI : 10.1109/SP.2011.21

T. [. Küsters, A. Truderung, and . Vogt, Clash Attacks on the Verifiability of E-Voting Systems, 2012 IEEE Symposium on Security and Privacy
DOI : 10.1109/SP.2012.32

C. Byoungcheon-lee, E. Boyd, K. Dawson, J. Kim, S. Yang et al., Providing Receipt-Freeness in Mixnet-Based Voting Protocols, 6th International Conference on Information Security and Cryptology (ICISC), 2004.

[. Levy, SAM and Key Management Functional Presentation Available from http, 2010.

J. Liu, A Proof of Coincidence of Labeled Bisimilarity and Observational Equivalence in Applied Pi Calculus, LiuJia0608. pdf

]. G. Low96 and . Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.9-9

D. Longley and S. Rigby, An automatic search for security flaws in key management schemes, Computers & Security, vol.11, issue.1
DOI : 10.1016/0167-4048(92)90222-D

S. Mödersheim and P. Modesti, Verifying SeVeCom using set-based abstraction, 2011 7th International Wireless Communications and Mobile Computing Conference
DOI : 10.1109/IWCMC.2011.5982705

J. K. Millen and V. Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, Proceedings of the 8th ACM conference on Computer and Communications Security , CCS '01
DOI : 10.1145/501983.502007

S. Meier, B. Schmidt, C. Cremers, and D. A. Basin, The TAMARIN Prover for the Symbolic Analysis of Security Protocols, 25th International Conference on Computer Aided Verification (CAV)
DOI : 10.1007/978-3-642-39799-8_48

T. [. Neuman, S. Yu, K. Hartman, and . Raeburn, The kerberos network authentication service -rfc 4120, 2005.

F. Ohkubo, M. Miura, A. Abe, T. Fujioka, and . Okamoto, An Improvement on a Practical Secret Voting Scheme, Second International Information Security Workshop (ISW), pp.9-9
DOI : 10.1007/3-540-47790-X_19

R. L. Rivest, The ThreeBallot Voting System. Unpublished draft Available at http://people.csail.mit, 2006.

M. Rusinowitch and . Turuani, Protocol insecurity with finite number of sessions is NP-complete, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001.
DOI : 10.1109/CSFW.2001.930145

URL : https://hal.archives-ouvertes.fr/inria-00072492

[. Ryan, Introduction to the TPM 1.2, 2009.

A. [. Steel and . Bundy, Attacking Group Protocols by Refuting Incorrect Inductive Conjectures, Journal of Automated Reasoning, vol.4, issue.1/2
DOI : 10.3233/JCS-2001-91-203

B. Schneier, Applied Cryptography Protocols, Algorithms, and Source Code in C, 1995.

A. T. Sherman, R. A. Fink, R. Carback, and D. Chaum, Scantegrity III: Automatic Trustworthy Receipts, Highlighting Over/Under Votes, and Full Voter Verifiability, Electronic Voting Technology Workshop / Workshop on Trustworthy Elections, EVT/WOTE

A. Tiu and J. E. Dawson, Automating Open Bisimulation Checking for the Spi Calculus, 2010 23rd IEEE Computer Security Foundations Symposium, 2010.
DOI : 10.1109/CSF.2010.28

[. Thayer, J. C. Herzog, and J. D. Guttman, Strand Spaces: Proving Security Protocols Correct, Journal of Computer Security, vol.1, pp.9-9

[. Viganò, Automated Security Protocol Analysis With the AVISPA Tool, Electronic Notes in Theoretical Computer Science, vol.155
DOI : 10.1016/j.entcs.2005.11.052

[. Weidenbach, Towards an Automatic Analysis of Security Protocols in First-Order Logic, 16th International Conference on Automated Deduction, pp.1-9
DOI : 10.1007/3-540-48660-7_29

]. B. Wey11 and . Weyl, Secure On-board Architecture Specification. Deliverable D3.2 for EU Project EVITA

C. Wiedling, Source Files for ProVerif, JavaCard and rF ? Code (Under Construction )

]. S. Wwh-+-10, E. Wolchok, J. A. Wustrow, H. K. Halderman, A. Prasad et al., Security Analysis of India's Electronic Voting Machines, 17th ACM Conference on Computer and Communications Security (CCS)

X. Zouz, Y. Wan, and B. Ramamurthy, KeyRev: An Effifcient Key Revocation Scheme for Wireless Sensor Networks, IEEE International Conference on Communications (ICC)