Publications HAL de la collection SVP

2025

Journal articles

titre
Preservation of Speculative Constant-time by Compilation
auteur
Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
article
Proceedings of the ACM on Programming Languages, 2025, 9 (POPL), pp.1293 - 1325. ⟨10.1145/3704880⟩
Accès au texte intégral et bibtex
https://hal.univ-lorraine.fr/hal-04663857/file/3704880.pdf BibTex
titre
Vote&Check: Secure Postal Voting with Reduced Trust Assumptions
auteur
Véronique Cortier, Alexandre Debant, Pierrick Gaudry, Léo Louistisserand
article
Proceedings on Privacy Enhancing Technologies, 2025, 2025 (3), pp.333-348. ⟨10.56553/popets-2025-0101⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04813613/file/main2.pdf BibTex

Conference papers

titre
Narrowbeer: A Practical Replay Attack Against the Widevine DRM
auteur
Florian Roudot, Mohamed Sabt
article
34th USENIX Security Symposium (USENIX Security '25), Aug 2025, Seattle, United States
Accès au texte intégral et bibtex
https://hal.science/hal-05111498/file/paper.pdf BibTex
titre
Automatic verification of Finite Variant Property beyond convergent equational theories
auteur
Vincent Cheval, Caroline Fontaine
article
2025 IEEE 38th Computer Security Foundations Symposium (CSF 2025), IEEE, Jul 2025, Santa Cruz, United States
Accès au texte intégral et bibtex
https://hal.science/hal-04748770/file/main.pdf BibTex
titre
GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses
auteur
Pierrick Philippe, Mohamed Sabt, Pierre-Alain Fouque
article
Dependable Systems and Networks 2025, IEEE/IFIP, Jun 2025, Naples, Italy
Accès au texte intégral et bibtex
https://inria.hal.science/hal-05065294/file/GnuZero_final.pdf BibTex
titre
SMT-based Automation for Overwhelming Truth
auteur
David Baelde, Stéphanie Delaune, Stanislas Riou
article
38th IEEE Computer Security Foundations Symposium, Owen Arden and Mohsen Lesani, Jun 2025, Santa Cruz, United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04884758/file/main.pdf BibTex
titre
Zero-Knowledge Proofs from Learning Parity with Noise: Optimization, Verification, and Application
auteur
Thomas Haines, Rafieh Mosaheb, Johannes Müller, Reetika Reetika
article
IEEE Computer Security Foundations (CSF) Symposium 2025, Jun 2025, Santa Cruz, United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04856221/file/Zero_Knowledge_Proofs_from_Learning_Parity_with_Noise__Optimization__Verification__and_Application.pdf BibTex
titre
Formal Analysis of Random Nonce Misuses in Cryptographic Protocols
auteur
Gildas Avoine, Tristan Claverie, Stéphanie Delaune
article
38th IEEE Computer Security Foundations Symposium (CFS 2025), Jun 2025, Santa Cruz, CA, United States
Accès au texte intégral et bibtex
https://hal.science/hal-05066621/file/master.pdf BibTex
titre
Secrecy by typing in the computational model
auteur
Stéphanie Delaune, Clément Herouard, Joseph Lallemand
article
38th IEEE Computer Security Foundations Symposium (CSF 2025), Owen Arden, Jun 2025, Santa Cruz, CA, United States
Accès au texte intégral et bibtex
https://cnrs.hal.science/hal-04666965/file/main-long.pdf BibTex
titre
A Quantitative Probabilistic Relational Hoare Logic
auteur
Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire
article
POPL 2025 - 52nd ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2025, Denver (Colorado), United States. ⟨10.1145/3704876⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04834149/file/paper.pdf BibTex
titre
A Comprehensive Formal Security Analysis of OPC UA
auteur
Vincent Diemunsch, Lucca Hirschi, Steve Kremer
article
Usenix Security 2025, 2025, Seattle (USA), Washington, United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04989554/file/main.pdf BibTex
titre
Breaking verifiability and vote privacy in CHVote
auteur
Véronique Cortier, Alexandre Debant, Pierrick Gaudry
article
30th European Symposium on Research in Computer Security - ESORICS 2025, 2025, Toulouse, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04895582/file/paper.pdf BibTex

Preprints, Working Papers, ...

titre
Attacking and Fixing the Android Protected Confirmation Protocol
auteur
Myrto Arapinis, Vincent Danos, Maïwenn Racouchot, David Robin, Thomas Zacharias
article
2025
Accès au texte intégral et bibtex
https://hal.science/hal-05038009/file/main.pdf BibTex
titre
Verifying Protocols with Squirrel: Making Strides Without Compromise
auteur
David Baelde, Stéphanie Delaune, Julia Gabet, Clément Hérouard
article
2025
Accès au texte intégral et bibtex
https://hal.science/hal-05013723/file/main.pdf BibTex
titre
Proving e-voting mixnets in the CCSA model: zero-knowledge proofs and rewinding
auteur
Margot Catinaud, Caroline Fontaine, Guillaume Scerri
article
2025
Accès au texte intégral et bibtex
https://hal.science/hal-04937921/file/main.pdf BibTex

2024

Journal articles

titre
Post-quantum XML and SAML Single Sign-On
auteur
Johannes Müller, Jan Oupický
article
Proceedings on Privacy Enhancing Technologies, 2024, 2024 (4), pp.525-543. ⟨10.56553/popets-2024-0128⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04845637/file/Post_quantum_SAML.pdf BibTex
titre
A Comprehensive Survey on Post-Quantum TLS
auteur
Nouri Alnahawi, Johannes Müller, Jan Oupický, Alexander Wiesmaier
article
IACR Communications in Cryptology, 2024, ⟨10.62056/ahee0iuc⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04845617/file/1-2-6.pdf BibTex
titre
The Squirrel Prover and its Logic
auteur
David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, Joseph Lallemand
article
ACM SIGLOG News, 2024, 11 (2), ⟨10.1145/3665453.3665461⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04579038/file/main.pdf BibTex
titre
DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice
auteur
Vincent Cheval, Steve Kremer, Itsaka Rakotonirina
article
TheoretiCS, 2024, Volume3, ⟨10.46298/theoretics.24.4⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04875934/file/2211.03225-4.pdf BibTex
titre
High-assurance zeroization
auteur
Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
article
IACR Transactions on Cryptographic Hardware and Embedded Systems, 2024, 2024 (1), pp.375-397. ⟨10.46586/tches.v2024.i1.375-397⟩
Accès au texte intégral et bibtex
https://hal.univ-lorraine.fr/hal-04691165/file/TCHES2024_1_13.pdf%22%3Bfilename%2A%3DUTF-8%27%27TCHES2024_1_13.pdf BibTex

Conference papers

titre
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs
auteur
Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni
article
OOPSLA 2024 -ACM Conference on Object Oriented Programming Systems Languages and Applications, Oct 2024, Pasadena (CA), United States. pp.784-809, ⟨10.1145/3649839⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04834120/file/paper.pdf BibTex
titre
Foundations for Cryptographic Reductions in CCSA Logics
auteur
David Baelde, Adrien Koutsos, Justine Sauvage
article
CCS '24: ACM SIGSAC Conference on Computer and Communications Security, Oct 2024, Salt Lake City UT, United States. pp.2814-2828, ⟨10.1145/3658644.3690193⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04511718/file/hal-v2.pdf BibTex
titre
SoK: Mechanisms Used in Practice for Verifiable Internet Voting
auteur
Florian Moser, Michael Kirsten, Felix Dörre
article
E-Vote-ID 2024 - 9th International Joint Conference on Electronic Voting, Oct 2024, Tarragona, Spain. pp.141-162, ⟨10.18420/e-vote-id2024_10⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04686386/file/main.pdf BibTex
titre
Belenios with cast-as-intended: towards a usable interface
auteur
Véronique Cortier, Pierrick Gaudry, Anselme Goetschmann, Sophie Lemonnier
article
EVote-ID 2024 - 9th International Joint Conference on Electronic Voting, Oct 2024, Terragona, Spain
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04646244/file/main.pdf BibTex
titre
Code voting: when simplicity meets security
auteur
Véronique Cortier, Alexandre Debant, Florian Moser
article
ESORICS 2024 29th European Symposium on Research in Computer Security, Sep 2024, Bydgoszcz, Poland
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04627733/file/main.pdf BibTex
titre
Formally verifying Kyber: Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt
auteur
José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
article
Crypto 2024, International Association for Cryptologic Research, Aug 2024, Santa Barbara (CA), United States. ⟨10.1007/978-3-031-68379-4_12⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04595591/file/2024-843.pdf BibTex
titre
Formal Security Analysis of Widevine through the W3C EME Standard
auteur
Stéphanie Delaune, Joseph Lallemand, Gwendal Patat, Florian Roudot, Mohamed Sabt
article
USENIX Security Symposium, Aug 2024, PHILADELPHIA, United States
Accès au texte intégral et bibtex
https://hal.science/hal-04631369/file/main.pdf BibTex
titre
Shaken, not Stirred -Automated Discovery of Subtle Attacks on Protocols using Mix-Nets
auteur
Jannik Dreier, Pascal Lafourcade, Dhekra Mahmoud
article
Usenix Security Symposium, Aug 2024, Philadelphia, United States
Accès au texte intégral et bibtex
https://uca.hal.science/hal-04615474/file/main.pdf BibTex
titre
Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging
auteur
Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, Rolfe Schmidt
article
33rd USENIX Security Symposium, Aug 2024, Philadelphia (PA), United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04604518/file/main.pdf BibTex
titre
Election Eligibility with OpenID: Turning Authentication into Transferable Proof of Eligibility
auteur
Véronique Cortier, Alexandre Debant, Anselme Goetschmann, Lucca Hirschi
article
USENIX Security Symposium, Aug 2024, Philadelphie (USA), United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04764478/file/usenixsecurity24-cortier.pdf BibTex
titre
Dealing with Dynamic Key Compromise in CryptoVerif
auteur
Bruno Blanchet
article
37th IEEE Computer Security Foundations Symposium, IEEE, Jul 2024, Enschede, Netherlands. pp.495-510, ⟨10.1109/CSF61375.2024.00015⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04271666/file/main.pdf BibTex
titre
A Probabilistic Logic for Concrete Security
auteur
David Baelde, Caroline Fontaine, Adrien Koutsos, Guillaume Scerri, Théo Vignon
article
CSF 2024 - 37th IEEE Computer Security Foundations Symposium, Jul 2024, Enschede, Netherlands. pp.324-339
Accès au texte intégral et bibtex
https://hal.science/hal-04577828/file/main.pdf BibTex
titre
CV2EC: Getting the Best of Both Worlds
auteur
Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub
article
CSF 2024 - 37th IEEE Computer Security Foundations Symposium, IEEE, Jul 2024, Enschede, Netherlands. pp.283-298, ⟨10.1109/CSF61375.2024.00019⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04321656/file/main.pdf BibTex
titre
Nothing is Out-of-Band: Formal Modeling of Ceremonies
auteur
Barbara Fila, Saša Radomirović
article
2024 IEEE 37th Computer Security Foundations Symposium (CSF), Jul 2024, Enschede, Netherlands. pp.464-478, ⟨10.1109/CSF61375.2024.00049⟩
Accès au bibtex
BibTex
titre
Post-quantum sound CryptoVerif and verification of hybrid TLS and SSH key-exchanges
auteur
Bruno Blanchet, Charlie Jacomme
article
CSF'24 - 37th IEEE Computer Security Foundations Symposium, IEEE, Jul 2024, Enschede, Netherlands. pp.543-556, ⟨10.1109/CSF61375.2024.00032⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04577912/file/main.pdf BibTex
titre
Belenios: the Certification Campaign
auteur
Angèle Bossuat, Eloïse Brocas, Véronique Cortier, Pierrick Gaudry, Stéphane Glondu, Nicolas Kovacs
article
SSTIC 2024 - Symposium sur la sécurité des technologies de l'information et des communications, Jun 2024, Rennes, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04578848/file/Belenios.pdf BibTex
titre
Is the JCJ voting system really coercion-resistant?
auteur
Véronique Cortier, Pierrick Gaudry, Quentin Yang
article
37th IEEE Computer Security Foundations Symposium (CSF), 2024, Enschede, Netherlands
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03629587/file/main-full.pdf BibTex

Software

titre
Artifact for "Foundations for Cryptographic Reductions in CCSA Logics
auteur
David Baelde, Adrien Koutsos, Justine Sauvage
article
2024
Accès au texte intégral et bibtex
https://hal.science/hal-04650670/file/squirrel-artifact-ccs24%20%281%29.zip BibTex

Theses

titre
Formal analysis of security protocols:real-world case-studies and automated proof strategies
auteur
Maïwenn Racouchot
article
Computer Science [cs]. Université de Lorraine, 2024. English. ⟨NNT : 2024LORR0186⟩
Accès au texte intégral et bibtex
https://hal.science/tel-04965599/file/DDOC_T_2024_0186_RACOUCHOT.pdf BibTex

2023

Journal articles

titre
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
auteur
Son Ho, Aymeric Fromherz, Jonathan Protzenko
article
Proceedings of the ACM on Programming Languages, 2023, 7 (ICFP), pp.385-416. ⟨10.1145/3607844⟩
Accès au bibtex
BibTex
titre
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability
auteur
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
article
ACM Transactions on Privacy and Security, 2023, 26 (3), pp.1-34. ⟨10.1145/3589962⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04048217/file/hal-preprint.pdf BibTex
titre
Symbolic protocol verification with dice
auteur
Vincent Cheval, Raphaëlle Crubillé, Steve Kremer
article
Journal of Computer Security, 2023, pp.1-38. ⟨10.3233/JCS-230037⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04179875/file/main.pdf BibTex

Conference papers

titre
Comparse: Provably Secure Formats for Cryptographic Protocols
auteur
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
article
CCS '23: ACM SIGSAC Conference on Computer and Communications Security, Nov 2023, Copenhagen, Denmark. pp.564-578, ⟨10.1145/3576915.3623201⟩
Accès au bibtex
BibTex
titre
French 2022 legislatives elections: a verifiability experiment
auteur
Véronique Cortier, Pierrick Gaudry, Stéphane Glondu, Sylvain Ruhault
article
The E-Vote-ID Conference 2023, Oct 2023, Luxembourg City, Luxembourg
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04205615/file/main.pdf BibTex
titre
Machine-Checked Proofs of Accountability: How to sElect who is to Blame
auteur
Constantin Catalin Dragan, François Dupressoir, Kristian Gjøsteen, Thomas Haines, Peter Rønne, Morten Rotvold Solberg
article
ESORICS 2023, Sep 2023, The Hague, The Netherlands, Netherlands. ⟨10.1007/978-3-031-51479-1_24⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04216243/file/main-lncs.pdf BibTex
titre
Extended version: Tamarin-based Analysis of Bluetooth Uncovers Two Practical Pairing Confusion Attacks
auteur
Tristan Claverie, Gildas Avoine, Stéphanie Delaune, José Lopes Esteves
article
28th European Symposium on Research in Computer Security on Computer Security, Gene Tsudik, Mauro Conti, Kaitai Liang, Georgios Smaragdakis, Sep 2023, The Hague, Netherlands
Accès au texte intégral et bibtex
https://hal.science/hal-04079883/file/master.pdf BibTex
titre
Formally verifying Kyber: Episode IV: Implementation correctness
auteur
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
article
CHES 2023 - Conference on Cryptographic Hardware and Embedded Systems, IACR, Sep 2023, Praha, Czech Republic. pp.164-193, ⟨10.46586/tches.v2023.i3.164-193⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04218417/file/a.pdf BibTex
titre
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium
auteur
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
article
CRYPTO 2023 - 43rd International Cryptology Conference, Aug 2023, Santa Barbara, United States. pp.358-389, ⟨10.1007/978-3-031-38554-4_12⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04315311/file/dilithium.pdf BibTex
titre
TreeSync: Authenticated Group Management for Messaging Layer Security
auteur
Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan
article
USENIX Security '23, Aug 2023, Anaheim, United States
Accès au bibtex
BibTex
titre
Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations
auteur
Cas Cremers, Charlie Jacomme, Aurora Naska
article
USENIX Security 2023 - 32nd USENIX Security Symposium, Aug 2023, Anaheim, United States
Accès au bibtex
BibTex
titre
Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact Protocol Security
auteur
Cas Cremers, Alexander Dax, Charlie Jacomme, Mang Zhao
article
32nd USENIX Security Symposium 2023, USENIX, Aug 2023, Anaheim, United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04126116/file/AEAD-eprint.pdf BibTex
titre
A comprehensive, formal and automated analysis of the EDHOC protocol
auteur
Charlie Jacomme, Elise Klein, Steve Kremer, Maïwenn Racouchot
article
USENIX Security '23 - 32nd USENIX Security Symposium, Aug 2023, Anaheim, CA, United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03810102/file/paper.pdf BibTex
titre
Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses
auteur
Vincent Cheval, Cas Cremers, Alexander Dax, Lucca Hirschi, Charlie Jacomme, Steve Kremer
article
32nd USENIX Security Symposium, Aug 2023, Anaheim, United States
Accès au texte intégral et bibtex
https://hal.science/hal-03795715/file/eprint.pdf BibTex
titre
Indistinguishability Beyond Diff-Equivalence in ProVerif
auteur
Vincent Cheval, Itsaka Rakotonirina
article
2023 IEEE 36th Computer Security Foundations Symposium (CSF), Jul 2023, Dubrovnik, Croatia. pp.184-199, ⟨10.1109/CSF57540.2023.00036⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04219230/file/CR-csf23.pdf BibTex
titre
Proving Unlinkability using ProVerif through Desynchronized Bi-Processes
auteur
David Baelde, Alexandre Debant, Stéphanie Delaune
article
IEEE Computer Security Foundations Symposium, Jul 2023, Dubrovnik, Croatia
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03674979/file/main-csf.pdf BibTex
titre
Election Verifiability with ProVerif
auteur
Vincent Cheval, Véronique Cortier, Alexandre Debant
article
CSF 2023 - 36th IEEE Computer Security Foundations Symposium, Jul 2023, Dubrovnik, Croatia. ⟨10.1109/CSF57540.2023.00032⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04177268/file/CSF23%20%281%29.pdf BibTex
titre
From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake
auteur
Daniel de Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, Karthikeyan Bhargavan
article
EuroS&P 2023 - IEEE 8th European Symposium on Security and Privacy, Jul 2023, Delft, Netherlands. pp.707-723, ⟨10.1109/EuroSP57164.2023.00048⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04175322/file/2023-eurosp-dragondoom.pdf BibTex
titre
Automatic verification of transparency protocols
auteur
Vincent Cheval, José Moreira, Mark Ryan
article
2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P), Jul 2023, Delft, Netherlands. ⟨10.1109/EuroSP57164.2023.00016⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04219234/file/CMR-EuroSnP23.pdf BibTex
titre
A Higher-Order Indistinguishability Logic for Cryptographic Reasoning
auteur
David Baelde, Adrien Koutsos, Joseph Lallemand
article
LICS, Jun 2023, Boston, United States. pp.1-13, ⟨10.1109/LICS56636.2023.10175781⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03981949/file/hal.pdf BibTex
titre
Typing High-Speed Cryptography against Spectre v1
auteur
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
article
SP 2023- IEEE Symposium on Security and Privacy, IEEE, May 2023, San Francisco, United States. pp.1592-1609, ⟨10.1109/SP46215.2023.10179418⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04106448/file/camera_ready.pdf BibTex
titre
Sound Verification of Security Protocols: From Design to Interoperable Implementations
auteur
Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David Basin, Peter Müller
article
2023 IEEE Symposium on Security and Privacy (SP), May 2023, San Francisco, United States
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04210887/file/main.pdf BibTex
titre
On the Auditability of the Estonian IVXV System and an Attack on Individual Verifiability
auteur
Anggrio Sutopo, Thomas Haines, Peter Rønne
article
Workshop on Advances in Secure Electronic Voting, May 2023, Bol, brac, Croatia. ⟨10.1007/978-3-031-48806-1_2⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04216242/file/Estonia_VOTING_23.pdf BibTex
titre
Belenios with cast as intended
auteur
Véronique Cortier, Alexandre Debant, Pierrick Gaudry, Stéphane Glondu
article
Voting 2023 - 8th Workshop on Advances in Secure Electronic Voting, May 2023, Bol, Brač, Croatia
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04020110/file/main.pdf BibTex

