February 2013

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)

First Shots from Olympus OM-1

When we took the darkroom course our teacher Barbara would dismiss our every mistake with a “it’s good that we come across this now so you know what to do”. Taking it perhaps a bit too literally we’ve since continued to discover how safe one actually is when shooting digital. For instance, you don’t have to worry about dropping the raw film on the floor when trying to put it on a spool in complete darkness; nor about keeping your cool when running out of correctly tempered water in a situation where seconds make a difference; nor about closing the box of unexposed paper properly before turning on the light.

And this brings me to the title of this post: it was supposed to say First Shots from Olympus OM-1 and OM-2, and it was supposed to be even more exciting by including shots from a newly acquired lens. However, apparently there was a lesson that needed to be illustrated more vividly before sinking into my head: when loading a film make sure that the crank has a proper grip on it and is really rolling it out. This is very easy to test by the way, by simply noticing if the rewind wheel is turning with the crank.

I didn’t do this test I suppose, with the result that after opening the tank with the developed film from the OM-2 I was very surprised to find a film completely blank, without any marks of light ever hitting it. For a second the camera was the suspect, but only until I was ready to accept my responsibility. Lesson learned, and the OM-2 with the lens is already making it’s way through a new film.

On the other hand, the film from the OM-1 turned into splendid negatives, here scanned with my new Epson V600 scanner:

Having used the batteries that’s been in the camera for 20-25 years I had a certain scepticism towards the light meter, but as it turns out this was entirely without cause.

One thing to notice though: the water marks. This was the first time I didn’t use a wetting agent and it clearly shows — another lesson learned.

Langhoff & Juul, Aarhus

This summer a new place opened just across the street from us that could potentially be very hipster: they only serve organic food, and in an environment that most of all reminds me of the wooden cabin we stayed in during our weekend in Norway. We’ve been there a few times — for coffee, for a sandwich, and now for brunch — and so far they’ve steered clear of the undesirable label (either that, or I’m more hipster than I realise).

The food is good, and although the plates are not amazingly huge, I haven’t actually walked away from it hungry. The prices are not in the cheap end nor expensive, yet not more than what I’m willing to pay for organic food in a good atmosphere. The waiters are kind and welcoming, and without baggy trousers, top hats, Ray-Ban sunglasses, or analogue cameras (I fit with two of these).

The bottom line is that Langhoff & Juul comes recommandable, and with a hope that they are actually trying to make a modern and honest café that is not just following the latest hipster fashion (unlike for instance the awful Joe & the Juice); this is not easily done but so far they manage it very nicely.