Markulf Kohlweiss
Markulf Kohlweiss
Associate Professor (in British, Sr. Lecturer)
School of Informatics
University of Edinburgh
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.


Ouroboros Crypsinous

Ouroboros Crypsinous thei first formally analysed privacy-preserving proof-of-stake (PoS) blockchain protocol is now on ePrint.

State-separating proofs

Our paperState-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.


Security news

A Few Thoughts on Cryptographic Engineering by Matthew Green
Schneier on Security by Bruce Schneier


Current advisees:
Past advisees:

Personal Tutor



My research lie at the intersection of

My research is supported by the IOHK and Microsoft Research.


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
Int. J. Inf. Sec. 17(1) article
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
SNAPL 2017 article
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
POPL 2016 article
Light at the middle of the tunnel: middleboxes for selective disclosure of network monitoring to distrusted parties
Nik Sultana, Markulf Kohlweiss, Andrew W. Moore
HotMiddlebox@SIGCOMM 2016 article
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
PoPETs 2015(2) article

Other Things


Project Everest aims to build and deploy a verified HTTPS stackwebsite
An implementation of the TLS protocol, written in F*website
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