Portrait of Markulf Kohlweiss

Markulf Kohlweiss



I am a researcher at Microsoft Research Cambridge in the Programming Principles and Tools group and a member of the Constructive Security sub group.

I did my PhD at COSIC (Computer Security and Industrial Cryptography) group at the Department of Electrical Engineering ESAT of the K.U.Leuven. During my PhD I worked as a researcher in the European PRIME project (Privacy Enhancing Identity Management for Everyone) and PrimeLife project. In prehistoric times, I received a degree of Master in Computer Science (Diplom Ingenieur, Dipl.-Ing.) from the University of Klagenfurt, Austria and visited IBM Research Zurich for my master thesis.

I previously worked on privacy-friendly smart metering, zero-knowledge proofs and malleability, and formal verification of cryptographic protocols, especially modular, code-based cryptographic verification.

My current research focus is on privacy-enhancing cryptography and formal reasoning about cryptographic protocols. More specifically, I examine the interplay of cryptography and real-world security systems through collaborative projects on verifiable computation and SSL/TLS.

Please look at DBLP for my publications. Please also contact me directly if you have any questions on my most recent work.


Project Everest – Verified Secure Implementations of the HTTPS Ecosystem

Established: May 31, 2016

Summary Project Everest aims to build and deploy a verified HTTPS stack. The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle,…

Verifiable Computing

Verifiable computation schemes enable a client to outsource the computation of a function F on various inputs to an untrusted worker, and then verify the correctness of the returned results. Critically, the outsourcing and verification procedures must be more efficient…

The F* Project

Established: March 25, 2011

F* is a verification-oriented dialect of ML. For more information, please visit https://fstar-lang.org or click on the logo below.

Privacy-friendly smart metering

Many smart metering proposals threaten users' privacy by disclosing fine-grained consumption data to utilities. We have designed protocols that allow for precise billing of consumption while not revealing any consumption information to third parties. We also have developped protocols that…

F7: Refinement Types for F#

Established: May 29, 2008

F7 is an enhanced typechecker for the F# programming language, a dialect of ML. F7 pioneers the static checking of security properties expressed with refinement types. Although the original motivation was to check security properties, F7 is not security-specific and…