Tag Archives: Thesis

Ph.D. Thesis

It’s taken too long, it’s taken too much energy, but my thesis is finally done!

Part exhaustion, part laziness, and part lack of time, it ended up being a collection of my previous papers with a brand new unifying introduction stuck in front: under the title Symbolic Analysis of Cryptographic Protocols – Models, Methods, and Soundness I’ve gathered the full version of the Japanese paper, one of the French papers, and the full version of the Aarhus Eel. It turns out (I really haven’t been very streamlined in my research) that besides symbolic models and cryptographic protocols the three papers are also related through the expressive power vs usability scale: the Japanese paper aims for an efficient method suitable for non-experts, while the Aarhus Eel exchanges the hope for non-experts with an expressive power fitting for advanced modern cryptographic protocols such as secure computation. It took a while to screw this link together but it was a good day when it happened.

Obviously there was the small devil in my head longing for writing everything into a long proper monologue, avoiding the duplications and making it seem as if I have been a lot more streamlined during the last few years, but here, at the end, he has been far easier to keep quiet than I imagined — being done has been pretty hard to beat. Not that I’m unhappy with the outcome by the way, not at all; this is only about its ‘visual appearance’, and underneath it would have been exactly the same.

The next step now is for it to go through revision by my committee and then hopefully getting accepted. But for now it’s no-writing-and-no-computer for a while!

Master’s Thesis

It’s been some years now since this was produced, yet working with type systems recently I figured it was worth putting my master’s thesis online as well. It didn’t contain any break-through results, but I remember being content with its ridged formulations and proofs, and its self-containment — it even including a section in the appendix outlining the entire approach in the form of a tiny and easy-to-understand type system.

From the abstract:

In this paper we give a type inference algorithm for a type system for a pi calculus. The effect type system with dependent types guarantees that well-typed processes respect an authenticity property expressed as correspondences.

Given a process and a type context we generate constraints that are satisfiable if and only if the process can be made well-typed under the context. […] The output of the algorithm can be used to efficiently construct a proof of safety in the form of a derivation tree.

Experiments with a Caml implementation have shown that the algorithm performs well in praxis.

A small paper based on the thesis was presented at Nordic Workshop on Programming Theory 2008 (NWPT’08), and it also served as the basis for a later paper on a more advanced type system, presented at Workshop on Foundations of Security and Privacy 2010 (FCS-PrivMod’10).