I am associate professor in the
Security and Privacy research group at the University of Edinburgh. I hold a PhD in cryptography from
COSIC at the K.U. Leuven and previously was a researcher at Microsoft Research Cambridge in the
Programming Principles and Tools group.
I worked on the
Identity Mixer anonymous credential system at IBM Research Zurich and I am a founding member of the miTLS project, now
project Everest, a verified implementation of the TLS standard. For the latter work I am a co-recipient of received the Levchin prize for real-world cryptography.
I am looking for motivated PhD students with interest in cryptography, blockchain technologies, security, and/or formal verification. If you are already a student at the University of Edinburgh drop by my office to discuss.
News
Ouroboros Crypsinous
Ouroboros Crypsinous thei
first formally analysed privacy-preserving
proof-of-stake (PoS) blockchain protocol is now
on
ePrint.
State-separating proofs
Our paper
State-Separating Proofs: A Reduction
Methodology for Real-World Protocols (joint work with
C. Brzuska, A. Delignat-Lavaud, K. Kohbrok) is available
on
ePrint
now.
One of the goals of the paper is to reduce
suffering when writing and reading real-life protocol
reduction proofs, to make them readable and verifiable and
also shorter and more precise. To get a good idea about
the potential for simplification, look at the original
proof of the miTLS, TLS 1.2
handshake, ePrint.
The navigation elements on this page and many layout
elements are heavily inspired by and adapted
from Mike
Rouselek's homepage. The similarity between the
definitional style of our paper and his
textbook,
The Joy of Cryptography, are, however, due to our
independently formed believe that it is more accessible
than what is "traditional" in crypto.
In our paper we also make the case that this style is
more composeable, scaleable, and amenable to formal
verification.
The updatable CRS model
Our paper
Updatable
and Universal Common Reference Strings with Applications
to zk-SNARKs (joint work with Jens Groth, Mary
Maller, Sarah Meiklejohn, Ian Miers) is available
on
ePrint
now.
The goal of the paper is to replace the zcash ceremony
which is bordering on the paranoid (listen to a
great
radiolab
episode) with publicly verifiable non-interactive CRS
updates.
Teaching
Security news
A Few Thoughts on Cryptographic Engineering by Matthew Green
Schneier on Security by Bruce Schneier
Mentoring
Personal Tutor
Research
My research lie at the intersection of
- formal verification,
- foundations of cryptography and
- applied cryptography, especially with regard to
- privacy-enhancing protocols, blockchains, and crypto currencies and the
- formal verification of protocol implementations.
My research is supported by the IOHK and Microsoft Research.
Publications
More bibliographic information is also available on my Google scholar page and DBLP page. For most publications I include a link to a free version of the article; however, some papers are behind paywalls. Send me email if you would like a copy of paywalled publications.
Privacy-preserving smart metering revisited
Alfredo Rial, George Danezis, Markulf Kohlweiss
A messy state of the union: taming the composite state machines of TLS
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cedric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
Commun. ACM 60(2): 99-107 (2017)
article
Everest: Towards a Verified, Drop-in Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cedric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay R. Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue
Implementing and Proving the TLS 1.3 Record Layer
Antoine Delignat-Lavaud, Cedric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin, Karthikeyan Bhargavan, Jianyang Pan, Jean Karim Zinzindohoue
IEEE Symposium on Security and Privacy 2017
article
miTLS: Verifying Protocol Implementations against Real-World Attacks
Karthikeyan Bhargavan, Cedric Fournet, Markulf Kohlweiss
EEE Security & Privacy 14(6): 18-25 (2016)
article
Constant-Size Structure-Preserving Signatures: Generic Constructions and Simple Assumptions
Masayuki Abe, Melissa Chase, Bernardo David, Markulf Kohlweiss, Ryo Nishimaki, Miyako Ohkubo
J. Cryptology 29(4): 833-878 (2016)
article
Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data
Dario Fiore, Cédric Fournet, Esha Ghosh, Markulf Kohlweiss, Olga Ohrimenko, Bryan Parno
ACM Conference on Computer and Communications Security 2016
article
Dependent types and multi-monadic effects in F
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella Béguelin
Light at the middle of the tunnel: middleboxes for selective disclosure of network monitoring to distrusted parties
Nik Sultana, Markulf Kohlweiss, Andrew W. Moore
Cinderella: Turning Shabby X.509 Certificates into Elegant Anonymous Credentials with the Magic of Verifiable Computation
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Bryan Parno
IEEE Symposium on Security and Privacy 2016
article
Downgrade Resilience in Key-Exchange Protocols
Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella Béguelin
IEEE Symposium on Security and Privacy 2016
article
Accountable Metadata-Hiding Escrow: A Group Signature Case Study
Markulf Kohlweiss, Ian Miers
Other Things
Projects
Everest
Project Everest aims to build and deploy a verified HTTPS stack
website
miTLS
An implementation of the TLS protocol, written in F*
website
HACL*
A verified library of cryptographic primitives written in F*
website
Professional Service
I have served on the following program committees (reverse chronological):
PKC 2019;
EuroS&P 2019;
CRYPTO 2018;
PETS 2018, 2017, 2016, 2015, 2014, 2013;
PKC 2018, 2017
ASIACCS 2017;
FC 2016;
CCS 2016;
IMACC 2015;
EUROCRYPT 2015;
SOFSEM 2014;
WPES 2013;
ESORICS 2013, 2012;
ARES 2013,2011;
CT-RSA 2011;
CMS 2011, 2010;
COMPSAC 2009