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…
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 am currently focusing on privacy-friendly smart metering, zero-knowledge proofs and malleability, and formal verification of cryptographic protocols, especially modular, code-based cryptographic verification.
Please look at DBLP for my publications. Please also contact me directly if you have any questions on my most recent work.
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.
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…
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…