Tag Archives: Paper submission

Universally Composable Symbolic Analysis for Two-Party Protocols based on Homomorphic Encryption

Retrospectively dubbed The Aarhus Eel for it’s ability to repeatedly avoid capture yet good juicy taste when it finally gave in, we yesterday submitted the result of more than a year’s worth of research!

It started with my supervisor saying “Wouldn’t it be nice to have a paper uniting your previous work (symbolic analysis) with your new work (secure computation)?” and me replying “Oh, it would, and it shouldn’t take that long!“.

This was summer 2012, followed by an autumn working out backwards what would be nice to have. For the following Christmas I managed to give my self the present of finally knowing where we wanted to go; concretely, we now had a model of an interesting protocol and its security requirements that we could analyse with current tools (ProVerif). The rest, I thought, would be somewhat straight-forward.

Spring came and went. Summer came and went. Terribly frustrating period to be honest, with some progress but mostly a lot of unforeseen problems, dead ends, and steps back. My view of the project go switch from motivated to hopeless, from relevant to useless, all within a few days. Not only did was a tired after work during this period, insecurities also started to creep in from the fear of spending this much time on something that might be trivial.

Then during autumn the proofs we needed finally started to form. There were far too many details in them to comfortably keep in my head at once so progress was still slow and often felt highly redundant: at this point, changing a small thing to get past an obstacle meant at least an hour or two reworking the proofs and checking that it didn’t break down somewhere else.

Around winter we settled for the technical material and I started working on applications, presentation, and polishing. This meant escaping the mind-filling proofs, and from seeing a product taking its final form motivation started to come back. The pressure of also having a thesis to finish replaced any last resistance to ever go over the report again with a pure mechanical approach of just finishing.

And after making a short 12-page version we then finally submitted the work to Crypto ’13 yesterday! Oh yay, oh yiy, the joy!

Here’s the abstract:

We consider a class of two-party function evaluation protocols in which the parties are allowed to use ideal functionalities as well as a set of powerful primitives, namely commitments, homomorphic encryption, and certain zero-knowledge proofs. With these it is possible to capture protocols for oblivious transfer, coin-flipping, and generation of multiplication-triple.

We show how any protocol in our class can be compiled to a symbolic representation expressed as a process in an abstract process calculus, and prove a general computational soundness theorem implying that if the protocol realises a given ideal functionality in the symbolic setting, then the original version also realises the ideal functionality in the standard computational UC setting. In other words, the theorem allows us to transfer a proof in the abstract symbolic setting to a proof in the standard UC model.

Finally, we have verified that the symbolic interpretation is simple enough in a number of cases for the symbolic proof to be partly automated using the ProVerif tool.

Joint work with Ivan Damgård, and with thanks to Ran Canetti at Boston University and Hubert Comon-Lundh at ENS de Cachan.

Update, 25 May 2013: the full version is online as IACR ePrint report 2013/296.

Update, 15 October 2013: after rejection from Crypto due to lack of full proofs, we have now added these from the full version and re-submitted to Eurocrypt 2014.

Update, 14 January 2014: the paper was been accepted for Eurocrypt, hurray!

Update, 21 March 2014: finally got around to clean up some of the ProVerif source files enough to not be ashamed of releasing them (DNO08 OT protocol)

Update, 15 May 2014: as the final talk of the conference I presented the paper today, thereby putting a nice end to the last PhD paper! (presentation slides, intentionally kept somewhat high-level as this literally was the end of a packed four conference)

Japanese Paper Submitted

We’ve just submitted what I’ve been referring to as “the japanese paper”!

Written together with professor Naoki Kabayashi and his student Yunde Sun this was my first time working with Japanese people. It didn’t make a huge difference. I installed a Dashboard widget to easily show what time it was in Japan (8 hours ahead), and that was more or less it. Naoki was very polite and fair, and the whole experience has left me thinking that spending some time in Japan might not be a bad idea.

For the more technical stuff, the paper deals with how to enable a computer to automatically analyse security protocols for errors. The motivation behind this is that human designers of these protocols are notorious for missing critical details that years later allow some bad guy to do some nasty stuff. Giving these designers computer tools to verify the details is the essence of our work. The formal abstract is as follows:

Gordon and Jeffrey developed a type system for verification of asymmetric and symmetric cryptographic protocols. We propose a modified version of Gordon and Jeffrey’s type system and develop a type inference algorithm for it, so that protocols can be verified automatically as they are, without any type annotations or explicit type casts. We have implemented a protocol verifier based on the algorithm, and confirmed its effectiveness. We also formally investigate the relationship between Gordon and Jeffrey’s type system and ours.

We have submitted the paper to the Computer Security Foundations 2011 Symposium (CSF ’11) and will know whether it is accepted or not by the end of March.

Today also marks the end of a rather busy period! It’s been too much. At the level you can only keep for a short time and where physical symptoms start to show (in this case chest pains). Three sweet sweet weeks of vacation awaits me now :).