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. ,
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é ,
A vérifie qu'il n'y a pas d'irrégularités entre les autres entités ,
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 ,
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
Helios: Web-based Open-Audit Voting, 17th USENIX Security Symposium, 2008. ,
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
RFC 6818: Public Key Infrastructure Certificate and Certificate Revocation List (CRL) Profile, 2013. ,
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
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption), First International Conference of Theoretical Computer Science (IFIP), 2000. ,
StatVerif: Verification of Stateful Processes, 24th IEEE Computer Security Foundations Symposium (CSF), 2011. ,
API-level attacks on embedded systems, Computer, vol.34, issue.10, 2001. ,
DOI : 10.1109/2.955101
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
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
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
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
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
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
Simple verifiable elections, USENIX/ACCURATE Electronic Voting Technology Workshop, 2006. ,
Probabilistic Relational Verification for Cryptographic Implementations, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014. ,
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
An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001. ,
DOI : 10.1109/CSFW.2001.930138
An Automatic Security Protocol Verifier based on Resolution Theorem Proving (invited tutorial), 20th International Conference on Automated Deduction (CADE), 2005. ,
Vérification Automatique de Protocoles Cryptographiques: Modèle Formel et Modèle Calculatoire Mémoire d'habilitation à diriger des recherches, 2008. ,
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
A Secure Cryptographic Token Interface, 2009 22nd IEEE Computer Security Foundations Symposium, 2009. ,
DOI : 10.1109/CSF.2009.7
From Security Protocols to Pushdown Automata, 40th International Colloquium on Automata, Languages, and Programming (ICALP), 2013. ,
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
Trace equivalence decision, Proceedings of the 18th ACM conference on Computer and communications security, CCS '11, 2011. ,
DOI : 10.1145/2046707.2046744
Civitas: Toward a Secure Voting System, IEEE Symposium on Security and Privacy (S&P), 2008. ,
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
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
A Secure and Optimally Efficient Multi-Authority Election Scheme, International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt), 1997. ,
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
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
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
Computational soundness of observational equivalence, Proceedings of the 15th ACM conference on Computer and communications security, CCS '08, 2008. ,
DOI : 10.1145/1455770.1455786
Intruder Deductions, Constraint Solving and Insecurity Decisionin Presence of Exclusive Or, 18th IEEE Symposium on Logic in Computer Science (LICS), 2003. ,
On the Security of PKCS #11, Cryptographic Hardware and Embedded Systems (CHES), 2003. ,
DOI : 10.1007/978-3-540-45238-6_32
Defending the Bank with a Proof Assistant, 6th International Workshop on Issues in the Theory of Security (WITS), 2006. ,
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
Unbounded Verification, Falsification, and Characterization of Security Protocols by Pattern Refinement, ACM Conference on Computer and Communications Security, 2008. ,
A Practical Voter-Verifiable Election Scheme, 10th European Symposium on Research in Computer Security (ESORICS), 2005. ,
DOI : 10.1007/11555827_8
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
Attacking and fixing Helios: An analysis of ballot secrecy, Journal of Computer Security, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00732899
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
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
Formal Analysis of PKCS#11, 2008 21st IEEE Computer Security Foundations Symposium, 2008. ,
DOI : 10.1109/CSF.2008.16
Undecidability of Bounded Security Protocols, Proceedings of the Workshop on Formal Methods and Security Protocols, 1999. ,
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
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
Type-Based Verification of Electronic Voting Systems, 2009. ,
Security Analysis of the Diebold AccuVote-TS Voting Machine, USENIX/ACCURATE Electronic Voting Technology Workshop (EVT), 2007. ,
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
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
Analysis of an Internet Voting Protocol, Cryptology ePrint Archive Report, vol.380, 2010. ,
Web Page of the Norwegian Government on the Deployment of E-voting ,
Caveat Coercitor: Coercion-Evidence in Electronic Voting, IEEE Symposium on Security and Privacy (S&P), 2013. ,
Efficient Maximal Privacy in Boardroom Voting and Anonymous Broadcast, In Financial Cryptography, 2004. ,
DOI : 10.1007/978-3-540-27809-2_10
Anonymous voting by two-round public discussion, IET Information Security, vol.4, issue.2, 2010. ,
DOI : 10.1049/iet-ifs.2008.0127
Deciding Framed Bisimilarity, Electr. Notes Theor. Comput. Sci, 2002. ,
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
A Verifiable Multi-Authorities Secret Election Allowing Abstaining from Voting, International Computer Symposium, 1998. ,
Broken Ballots: Will Your Vote Count? Center For The Study Of Language And Information, 2012. ,
The Codebreakers : the Story of Secret Writing, 1996. ,
Sevecom Baseline Architecture. Deliverable D2.1-App.A for EU Project Sevecom, 2009. ,
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
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
ProSwapper: Improved equivalence verifier for ProVerif, 2010. ,
Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach, 2008. ,
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
Accountability: Definition and Relationship to Verifiability, ACM Conference on Computer and Communications Security (CCS), 2010. ,
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
Clash Attacks on the Verifiability of E-Voting Systems, 2012 IEEE Symposium on Security and Privacy, 2012. ,
DOI : 10.1109/SP.2012.32
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. ,
A Proof of Coincidence of Labeled Bisimilarity and Observational Equivalence in Applied Pi Calculus, 2011. ,
Breaking and fixing the Needham-Schroeder public-key protocol using FDR, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1996. ,
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
Verifying SeVeCom using set-based abstraction, 2011 7th International Wireless Communications and Mobile Computing Conference, 2011. ,
DOI : 10.1109/IWCMC.2011.5982705
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
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
The kerberos network authentication service -rfc 4120, 2005. ,
An Improvement on a Practical Secret Voting Scheme, Second International Information Security Workshop (ISW), 1999. ,
DOI : 10.1007/3-540-47790-X_19
The ThreeBallot Voting System. Unpublished draft Available at http://people.csail.mit, 2006. ,
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
Introduction to the TPM 1.2, 2009. ,
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
Applied Cryptography Protocols, Algorithms, and Source Code in C, 1995. ,
Scantegrity III: Automatic Trustworthy Receipts, Highlighting Over/Under Votes, and Full Voter Verifiability, Electronic Voting Technology Workshop / Workshop on Trustworthy Elections, EVT/WOTE, 2011. ,
Automating Open Bisimulation Checking for the Spi Calculus, 2010 23rd IEEE Computer Security Foundations Symposium, 2010. ,
DOI : 10.1109/CSF.2010.28
Strand Spaces: Proving Security Protocols Correct, Journal of Computer Security, 1999. ,
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
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
Secure On-board Architecture Specification, 2011. ,
Source Files for ProVerif, JavaCard and rF * Code (Under Construction ) ,
Security Analysis of India's Electronic Voting Machines, 17th ACM Conference on Computer and Communications Security (CCS), 2010. ,
KeyRev: An Effifcient Key Revocation Scheme for Wireless Sensor Networks, IEEE International Conference on Communications (ICC), 2007. ,