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é ,
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 ,
é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 ,
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 ,
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 ,
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 ,
Just Fast Keying in the Pi Calculus, ACM Transactions on Information and System Security, 2007. ,
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
Helios: Web-based Open-Audit Voting, 17th USENIX Security Symposium ,
Mobile Values, New names, and Secure Communication, 28th ACM Symposium on Principles of Programming Languages (POPL) ,
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 ,
DOI : 10.1007/978-3-540-30079-3_16
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption), First International Conference of Theoretical Computer Science (IFIP) ,
StatVerif: Verification of Stateful Processes, 24th IEEE Computer Security Foundations Symposium (CSF), 2011. ,
API-level attacks on embedded systems, Computer, vol.34, issue.10 ,
DOI : 10.1109/2.955101
Automated Verification of Selected Equivalences for Security Protocols, J. Log. Algebr. Program ,
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
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
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
Adapting Helios for Provable Ballot Secrecy, 16th European Symposium on Research in Computer Security (ESORICS) ,
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) ,
DOI : 10.1007/978-3-540-77050-3_9
Simple verifiable elections, USENIX/ACCURATE Electronic Voting Technology Workshop ,
Probabilistic Relational Verification for Cryptographic Implementations, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) ,
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
An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 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) ,
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) ,
DOI : 10.1007/978-3-642-34961-4_38
A Secure Cryptographic Token Interface, 2009 22nd IEEE Computer Security Foundations Symposium ,
DOI : 10.1109/CSF.2009.7
From Security Protocols to Pushdown Automata, 40th International Colloquium on Automata, Languages, and Programming (ICALP) ,
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
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
Civitas: Toward a Secure Voting System, IEEE Symposium on Security and Privacy (S&P) ,
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
A Generic Construction for Voting Correctness at Minimum Cost -Application to Helios, IACR Cryptology ePrint Archive ,
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), pp.9-9 ,
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
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
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
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
Intruder Deductions, Constraint Solving and Insecurity Decisionin Presence of Exclusive Or, 18th IEEE Symposium on Logic in Computer Science (LICS) ,
On the Security of PKCS #11, Cryptographic Hardware and Embedded Systems (CHES) ,
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) ,
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 ,
A Practical Voter-Verifiable Election Scheme, 10th European Symposium on Research in Computer Security (ESORICS) ,
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) ,
URL : https://hal.archives-ouvertes.fr/inria-00426621
Attacking and fixing Helios: An analysis of ballot secrecy, Journal of Computer Security ,
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 ,
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. ,
URL : https://hal.archives-ouvertes.fr/hal-00732907
Verifying privacy-type properties of electronic voting protocols, Journal of Computer Security, vol.17, issue.4 ,
DOI : 10.3233/JCS-2009-0340
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, pp.9-9 ,
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
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
Type-Based Verification of Electronic Voting Systems, 2009. ,
Security Analysis of the Diebold AccuVote-TS Voting Machine, USENIX/ACCURATE Electronic Voting Technology Workshop (EVT) ,
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
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
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) ,
Efficient Maximal Privacy in Boardroom Voting and Anonymous Broadcast, Financial Cryptography ,
DOI : 10.1007/978-3-540-27809-2_10
Anonymous voting by two-round public discussion, IET Information Security, vol.4, issue.2 ,
DOI : 10.1049/iet-ifs.2008.0127
Deciding Framed Bisimilarity, Electr. Notes Theor. Comput. Sci, 2002. ,
Coercion-Resistant Electronic Elections, ACM Workshop on Privacy in the Electronic Society ,
A Verifiable Multi-Authorities Secret Election Allowing Abstaining from Voting, International Computer Symposium, vol.1, pp.9-9 ,
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) ,
DOI : 10.1007/978-3-540-31987-0_14
Election Verifiability in Electronic Voting Protocols, 15th European Symposium on Research in Computer Security (ESORICS) ,
DOI : 10.1007/978-3-642-15497-3_24
ProSwapper: Improved equivalence verifier for ProVerif ,
Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach ,
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
Accountability: Definition and Relationship to Verifiability, ACM Conference on Computer and Communications Security (CCS) ,
Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study, 2011 IEEE Symposium on Security and Privacy ,
DOI : 10.1109/SP.2011.21
Clash Attacks on the Verifiability of E-Voting Systems, 2012 IEEE Symposium on Security and Privacy ,
DOI : 10.1109/SP.2012.32
Providing Receipt-Freeness in Mixnet-Based Voting Protocols, 6th International Conference on Information Security and Cryptology (ICISC), 2004. ,
SAM and Key Management Functional Presentation Available from http, 2010. ,
A Proof of Coincidence of Labeled Bisimilarity and Observational Equivalence in Applied Pi Calculus, LiuJia0608. pdf ,
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 ,
An automatic search for security flaws in key management schemes, Computers & Security, vol.11, issue.1 ,
DOI : 10.1016/0167-4048(92)90222-D
Verifying SeVeCom using set-based abstraction, 2011 7th International Wireless Communications and Mobile Computing Conference ,
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 ,
DOI : 10.1145/501983.502007
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
The kerberos network authentication service -rfc 4120, 2005. ,
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
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. ,
DOI : 10.1109/CSFW.2001.930145
URL : https://hal.archives-ouvertes.fr/inria-00072492
Introduction to the TPM 1.2, 2009. ,
Attacking Group Protocols by Refuting Incorrect Inductive Conjectures, Journal of Automated Reasoning, vol.4, issue.1/2 ,
DOI : 10.3233/JCS-2001-91-203
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 ,
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, vol.1, pp.9-9 ,
Automated Security Protocol Analysis With the AVISPA Tool, Electronic Notes in Theoretical Computer Science, vol.155 ,
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, pp.1-9 ,
DOI : 10.1007/3-540-48660-7_29
Secure On-board Architecture Specification. Deliverable D3.2 for EU Project EVITA ,
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) ,
KeyRev: An Effifcient Key Revocation Scheme for Wireless Sensor Networks, IEEE International Conference on Communications (ICC) ,