Writing

Campaigns

Trending

  • ProVerif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial
  • Ballot secrecy: Security definition, sufficient conditions, and analysis of Helios
  • TLS 1.3 for engineers: An exploration of the TLS 1.3 specification and OpenJDK's Java implementation
  • A foundation for secret, verifiable elections
  • Automated reasoning for equivalences in the applied pi calculus with barriers
  • Secret, verifiable auctions from elections
  • Formal analysis of privacy in Direct Anonymous Attestation schemes
  • Truncating TLS Connections to Violate Beliefs in Web Applications
  • Attacking and fixing Helios: An analysis of ballot secrecy
  • Election verifiability in electronic voting protocols

Drafts5

  • Annotated biography: Free & fair elections
  • Hooking up with Fiat-Shamir
  • Score-based decisions: Influence, freedom, legitimacy
  • Overcoming Arrow's impossibility: Honeybee sidestep
  • TLS 1.3 for engineers: An exploration of the TLS 1.3 specification and OpenJDK's Java implementation

Communication13

Web, mobile, and hardware standards fail catastrophically; I break them and prove the fixes, hardening the protocols billions trust. Read the essay ›

Web5Truncation, TLS 1.3, encrypted caching

  • The Transport Layer Security (TLS) Protocol Version 1.3
  • TLS 1.3 for engineers: An exploration of the TLS 1.3 specification and OpenJDK's Java implementation
  • CryptoCache: Network Caching with Confidentiality
  • Truncating TLS Connections to Violate Beliefs in Web Applications
  • Secure Authenticated Key Exchange with Revocation for Smart Grid

Hardware4DAA, eUICC, distance bounding

  • An Overview of GSMA's M2M Remote Provisioning Specification
  • Attacks against GSMA's M2M Remote Provisioning
  • Modelling and Analysis of a Hierarchy of Distance Bounding Attacks
  • Formal analysis of privacy in Direct Anonymous Attestation schemes

Cryptography4Non-malleable encryption, Fiat-Shamir

  • Hooking up with Fiat-Shamir
  • Non-malleable encryption with proofs of plaintext knowledge and applications to voting
  • Authentication with weaker trust assumptions for voting systems
  • Adapting Helios for provable ballot privacy

Governance24

Nations are adopting election systems unfit for purpose; I pondered the meaning of free and fair governance for twenty-one years, I have my answer, and a voting system that delivers. Read the essay ›

6Tutorials, the annotated biography, auctions, social choice

  • Annotated biography: Free & fair elections
  • Overcoming Arrow's impossibility: Honeybee sidestep
  • First-past-the-post suffices for ranked voting
  • A short introduction to secrecy and verifiability for elections
  • Secret, verifiable auctions from elections
  • A foundation for secret, verifiable elections

Privacy4Ballot secrecy, receipt-freeness, coercion resistance

  • Championing tally-then-decrypt secrecy
  • Ballot secrecy: Security definition, sufficient conditions, and analysis of Helios
  • Surveying definitions of coercion resistance
  • A critique of game-based definitions of receipt-freeness for voting

6Verifiability for legitimacy

  • Surveying definitions of election verifiability
  • Election Verifiability: Cryptographic Definitions and an Analysis of Helios, Helios-C, and JCJ
  • Cast-as-Intended: A Formal Definition and Case Studies
  • Surveying global verifiability
  • Mind the Gap: Individual- and universal-verifiability plus cast-as-intended don't yield verifiable voting systems
  • Election verifiability in electronic voting protocols

8Helios, Athena, IFL: attacked, repaired, built

  • Score-based decisions: Influence, freedom, legitimacy
  • Athena: A verifiable, coercion-resistant voting system with linear complexity
  • Exploiting re-voting in the Helios election system
  • Verifiability of Helios Mixnet
  • Attacking and fixing Helios: An analysis of ballot secrecy
  • A Fair and Robust Voting System by Broadcast
  • Replay attacks that violate ballot secrecy in Helios
  • A note on replay attacks that violate privacy in electronic voting schemes

Reasoning5

Software is unpredictable, sheer complexity kills intuition; to ensure safety I exhaustively rule out every failure. Read the essay ›

Reasoning5Observational equivalence, applied pi calculus, ProVerif

  • ProVerif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial
  • Automated reasoning for equivalences in the applied pi calculus with barriers
  • Automatically Checking Commitment Protocols in ProVerif without False Attacks
  • Applied pi calculus
  • Formal verification of cryptographic protocols with automated reasoning

Everything61

$ ls -t writing/ | column
2026The Transport Layer Security (TLS) Protocol Version 1.3 · RFC9846, IETFpdf
2025Annotated biography: Free & fair elections · Draftpdf
2025Hooking up with Fiat-Shamir · Draftpdf
2025Score-based decisions: Influence, freedom, legitimacy · Draftpdf
2024Championing tally-then-decrypt secrecy · Draftpdf
2023ProVerif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial · Manualpdf
2022Overcoming Arrow's impossibility: Honeybee sidestep · Draftpdf
2022Surveying definitions of election verifiability · IPLpdf
2021Election Verifiability: Cryptographic Definitions and an Analysis of Helios, Helios-C, and JCJ · IACRpdf
2021Ballot secrecy: Security definition, sufficient conditions, and analysis of Helios · JCSpdf
2021Cast-as-Intended: A Formal Definition and Case Studies · FC'21pdf
2020Surveying definitions of coercion resistance · IACRpdf
2020Mind the Gap: Individual- and universal-verifiability plus cast-as-intended don't yield verifiable voting systems · IACRpdf
2020Surveying global verifiability · IPLpdf
2019Non-malleable encryption with proofs of plaintext knowledge and applications to voting · International Journal of Security and Networkspdf
2019Athena: A verifiable, coercion-resistant voting system with linear complexity · IACRpdf
2019An Overview of GSMA's M2M Remote Provisioning Specification · arXiv—
2019A critique of game-based definitions of receipt-freeness for voting · ProvSec'19—
2019Exploiting re-voting in the Helios election system · IPLpdf
2019TLS 1.3 for engineers: An exploration of the TLS 1.3 specification and OpenJDK's Java implementation · arXivpdf
2018A short introduction to secrecy and verifiability for elections · arXivpdf
2018First-past-the-post suffices for ranked voting · Draftpdf
2018Secret, verifiable auctions from elections · TCSpdf
2018A foundation for secret, verifiable elections · IACRpdf
2018Attacks against GSMA's M2M Remote Provisioning · FC'18pdf
2018Authentication with weaker trust assumptions for voting systems · AFRICACRYPT'18pdf
2018Automated reasoning for equivalences in the applied pi calculus with barriers · JCSpdf
2018Modelling and Analysis of a Hierarchy of Distance Bounding Attacks · USENIX Security'18pdf
2018Verifiability of Helios Mixnet · Voting'18pdf
2017CryptoCache: Network Caching with Confidentiality · ICC'17—
2016Automated reasoning for equivalences in the applied pi calculus with barriers · CSF'16pdf
2015NM-CPA secure encryption with proofs of plaintext knowledge · IWSEC'15—
2015Formal analysis of privacy in Direct Anonymous Attestation schemes · Science of Computer Programmingpdf
2015Automatically Checking Commitment Protocols in ProVerif without False Attacks · POST'15pdf
2015Truncating TLS Connections to Violate Beliefs in Web Applications · Tech Reportpdf
2014Ballot secrecy and ballot independence: definitions and relations · IACRpdf
2014Ballot secrecy with malicious bulletin boards · IACRpdf
2014Forget Me Do: Empowering user privacy on social network sites · Tech Report—
2014Hawk and Aucitas: e-auction schemes from the Helios and Civitas e-voting schemes · FC'14pdf
2013Ballot secrecy and ballot independence coincide · ESORICS'13pdf
2013Truncating TLS Connections to Violate Beliefs in Web Applications · WOOT'13pdf
2013Attacking and fixing Helios: An analysis of ballot secrecy · JCSpdf
2012A Fair and Robust Voting System by Broadcast · EVOTE'12pdf
2012Proceedings of the 8th International Conference on Information Security Practice and Experience (ISPEC'12) · Proceedings—
2012Secure Authenticated Key Exchange with Revocation for Smart Grid · ISGT'12—
2012Replay attacks that violate ballot secrecy in Helios · IACRpdf
2011Adapting Helios for provable ballot privacy · ESORICS'11pdf
2011Formal analysis of anonymity in ECC-based Direct Anonymous Attestation schemes · FAST'11pdf
2011A note on replay attacks that violate privacy in electronic voting schemes · Tech Reportpdf
2011Attacking and fixing Helios: An analysis of ballot secrecy · CSF'11pdf
2011Applied pi calculus · IOS Presspdf
2011Formal verification of cryptographic protocols with automated reasoning · Tech Reportpdf
2011ProVerif 1.85: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial · Manualpdf
2010Election verifiability in electronic voting protocols · ESORICS'10pdf
2010Exploiting Natwest and RBS online banking systems for profit · Tech Reportpdf
2010Five ways to stay safe when using iTunes · Times Podcast—
2010Forgotten your responsibilities? How password recovery threatens banking security · Tech Reportpdf
2010Privacy vs. Usability: A failure of Barclays online banking? · Tech Reportpdf
2010Towards automatic analysis of election verifiability properties · ARSPA-WITS'10pdf
2008Automatic verification of privacy properties in the applied pi-calculus · IFIPTM'08pdf
2007Direct Anonymous Attestation (DAA): Ensuring privacy with corrupt administrators · ESAS'07pdf