CSF day 3

Monday's invited talk was Gilles Barthe on advances in easycrypt - I really need to learn how to use that some day, probably at the Paris winter school this November that was announced in one of the short talks today. One of the more interesting points was that most cryptgraphic proofs are variations on the same five techniques: two that introduce fresh randomness (replacing x XOR r with r when r is fresh random; replacing H(x) with fresh r if H is a hash or similar), two that propagate trace properties (by construction and by reduction) and one for propagating indistinguishability.

As a case study, Barthe discussed OAEP and a few hundred variations thereof, parametrising them as a kind of Feistel network with several points where optional randomness can be added and then proving or disproving security of many instances of this model.

In the session on protocol verification, several authors turned their attention to key-exchange protocols. We're not short of models in this area but I find the formal-modelling approach a welcome addition to the area, particularly for its tendency to provide a concrete attack with each failed proof.

While the general probem "Is my Diffie-Hellman type protocol secure?" is undecidable in the formal world, Dougherty and Guttman showed that for a certain class of "lightwieght" protocols, a decision procedure exists. Their approach has two novel components: first, rather than just considering a term algebra, they explicitly model the exponent field as a finite field. Secondly, they show a finite-model theorem that gives the required decidability: a common problem in formal approaches to key-exchange protocols is that you can easily check whether or not there are any attacks that use at most 0, 1, 2, ... sessions but extending this to an unbounded number of sessions is undecidable. The class of lightwieght protocols in the talk have the property that one can find a bound b such that if there is any attack, there is also one with at most b sessions. This looks like a very promising approach to me that I'd hope one can generalise to more protocols: with a suitable bound, one hopes that one could let loose a theorem prover to "clean up" the rest of the problem.

The session ended with Mödersheim and Katsoris addressing the parsing problem. We know from Paterson et al. that there is a big difference between MAC-then-encrypt and MAC-then-pad-then-encrypt; the key to such TLS attacks as Lucky 13 is that the adversary can maul a message to change the way it is parsed. Any analysis of a protocol in a symbolic model with a term algebra operates at too high a level to capture such attacks, as a model of a term algebra implies a perfect encoding/parsing scheme. The mentioned paper refines a formal model down to the byte level and applies this to among other things the XML format and (simplified) TLS messages. A result of the paper is some easy to verify conditions on formats that could well be put to practical use, both for designers/implementors of new message formats and for security analysts who now have a tool to extend their symbolic model to the level of bits and bytes.