. Testé-en-septembre, pour des élections municipales en Norvège [Gov], ce protocole a été mis en place dans dix municipalités et a été utilisé par environ 28 000 votants en, 2011.

. 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é

R. Durant-la-phase-de-décompteb, A vérifie qu'il n'y a pas d'irrégularités entre les autres entités

. 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

M. Arnaud, V. Cortier, and C. Wiedling, Analysis of an Electronic Boardroom Voting System, 4th International Conference on E-Voting and Identify, p.2013
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, 2008.

M. Abadi and C. Fournet, Mobile Values, New names, and Secure Communication, 28th ACM Symposium on Principles of Programming Languages (POPL), 2001.
DOI : 10.1145/373243.360213

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, 2004.
DOI : 10.1007/978-3-540-30079-3_16

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.80.9042

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

[. 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, 2001.
DOI : 10.1109/2.955101

[. Blanchet, M. Abadi, and C. Fournet, Automated Verification of Selected Equivalences for Security Protocols, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), 2008.
DOI : 10.1109/LICS.2005.8

M. Baudet, Deciding security of protocols against off-line guessing attacks, Proceedings of the 12th ACM conference on Computer and communications security , CCS '05, 2005.
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), 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, 2010.
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), 2011.
DOI : 10.1007/978-3-642-23822-2_19

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

[. 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), 2007.
DOI : 10.1007/978-3-540-77050-3_9

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

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), 2014.

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), 2011.
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., 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), 2005.

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), 2012.
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, 2009.
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), 2013.

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), 2014.
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, 2011.
DOI : 10.1145/2046707.2046744

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

[. Cortier and S. Delaune, A Method for Proving Observational Equivalence, 2009 22nd IEEE Computer Security Foundations Symposium, 2009.
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, 2013.
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), 1997.

V. Cheval, APTE: An Algorithm for Proving Trace Equivalence, 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2014.
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), 2007.
DOI : 10.1007/978-3-540-71209-1_42

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

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

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

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

J. Clulow, On the Security of PKCS #11, Cryptographic Hardware and Embedded Systems (CHES), 2003.
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), 2006.

[. 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, 2008.

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

[. Cortier and G. Steel, A Generic Security API for Symmetric Key Management on Cryptographic Devices, 14th European Symposium on Research in Computer Security (ESORICS), 2009.
DOI : 10.1109/CSFW.2001.930145

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

[. Cortier and B. Smyth, Attacking and fixing Helios: An analysis of ballot secrecy, Journal of Computer Security, 2013.
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, 2012.
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. [DKR09] Stéphanie Delaune, Steve Kremer, and Mark Ryan. Verifying Privacy-type Properties of Electronic Voting Protocols, 2009.
DOI : 10.3233/JCS-15777

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

[. 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

N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov, Undecidability of Bounded Security Protocols, Proceedings of the Workshop on Formal Methods and Security Protocols, 1999.

[. Daubignard, D. Lubicz, and G. Steel, A Secure Key Management Interface with Asymmetric Cryptography, Third International Conference on Principles of Security and Trust (POST), 2014.
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, 2002.
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), 2007.

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, 1992.
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, 2009.
DOI : 10.1007/978-3-642-03459-6_7

[. 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), 2013.

J. Groth, Efficient Maximal Privacy in Boardroom Voting and Anonymous Broadcast, In Financial Cryptography, 2004.
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, 2010.
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, Proceedings of the 2005 ACM workshop on Privacy in the electronic society , WPES '05, 2005.
DOI : 10.1145/1102199.1102213

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.8779

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

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), 2005.
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), 2010.
DOI : 10.1007/978-3-642-15497-3_24

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

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

T. [. Küsters and . Truderung, An Epistemic Approach to Coercion-Resistance for Electronic Voting Protocols, 2009 30th IEEE Symposium on Security and Privacy, 2009.
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), 2010.

[. 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, 2011.
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, 2012.
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)Lev10] Frederic Levy. SAM and Key Management Functional Presentation. Available from http, 2004.

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

]. 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), 1996.

D. Longley and S. Rigby, An automatic search for security flaws in key management schemes, Computers & Security, vol.11, issue.1, 1992.
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, 2011.
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, 2001.
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), 2013.
DOI : 10.1007/978-3-642-39799-8_48

C. Neuman, T. Yu, S. Hartman, and K. 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), 1999.
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., 2001.
DOI : 10.1109/CSFW.2001.930145

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

[. 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, 2006.
DOI : 10.1007/s10817-005-9016-8

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, 2011.

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, 1999.

[. Viganò, Automated Security Protocol Analysis With the AVISPA Tool, Electronic Notes in Theoretical Computer Science, vol.155, 2006.
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, CADE, 1999.
DOI : 10.1007/3-540-48660-7_29

]. B. Wey11 and . Weyl, Secure On-board Architecture Specification, 2011.

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), 2010.

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