Symbolic Models for Isolated Execution Environments. - Charlie Jacomme; Steve Kremer; Guillaume Scerri (IACR Cryptol. ePrint Arch., 2017)

Symbolic Proofs for Lattice-Based Cryptography. - Gilles Barthe; Xiong Fan; Joshua Gancher; Benjamin Grégoire; Charlie Jacomme; Elaine Shi (IACR Cryptol. ePrint Arch., 2018)

Symbolic Methods in Computational Cryptography Proofs. - Gilles Barthe; Benjamin Grégoire; Charlie Jacomme; Steve Kremer; Pierre-Yves Strub (CSF, 2019)

Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets. - Hubert Comon; Charlie Jacomme; Guillaume Scerri (CCS, 2020)

Preuves de protocoles cryptographiques : méthodes symboliques et attaquants puissants. (Proofs of security protocols : symbolic methods and powerful attackers). - Charlie Jacomme (2020)

An Interactive Prover for Protocol Verification in the Computational Model. - David Baelde; Stéphanie Delaune; Charlie Jacomme; Adrien Koutsos; Solène Moreau (SP, 2021)

An Extensive Formal Analysis of Multi-factor Authentication Protocols. - Charlie Jacomme; Steve Kremer (ACM Trans. Priv. Secur., 2021)

Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses. - Vincent Cheval; Cas Cremers; Alexander Dax; Lucca Hirschi; Charlie Jacomme; Steve Kremer (IACR Cryptol. ePrint Arch., 2022)

Sapic+: protocol verifiers of the world, unite! - Vincent Cheval; Charlie Jacomme; Steve Kremer; Robert Künnemann (IACR Cryptol. ePrint Arch., 2022)

A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols. - Cas Cremers; Caroline Fontaine; Charlie Jacomme (IACR Cryptol. ePrint Arch., 2022)

Subterm-based proof techniques for improving the automation and scope of security protocol analysis. - Cas Cremers; Charlie Jacomme; Philip Lukert (IACR Cryptol. ePrint Arch., 2022)

Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations. - Cas Cremers; Charlie Jacomme; Aurora Naska (IACR Cryptol. ePrint Arch., 2022)

TokenWeaver: Privacy Preserving and Post-Compromise Secure Attestation. - Cas Cremers; Charlie Jacomme; Eyal Ronen (IACR Cryptol. ePrint Arch., 2022)

Universal Equivalence and Majority of Probabilistic Programs over Finite Fields. - Gilles Barthe; Charlie Jacomme; Steve Kremer (ACM Trans. Comput. Log., 2022)

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

Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact Protocol Security. - Cas Cremers; Alexander Dax; Charlie Jacomme; Mang Zhao (IACR Cryptol. ePrint Arch., 2023)

Post-Quantum Sound CryptoVerif and Verification of Hybrid TLS and SSH Key-Exchanges. - Bruno Blanchet; Charlie Jacomme (CSF, 2024)

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

The Squirrel Prover and its Logic. - David Baelde; Stéphanie Delaune; Charlie Jacomme; Adrien Koutsos; Joseph Lallemand (ACM SIGLOG News, 2024)

Token Weaver: Privacy Preserving and Post-Compromise Secure Attestation. - Cas Cremers; Gal Horowitz; Charlie Jacomme; Eyal Ronen (SP, 2025)