Charlie Jacomme

Latest

• Are ideal functionalities really ideal?
• Subversion-resilient Key-exchange in the Post-quantum World
• Token Weaver: Privacy Preserving and Post-Compromise Secure Attestation
• Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging
• Post-quantum sound CryptoVerif and verification of hybrid TLS and SSH key-exchanges
• A comprehensive, formal and automated analysis of the EDHOC protocol
• Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact Protocol Security
• Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations
• Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses
• A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols
• SAPIC+: protocol verifiers of the world, unite!
• Universal Equivalence and Majority of Probabilistic Programs over Finite Fields
• An extensive formal analysis of multi-factor authentication protocols
• An interactive prover for protocol verification in the computational model
• Oracle simulation: a technique for protocol composition with long term shared secrets
• Proofs of Security Protocols - Symbolic Methods and Powerful Attackers
• Universal equivalence and majority on probabilistic programs over finite fields
• Symbolic methods in computational cryptography proofs
• Symbolic Proofs for Lattice-Based Cryptography
• An extensive formal analysis of multi-factor authentication protocols
• Symbolic Models for Isolated Execution Environments