Newton Institute - Formal and Computational Cryptographic Proofs

Formal and Computational Cryptographic Proofs
Newton Institute, 10-13 April 2012

This week many of our Bristol students are in Cambridge for a seminar organised by our very own Nigel Smart at the Newton Institute as part of the Turing year.

In one of today's talks, Bogdan spoke about composition of game-based proofs. Games and simulations are the two main means of reasoning about security of protocols. Simulation-based notions claim to be conceptually simpler and especially to offer composition for free - for example the well-known Universal Composability (UC) framework.

Bogdan gave the example of a key-exchange protocol: just having a key is of little use on its own unless you can use that key, for example to transmit encrypted messages. So it is a very natural requirement that a key exchange protocol be composable with other protocols.

Simulation-based approaches have many disadvantages once one takes a closer look. Once one actually has to read or write a proof of a concrete protocol, any suggestion of simplicitly quickly evaporates. Consequently, real-world protocols such as TLS are rarely proved secure in simulation-based models.
Among the disadvantages of simulation, besides the number of conflicting frameworks (UC, JUC, RS, IITM, GNUC just to name some) Bogdan pointed out that the frameworks themselves duplicate features of the protocols such as session identifiers. There are also complexities involving joint state between sessions and particularly with adaptive corruption of parties.

Instead, Bogdan (joint work with several others) proposed to look at composition of game-based notions. Security games are in fact not wholly unamenable to compositional proofs, even generic ones: Bogdan gave a theorem that allowed composition of a key-exchange protocol secure in the Bellare-Rogaway (game-based) model with any other protocol as long as the key exchange has the property that partnered sessions are easy to identify.

This covers SSH, IKE and a few others but not TLS (which is not BR-secure). The reason is that the TLS key establishment protocol already uses the derived session key for an encryption, disallowing any clean separation between establishment and use of the session key.
Even this problem can be solved though and the technique is to consider protocols proved secure from primitives by means of a so-called "key independent reduction". This essentially means that the protocol only uses the key via the primitive, allowing the triple of key agreement, primitive and protocol in TLS (the primitive is length-hiding authenticated encryption with a minor restriction) to be proved secure in a generic and modular way from game-based notions.


I think this work is important in several ways. It is obvious that we need composable security notions. The claim that simulation-based notions are the best (or even only) way to reliably get composition has never convinced me personally. My main reason for liking game-based proofs is that they feel much more natural and intuitive to me: not only do I find it much easier both to read and write proofs in game-based models but they also provide better conceptual links between the techniques in the proofs themselves and informal or "intuitive" notions of security.
The techniques employed in game-based proofs, from reductions to hybrid arguments, are often compositional in nature (in a recent paper for example we composed DAA out of various cryptographic "building blocks" and proved the DAA scheme secure in a modular and compositional manner) - but until now each composition had to be done by hand. The line of work presented today could, so I hope, lead to much easier notions of composing game-based proofs.