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

Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

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)

Leave a Reply

Your email address will not be published.