Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
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 am working on privacy-preserving applications of cryptography, zero-knowledge proofs and malleability and formal verification of cryptographic protocols. My current focus is on secure communication and real-world protocols such as TLS/SSL.

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 pre-historic 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.

Please look at DBLP for my publications. The information below may be outdated but might contain nuggets that cannot otherwise be found online. Please also contact me directly if you  have any questions on my most recent work.

Selected Publications

More publications...


F7: Refinement Types for F#.

F*: The successor of F7, an ML-like functional programming language aimed at program verification. Programs written in F* can be translated to OCaml or F# for execution.

Privacy-friendly smart metering We have designed protocols that allow for precise billing of consumption while not revealing any consumption information to third parties. We also have developed protocols that allow for privacy-friendly real-time aggregation of smart-meter readings.

Verifiable Computing Verifiable computation schemes enable a client to outsource a computation to an untrusted worker that derives the result together with a proof of its correctness. Crucially, verifying the proof must be more efficient for the client than computing the result.

miTLS: A verified reference implementation of the TLS protocol. Verification is based on a modular code-based cryptographic verification methodology based on types and idealized implementations of cryptographic primitives.



2005-2010 Ph.D., K.U. Leuven, Belgium

Nov 2002–May 2003 Internship as Master’s Student at IBM Zurich Research Laboratory

1997-2004 Dipl Ing., Computer Science at Universität Klagenfurt, Austria


email: markulf at microsoft com
tel:  +44 (1223) 479934 934