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, with headline-grabbing attacks such as FREAK and LogJam and emergency patches many times a year. Project Everest proposes to solve this problem by constructing a high-performance, standards-compliant, and verified implementation of the full HTTPS ecosystem. We…

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 than performing the computation itself. In more detail, we introduce and formalize the notion of Verifiable Computation, which enables a computationally weak client to "outsource" the computation of an arbitrary function F on…

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 allow for privacy-friendly real-time aggregation of smart-meter readings. Information computed on the basis of fine-grained smart-meter readings has multiple uses within the energy industry, including billing, providing energy advice, settlement,…

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 is applied in other areas, such as database modelling. The theoretical core of F7 is the typed lambda-calculus Refined Concurrent FPC, or RCF for short. FPC itself is Plotkin and Gunter's lambda-calculus with function, sum,…