Reports

titre
One Vote is Enough for Analysing Privacy
auteur
Stéphanie Delaune, Joseph Lallemand, Arthur Outrey
article
CNRS. 2023
Accès au texte intégral et bibtex
https://hal.science/hal-04262499/file/version-hal-31-10-2023.pdf BibTex
titre
CryptoVerif: a Computationally-Sound Security Protocol Verifier
auteur
Bruno Blanchet, Charlie Jacomme
article
RR-9526, Inria. 2023, pp.194
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04253820/file/RR-9526.pdf BibTex
titre
CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels)
auteur
Bruno Blanchet
article
RR-9525, Inria Paris. 2023, pp.166
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04246199/file/RR-9525.pdf BibTex
titre
Aeneas: Rust Verification by Functional Translation
auteur
Son Ho, Jonathan Protzenko, Aymeric Fromherz
article
Inria Paris. 2023
Accès au texte intégral et bibtex
https://hal.science/hal-04136056/file/main.pdf BibTex

Preprints, Working Papers, ...

titre
Reversing, Breaking, and Fixing the French Legislative Election E-Voting Protocol
auteur
Alexandre Debant, Lucca Hirschi
article
2023
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03875463/file/1653%20%281%29.pdf BibTex
titre
Symbolic protocol verification with dice: process equivalences in the presence of probabilities (extended version)
auteur
Vincent Cheval, Raphaëlle Crubillé, Steve Kremer
article
2023
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03683907/file/main.pdf BibTex

