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 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:
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.
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.