# how much trust can we place in protocol verifiers? [closed]

I read many papers on authenticated key exchange protocols, and most security proofs are done by the authors. In this method, you can imagine that the efficiency is low. Moreover, even if you have proven an AKE protocol's security under a certain model (say eCK), you still cannot ensure the security under all other models, including real life.

This lead me to ask: Can verify protocol's with some automated tool, for example Tamarin? This would be very efficient after all. My initial worry would be whether this will be accepted by people and as convincing as the traditional way?

-
Related, possibly duplicate: Is there an automated security protocol verification tool? –  Ilmari Karonen Oct 8 '13 at 20:36
no ,it's not that –  Alex Oct 8 '13 at 23:50
This is not a duplicate but off-topic nevertheless. It's a good question but it belongs on Security.SE with the title "how much trust can we place in protocol verifiers" or similar. Cheers –  rath Oct 9 '13 at 4:50
@rath i agree with you! but the answer i want is in Cryptography –  Alex Oct 9 '13 at 10:23
Do you think that there is an objective answer to this question or will the answer be necessarily opinion based? –  mikeazo Oct 9 '13 at 16:44
show 1 more comment

## closed as primarily opinion-based by e-sushi, rath, Maeher, B-Con, Ricky DemerOct 18 '13 at 6:09

Many good questions generate some degree of opinion based on expert experience, but answers to this question will tend to be almost entirely based on opinions, rather than facts, references, or specific expertise.If this question can be reworded to fit the rules in the help center, please edit the question.

We know that traditional mathematical proofs can contain mistakes, and that these mistakes can remain undiscovered for years. Sometimes, the scheme is secure even if the proof is incorrect, e.g. RSA-OAEP. Sometimes, the scheme is mildly flawed, the flaws undiscovered because of mistakes in the proof, e.g. HMQV. And sometimes a scheme is simply insecure.

We know that formal systems can fail to describe the real world and therefore prove incorrect results, e.g. BAN logic, but nowadays formal systems seem much more complete.

Formal systems typically work with idealized cryptography. It is sometimes possible to prove that some idealization is sound, but in general this is difficult. Which means that in principle, it might be possible to design schemes that are secure in the formal system, but insecure regardless of what cryptography is used to instantiate the formal object. Similar results exist for the random oracle model and the generic group model, but still the random oracle model is considered a good heuristic for security in the real world (the generic group model less so).

Many systems restrict attention to various forms of encryption and digital signatures. This is in some sense good, because it is likely that the idealization is sound. On the other hand, you often cannot even express Diffie-Hellman in the formal system, which means that it is less useful. Where Diffie-Hellman can be expressed, the group model is often very limited, which means that the formal system might be unable to express various attacks involving subtle properties of groups, and as such it is much less clear how sound the idealization is.

The end result is that formal systems with tool support that are sound and capable of modeling the schemes you are interested in are useful and often very easy to work with. Traditional mathematical proofs are useful, but they are difficult to work with.

-
That's more thorough and you'll get the best out of both worlds. so what if there's a test case the tool doesn't cover? I'm sorry if I'm making a mistake, I've never used such a tool before so I don't really know how they work –  rath Oct 9 '13 at 20:35