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

Subterm-based proof techniques for improving the automation and scope of security protocol analysis

A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols

SAPIC+: protocol verifiers of the world, unite!

An interactive prover for protocol verification in the computational model

Oracle simulation: a technique for protocol composition with long term shared secrets

Universal equivalence and majority on probabilistic programs over finite fields

We study equivalence checking of probabilistic programs, a fundamental problem which arises in many application areas including cryptography, privacy, algorithmic fairness and machine learning. The programming language we consider manipulates …