Who watches the watcher?

Formal proofs are nice. Programs like proverif are even nicer, because they do the work for you.

It means that we have a way to check for the correctness of our model, independently from our implementation.

…But what happens when there is a mistake in the formal proof?
And how do we fix it?

Proverif

Proverif is a tool for automated reasoning and checking of cryptographic protocols. It can use pi-calculus and typed pi-calculus.

The protocol can be defined in a way that is simple enough, and the cryptographic primitives can be modelled, without the actual implementation.
The two main modes, without type (default) and with types (optional) lets us try different things:

without types: a more complete solution, tries to unify every message and submessage with any other message and submessage. This can spot attacks where the types are not checked. For example we could send a bunch of data that the server thinks is a nonce, and that gets signed, but it actually is a key exchange and not the attacker can sign any data with the server keys, without having it. Complexity is a problem: it’s easy to understand why.
with types: Less complete but much more performant solution. It can be used if the server somehow checks that the data he handles corresponds to to a particular format, so that the previous situation will never happen.

Fenrir proofs

Fenrir proofs for various cases are available here.

There are checks for the secrecy of keys and authentication data, for downgrade attacks and for rogue/compromised authentication servers.
It always made me feel safe to know that some automated tool told me everything was alright.

A bit too safe.

Some days ago I needed to check how I designed a part of the handshake, and discovered a nice little bug in the proof. Proverif still took its time to crunch all data and try to make all possible inferences, but there was a slight problem:
due to the bug, the protocol could not do a full connection.

Ouch. That’s bad. How did that happen? Well, to be fair, it is not proverif’s jobs to know if we meant what we wrote or if we had bugs in our implementation.

But it is the old question, “who watches the watcher?”. In this case, nothing did.

Updated proofs

The good news is: I have fixed and run again all proofs, and they still hold! Nice!
The “bad news” is: we now have to use the typed proverif version, since the complexity has risen too much. Still, we always check for formatted data, and never blindly sign something we received from the client.

The previous link now contains updated proofs.

But how do we make sure this does not happen again? Simple, we tell proverif to check that there actually is a way to reach the end of the connection.

This means that there are now 3 more tests that HAVE TO FAIL. Unfortunately I could not understand how to make proverif check that something happens without marking it as a possible violation of the proof.
The first 3 tests “connection_full” “connection_state” and “connection_dir” now check that we can actually reach the point where a connection has been made in the 3 different handshakes.

The proof has gotten quite heavy to compute… on my core i7-3630QM (3.2ghz in turbo):

real	120m10.932s
user	120m9.686s
sys	0m0.413s

So now there are different proofs you can enable and disable at the end of the proverif files. all of them are complementary and independent.

Proverif actually has a way to use more “phases” that are independent, but adding phases make things terribly slow, even if they are empty phases.
So be ready to let your computer waste some time :)

– Who watches the watcher? The watcher, obviously.

-Luker