FOSAD '12

This year's workshop on Foundations Of Security Analysis and Design is taking place at Bertinoro, as usual - a great location, in my opinion all security conferences should be held in castles. The only downside is it's been raining for most of the week so far, not helped by Mark Ryan from Brimingham starting his talk with the forecast of sunshine back home!

Mark's talk, spread out over two days, went into details of the ProVerif system and its aapplications. ProVerif is a protocol verifier that uses formal methods to try and prove security properties of protocols.

Day one covered the theory part, the syntax and as much semantics as you can fit into a slideshow. The basic construct is a predicate knows(-) to model data that the adversary could potentially discover from a protocol.
All operations take place on abstract data types specified by an equational theory. For example, the equation for public-key encryption is

dec(sk, enc(pk(sk), m, r)) = m

 ProVerif turns these equations into Horn clauses to construct a model of the system in first order logic.
For encryption, one clause is

knows(sk) & knows(enc(pk(sk), m, r) -> knows(m)

which states that if the adversary gets hold of a ciphertext and its key, then he can compute the message.

A type of security property can be modeled by checking that knows(s) is false for some secret s. ProVerif will try and derive knows(s) from the equational theory and present either an attack (a derivation of knows(s) ) or conclude that no such derivation exists (i.e. the protocol has the security property) - or, it will do something else.

ProVerif deliberately overestimates the adversary's capabilities to guarantee that if it terminates without finding a derivation, then none exists.
Apart from proving or disproving security, ProVerif can also turn up false positives - attacks that arise from its oversetimation of the adversary but that can't be launched in practice. If this happens, you need to rewrite your formalisation to exclude these attacks; Mark gave some tips and tricks for how to do this.
Finally, ProVerif can fail to terminate. This is in fact the usual case (at least when "hasn't completed when I come back at the end of my lunch break" is taken as evidence of non-termination), which is not so surprising when you consider that ProVerif is essentially trying to solve an undecidable problem,  hoping to hit on a decidable edge case.

In his second talk, Mark Ryan gave two applications to e-voting and the TPM. Both of these involve complex protocols and while a ProVerif "proof", like any other security "proof", has its limitations, it's definitely a good thing to consider to provide some level of assurance that a protocol achieves a security objective.