2022

Conference papers

titre
Verifiable Decryption in the Head
auteur
Kristian Gjøsteen, Thomas Haines, Johannes Müller, Peter Rønne, Tjerand Silde
article
Australasian Conference on Information Security and Privacy, Nov 2022, Wollongong, Australia. pp.355-374, ⟨10.1007/978-3-031-22301-3_18⟩
Accès au texte intégral et bibtex
https://cnrs.hal.science/hal-03913553/file/main.pdf BibTex
titre
Themis: an On-Site Voting System with Systematic Cast-as-intended Verification and Partial Accountability
auteur
Mikaël Bougon, Hervé Chabanne, Véronique Cortier, Alexandre Debant, Emmanuelle Dottax, Jannik Dreier, Pierrick Gaudry, Mathieu Turuani
article
CCS 2022 - The ACM Conference on Computer and Communications Security, Nov 2022, Los Angeles, United States. ⟨10.1145/3548606.3560563⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03763294/file/main%20%282%29.pdf BibTex
titre
Time, Privacy, Robustness, Accuracy: Trade-Offs for the Open Vote Network Protocol
auteur
Fatima-Ezzahra El Orche, Rémi Géraud-Stewart, Peter Rønne, Gergei Bana, David Naccache, Peter Y. A. Ryan, Marco Biroli, Megi Dervishi, Hugo Waltsburger
article
International Joint Conference on Electronic Voting 2022, Oct 2022, Bregenz, Austria. pp.19-35, ⟨10.1007/978-3-031-15911-4_2⟩
Accès au texte intégral et bibtex
https://cnrs.hal.science/hal-03913581/file/Robust.pdf BibTex
titre
One vote is enough for analysing privacy
auteur
Stéphanie Delaune, Joseph Lallemand
article
ESORICS 2022 - 27th European Symposium on Research in Computer Security, Sep 2022, Copenhague, Denmark
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03669664/file/main-long.pdf BibTex
titre
Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
auteur
Constantin Catalin Dragan, Francois Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y.A. Ryan, Peter Rønne, Morten Rotvold Solberg
article
2022 IEEE 35th Computer Security Foundations Symposium (CSF), Aug 2022, Haifa, Israel. ⟨10.1109/CSF54842.2022.9919663⟩
Accès au texte intégral et bibtex
https://cnrs.hal.science/hal-03913573/file/main.pdf BibTex