Publications

Bruno Blanchet, Charlie Jacomme (2024). Post-quantum sound CryptoVerif and verification of hybrid TLS and SSH key-exchanges. Proceedings of the 37th IEEE Computer Security Foundations Symposium (CSF'24).

Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, Rolfe Schmidt (2024). Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging. USENIX Security Symposium (USENIX Security), 2024.

Cas Cremers, Charlie Jacome, Philip Lukert (2023). Subterm-based proof techniques for improving the automation and scope of security protocol analysis. Proceedings of the 36th IEEE Computer Security Foundations Symposium (CSF'23).

Vincent Cheval, Cas Cremers, Alexander Dax, Lucca Hirschi, Charlie Jacomme, Steve Kremer (2023). Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses. USENIX Security Symposium (USENIX Security), 2023
🏆 Distinguished Paper Award.

Cas Cremers, Charlie Jacomme, Aurora Naska (2023). Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations. USENIX Security Symposium (USENIX Security), 2023.

Cas Cremers, Alexander Dax, Charlie Jacomme, Mang Zhao (2023). Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact Protocol Security. USENIX Security Symposium (USENIX Security), 2023.
🏆 Distinguished Paper Award.

Charlie Jacomme, Elise Klein, Steve Kremer, Maïwenn Racouchot (2023). A comprehensive, formal and automated analysis of the EDHOC protocol. USENIX Security Symposium (USENIX Security), 2023.

Vincent Cheval, Charlie Jacomme, Steve Kremer, Robert Künnemann (2022). SAPIC+: protocol verifiers of the world, unite!. USENIX Security Symposium (USENIX Security), 2022.

Cas Cremers, Caroline Fontaine, Charlie Jacomme (2022). A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols. Proceedings of the 43nd IEEE Symposium on Security and Privacy (S&P'22).

Gilles Barthe, Charlie Jacomme, Steve Kremer (2021). Universal Equivalence and Majority of Probabilistic Programs over Finite Fields. ACM Trans. Comput. Logic.

David Baelde, Stéphanie Delaune, Adrien Koutsos, Charlie Jacomme, Solène Moreau (2021). An interactive prover for protocol verification in the computational model. IEEE Symposium on Security and Privacy (S&P'21).

Charlie Jacomme, Steve Kremer (2021). An extensive formal analysis of multi-factor authentication protocols. ACM Transactions on Privacy and Security (TOPS).

Hubert Comon, Charlie Jacomme, Guillaume Scerri (2020). Oracle simulation: a technique for protocol composition with long term shared secrets. Proceedings of the 27st ACM Conference on Computer and Communications Security (CCS'20).

PDF Long Version

Charlie Jacomme (2020). Proofs of Security Protocols - Symbolic Methods and Powerful Attackers.

Gilles Barthe, Charlie Jacomme, Steve Kremer (2020). Universal equivalence and majority on probabilistic programs over finite fields. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'20).

Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub (2019). Symbolic methods in computational cryptography proofs. Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'19).

Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi (2018). Symbolic Proofs for Lattice-Based Cryptography. Proceedings of the 25th ACM Conference on Computer and Communications Security (CCS'18).

Charlie Jacomme, Steve Kremer (2018). An extensive formal analysis of multi-factor authentication protocols. Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18).

Charlie Jacomme, Steve Kremer, Guillaume Scerri (2018). Symbolic Models for Isolated Execution Environments. Proceedings of the 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17).