Publications

Mechanized Proofs of Adversarial Complexity and Application to Universal Composability
A Higher-Order Indistinguishability Logic for Cryptographic Reasoning
Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability
An Interactive Prover for Protocol Verification in the Computational Model
High-Assurance Cryptography in the Spectre Era
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations