How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. - David Butler 002; David Aspinall 001; Adrià Gascón (ITP, 2017)

On the Formalisation of Σ-Protocols and Commitment Schemes. - David Butler 002; David Aspinall 001; Adrià Gascón (POST, 2019)

Multi-Party Computation. - David Aspinall 001; David Butler 002 (Arch. Formal Proofs, 2019)

Sigma Protocols and Commitment Schemes. - David Butler 002; Andreas Lochbihler (Arch. Formal Proofs, 2019)

Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL. - David Butler 002; David Aspinall 001; Adrià Gascón (IACR Cryptol. ePrint Arch., 2019)

Formalising Σ-Protocols and Commitment Schemes using CryptHOL. - David Butler 002; Andreas Lochbihler; David Aspinall 001; Adrià Gascón (IACR Cryptol. ePrint Arch., 2019)

TraceSecure: Towards Privacy Preserving Contact Tracing. - James Bell 001; David Butler 002; Chris Hicks; Jon Crowcroft (CoRR, 2020)

SecureABC: Secure AntiBody Certificates for COVID-19. - Chris Hicks; David Butler 002; Carsten Maple; Jon Crowcroft (CoRR, 2020)

Differentially Private Health Tokens for Estimating COVID-19 Risk. - David Butler 002; Chris Hicks; James Bell 001; Carsten Maple; Jon Crowcroft (CoRR, 2020)

Formalising cryptography using CryptHOL. - David Butler 002 (2020)

Formalising $ varSigma$-Protocols and Commitment Schemes Using CryptHOL. - David Butler 002; Andreas Lochbihler; David Aspinall 001; Adrià Gascón (J. Autom. Reason., 2021)