49 documents
Articles dans une revue
- David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, Joseph Lallemand. The Squirrel Prover and its Logic. ACM SIGLOG News, 2024, 11 (2), ⟨10.1145/3665453.3665461⟩. ⟨hal-04579038⟩
- Son Ho, Aymeric Fromherz, Jonathan Protzenko. Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification. Proceedings of the ACM on Programming Languages, 2023, 7 (ICFP), pp.385-416. ⟨10.1145/3607844⟩. ⟨hal-04301439⟩
- Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability: Journal pre-print: full version. ACM Transactions on Privacy and Security, 2023, 26 (3), pp.1-34. ⟨10.1145/3589962⟩. ⟨hal-04048217⟩
- Vincent Cheval, Raphaëlle Crubillé, Steve Kremer. Symbolic protocol verification with dice: Process equivalences in the presence of probabilities. Journal of Computer Security, 2023, pp.1-38. ⟨10.3233/JCS-230037⟩. ⟨hal-04179875⟩
Communications dans un congrès
- Véronique Cortier, Pierrick Gaudry, Anselme Goetschmann, Sophie Lemonnier. Belenios with cast-as-intended: towards a usable interface. EVote-ID 2024 - 9th International Joint Conference on Electronic Voting, Oct 2024, Terragona, Spain. ⟨hal-04646244⟩
- Véronique Cortier, Alexandre Debant, Florian Moser. Code voting: when simplicity meets security. ESORICS 2024, Sep 2024, Bydgoszcz, Poland. ⟨hal-04627733⟩
- Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, Rolfe Schmidt. Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging. 33rd USENIX Security Symposium, Aug 2024, Philadelphia (PA), United States. ⟨hal-04604518v2⟩
- Stéphanie Delaune, Joseph Lallemand, Gwendal Patat, Florian Roudot, Mohamed Sabt. Formal Security Analysis of Widevine through the W3C EME Standard. USENIX Security Symposium, Aug 2024, PHILADELPHIA, United States. ⟨hal-04631369⟩
- Jannik Dreier, Pascal Lafourcade, Dhekra Mahmoud. Shaken, not Stirred -Automated Discovery of Subtle Attacks on Protocols using Mix-Nets. Usenix Security Symposium, Aug 2024, Philadelphia, United States. ⟨hal-04615474⟩
- Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub. CV2EC: Getting the Best of Both Worlds. CSF 2024 - 37th IEEE Computer Security Foundations Symposium, IEEE, Jul 2024, Enschede, Netherlands. pp.283-298, ⟨10.1109/CSF61375.2024.00019⟩. ⟨hal-04321656v2⟩
- Bruno Blanchet, Charlie Jacomme. Post-quantum sound CryptoVerif and verification of hybrid TLS and SSH key-exchanges. CSF'24 - 37th IEEE Computer Security Foundations Symposium, IEEE, Jul 2024, Enschede, Netherlands. pp.543-556, ⟨10.1109/CSF61375.2024.00032⟩. ⟨hal-04577912⟩
- David Baelde, Caroline Fontaine, Adrien Koutsos, Guillaume Scerri, Théo Vignon. A Probabilistic Logic for Concrete Security. CSF 2024 - 37th IEEE Computer Security Foundations Symposium, Jul 2024, Enschede, Netherlands. ⟨hal-04577828⟩
- Bruno Blanchet. Dealing with Dynamic Key Compromise in CryptoVerif. 37th IEEE Computer Security Foundations Symposium, IEEE, Jul 2024, Enschede (Pays Bas), Netherlands. pp.495-510, ⟨10.1109/CSF61375.2024.00015⟩. ⟨hal-04271666v2⟩
- Angèle Bossuat, Eloïse Brocas, Véronique Cortier, Pierrick Gaudry, Stéphane Glondu, et al.. Belenios: the Certification Campaign. SSTIC 2024 - Symposium sur la sécurité des technologies de l'information et des communications, Jun 2024, Rennes, France. ⟨hal-04578848⟩
- Véronique Cortier, Pierrick Gaudry, Quentin Yang. Is the JCJ voting system really coercion-resistant?. 37th IEEE Computer Security Foundations Symposium (CSF), 2024, Enschede, Netherlands. ⟨hal-03629587v3⟩
- Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan. Comparse: Provably Secure Formats for Cryptographic Protocols. CCS '23: ACM SIGSAC Conference on Computer and Communications Security, Nov 2023, Copenhagen, Denmark. pp.564-578, ⟨10.1145/3576915.3623201⟩. ⟨hal-04310972⟩
- Véronique Cortier, Pierrick Gaudry, Stéphane Glondu, Sylvain Ruhault. French 2022 legislatives elections: a verifiability experiment. The E-Vote-ID Conference 2023, Oct 2023, Luxembourg City, Luxembourg. ⟨hal-04205615⟩
- Constantin Catalin Dragan, François Dupressoir, Kristian Gjøsteen, Thomas Haines, Peter Rønne, et al.. Machine-Checked Proofs of Accountability: How to sElect who is to Blame. ESORICS 2023, Sep 2023, The Hague, The Netherlands, Netherlands. ⟨10.1007/978-3-031-51479-1_24⟩. ⟨hal-04216243⟩
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, et al.. Formally verifying Kyber: Episode IV: Implementation correctness. 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⟩. ⟨hal-04218417⟩
- Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, et al.. Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. CRYPTO 2023 - 43rd International Cryptology Conference, Aug 2023, Santa Barbara, United States. pp.358-389, ⟨10.1007/978-3-031-38554-4_12⟩. ⟨hal-04315311⟩
- Cas Cremers, Alexander Dax, Charlie Jacomme, Mang Zhao. Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact Protocol Security. 32nd USENIX Security Symposium 2023, USENIX, Aug 2023, Anaheim, United States. ⟨hal-04126116v3⟩
- Vincent Cheval, Cas Cremers, Alexander Dax, Lucca Hirschi, Charlie Jacomme, et al.. Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses. 32nd USENIX Security Symposium, Aug 2023, Anaheim, United States. ⟨hal-03795715⟩
- Cas Cremers, Charlie Jacomme, Aurora Naska. Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations. USENIX Security 2023 - 32nd USENIX Security Symposium, Aug 2023, Anaheim, United States. ⟨hal-03996689⟩
- Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan. TreeSync: Authenticated Group Management for Messaging Layer Security. USENIX Security '23, Aug 2023, Anaheim, United States. ⟨hal-04255953⟩
- Charlie Jacomme, Elise Klein, Steve Kremer, Maïwenn Racouchot. A comprehensive, formal and automated analysis of the EDHOC protocol. USENIX Security '23 - 32nd USENIX Security Symposium, Aug 2023, Anaheim, CA, United States. ⟨hal-03810102⟩
- Vincent Cheval, Itsaka Rakotonirina. Indistinguishability Beyond Diff-Equivalence in ProVerif. 2023 IEEE 36th Computer Security Foundations Symposium (CSF), Jul 2023, Dubrovnik, Croatia. pp.184-199, ⟨10.1109/CSF57540.2023.00036⟩. ⟨hal-04219230⟩
- David Baelde, Alexandre Debant, Stéphanie Delaune. Proving Unlinkability using ProVerif through Desynchronized Bi-Processes. IEEE Computer Security Foundations Symposium, Jul 2023, Dubrovnik, Croatia. ⟨hal-03674979v2⟩
- Vincent Cheval, Véronique Cortier, Alexandre Debant. Election Verifiability with ProVerif. CSF 2023 - 36th IEEE Computer Security Foundations Symposium, Jul 2023, Dubrovnik, Croatia. ⟨10.1109/CSF57540.2023.00032⟩. ⟨hal-04177268v2⟩
- Vincent Cheval, José Moreira, Mark Ryan. Automatic verification of transparency protocols. 2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P), Jul 2023, Delft, Netherlands. ⟨10.1109/EuroSP57164.2023.00016⟩. ⟨hal-04219234⟩
- Daniel de Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, Karthikeyan Bhargavan. From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake. EuroS&P 2023 - IEEE 8th European Symposium on Security and Privacy, Jul 2023, Delft, Netherlands. pp.707-723, ⟨10.1109/EuroSP57164.2023.00048⟩. ⟨hal-04175322⟩
- David Baelde, Adrien Koutsos, Joseph Lallemand. A Higher-Order Indistinguishability Logic for Cryptographic Reasoning. LICS, Jun 2023, Boston, United States. pp.1-13, ⟨10.1109/LICS56636.2023.10175781⟩. ⟨hal-03981949v2⟩
- Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, et al.. Typing High-Speed Cryptography against Spectre v1. SP 2023- IEEE Symposium on Security and Privacy, IEEE, May 2023, San Francisco, United States. pp.1592-1609, ⟨10.1109/SP46215.2023.10179418⟩. ⟨hal-04106448⟩
- Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, et al.. Sound Verification of Security Protocols: From Design to Interoperable Implementations. 2023 IEEE Symposium on Security and Privacy (SP), May 2023, San Francisco, United States. ⟨hal-04210887⟩
- Anggrio Sutopo, Thomas Haines, Peter Rønne. On the Auditability of the Estonian IVXV System and an Attack on Individual Verifiability. Workshop on Advances in Secure Electronic Voting, May 2023, Bol, brac, Croatia. ⟨10.1007/978-3-031-48806-1_2⟩. ⟨hal-04216242⟩
- Véronique Cortier, Alexandre Debant, Pierrick Gaudry, Stéphane Glondu. Belenios with cast as intended. Voting 2023 - 8th Workshop on Advances in Secure Electronic Voting, May 2023, Bol, Brač, Croatia. ⟨hal-04020110⟩
- Kristian Gjøsteen, Thomas Haines, Johannes Müller, Peter Rønne, Tjerand Silde. Verifiable Decryption in the Head. Australasian Conference on Information Security and Privacy, Nov 2022, Wollongong, Australia. pp.355-374, ⟨10.1007/978-3-031-22301-3_18⟩. ⟨hal-03913553v2⟩
- Mikaël Bougon, Hervé Chabanne, Véronique Cortier, Alexandre Debant, Emmanuelle Dottax, et al.. Themis: an On-Site Voting System with Systematic Cast-as-intended Verification and Partial Accountability. CCS 2022 - The ACM Conference on Computer and Communications Security, Nov 2022, Los Angeles, United States. ⟨10.1145/3548606.3560563⟩. ⟨hal-03763294v2⟩
- Fatima-Ezzahra El Orche, Rémi Géraud-Stewart, Peter Rønne, Gergei Bana, David Naccache, et al.. Time, Privacy, Robustness, Accuracy: Trade-Offs for the Open Vote Network Protocol. International Joint Conference on Electronic Voting 2022, Oct 2022, Bregenz, Austria. pp.19-35, ⟨10.1007/978-3-031-15911-4_2⟩. ⟨hal-03913581v2⟩
- Stéphanie Delaune, Joseph Lallemand. One vote is enough for analysing privacy. ESORICS 2022 - 27th European Symposium on Research in Computer Security, Sep 2022, Copenhague, Denmark. ⟨hal-03669664⟩
- Constantin Catalin Dragan, Francois Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, et al.. Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co. 2022 IEEE 35th Computer Security Foundations Symposium (CSF), Aug 2022, Haifa, Israel. ⟨10.1109/CSF54842.2022.9919663⟩. ⟨hal-03913573v2⟩
Pré-publications, Documents de travail
- David Baelde, Adrien Koutsos, Justine Sauvage. Cryptographic Reductions By Bi-Deduction. 2024. ⟨hal-04511718v2⟩
- José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, et al.. Formally verifying Kyber: Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. 2024. ⟨hal-04595591⟩
- Alexandre Debant, Lucca Hirschi. Reversing, Breaking, and Fixing the French Legislative Election E-Voting Protocol. 2023. ⟨hal-03875463v3⟩
- Vincent Cheval, Raphaëlle Crubillé, Steve Kremer. Symbolic protocol verification with dice: process equivalences in the presence of probabilities (extended version). 2023. ⟨hal-03683907v2⟩
- Tristan Claverie, Gildas Avoine, Stéphanie Delaune, José Lopes Esteves. Extended version: Tamarin-based Analysis of Bluetooth Uncovers Two Practical Pairing Confusion Attacks. 2023. ⟨hal-04079883⟩
Rapports
- Stéphanie Delaune, Joseph Lallemand, Arthur Outrey. One Vote is Enough for Analysing Privacy. CNRS. 2023. ⟨hal-04262499⟩
- Bruno Blanchet, Charlie Jacomme. CryptoVerif: a Computationally-Sound Security Protocol Verifier. RR-9526, Inria. 2023, pp.194. ⟨hal-04253820⟩
- Bruno Blanchet. CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels). RR-9525, Inria Paris. 2023, pp.166. ⟨hal-04246199⟩
- Son Ho, Jonathan Protzenko, Aymeric Fromherz. Aeneas: Rust Verification by Functional Translation. Inria Paris. 2023. ⟨hal-04136056⟩
Documents récupérés de l'archive ouverte HAL 
