Publications

Filter by type:

. Fixing the Achilles Heel of E-Voting: The Bulletin Board. CSF, 2021.

Preprint PDF Models and proofs

. A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols. Usenix Security, 2020.

PDF DOI Tool Models and proofs

. Verification of Stateful Cryptographic Protocols with Exclusive OR. JCS (journal), 2020.

Preprint PDF DOI Code

. Symbolic Abstractions for Quantum Protocol Verification. Submitted, 2019.

Preprint PDF Extended Abstract

. Symbolic Analysis of Identity-Based Protocols. Festschrift Symposium in Honor of Catherine Meadows, LNCS 11565, 2019.

PDF DOI Models

. A method for unbounded verification of privacy-type properties. JCS (journal), 2019.

Preprint PDF DOI Tool

. Improving Automated Symbolic Analysis for E-voting Protocols: A Method Based on Sufficient Conditions for Ballot Secrecy. Euro S&P, 2019.

PDF Slides DOI Extended version Models

. New Privacy Threat on 3G, 4G, and Upcoming 5G AKA Protocols. PETS, 2019.

Preprint PDF DOI Black-Hat USA'17 talk Media coverage Video of PoC Models

. A Formal Analysis of 5G Authentication. CCS, 2018.

PDF Slides Extended version DOI Media coverage Models

. POR for Security Protocol Equivalences : Beyond Action-Determinism. ESORICS, 2018.

PDF Extended version DOI Slides Tool

. Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR. CSF, 2018.

Preprint PDF DOI Code

. Automated Verification of Privacy in Security Protocols: Back and Forth Between Theory & Practice. PhD thesis, 2017.

PDF Slides 1-Page Summary DOI

. A Reduced Semantics for Deciding Trace Equivalence. LMCS (journal), 2017.

PDF DOI Code

. Mobile subscriber WiFi privacy. Security & Privacy Workshops (MoST), 2017.

PDF DOI Best paper award Models

. A method for verifying privacy-type properties: the unbounded case. Security & Privacy (Oakland), 2016.

PDF Slides DOI Tool Models

. Towards Completeness via Proof Search in the Linear Time μ-calculus. LICS, 2016.

PDF DOI

. A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. JLAMP (journal), 2016.

PDF DOI

. Partial Order Reduction for Security Protocols. CONCUR, 2015.

PDF Slides DOI Code

. A reduced semantics for deciding trace equivalence using constraint systems. POST, 2014.

PDF Slides DOI Code