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

Answers surely will be somewhat opinion-based, as no one can really say if manual checks are more or less convincing than automated checks. After all, both can be convincing if communicated/sold successfully to third parties.

From my personal point of view, the best approach would be to manually verify the results of automatic verifications. So, first automatic verifications and then manually checking/verifying the positive and negative results produced by the automatic verification tool(s). That's more thorough and you'll get the best out of both worlds.

Besides that, please remember there is no such thing like "100% security".
We can come close, but we'll most probably never be able to reach perfect security.

-
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
@rath Well, if you can't find a tool to test and/or verify a specific case or implementation, logic implies you have no other option than to rely on manual verification alone. If you're a bit of a coder, it would make sense to create a software solution that's able to handle that specific case (if possible and if it makes sense). When done, you could either sell that software or provide it as a free download, depending on how capitalistic your endeavors are. ;) So: use software + independently verify manually, compare results of overlapping verifications, finally combine it all into 1 report. –  e-sushi Oct 10 '13 at 14:33
@rath Simple think "double-verification" (manual + software) for cases and areas where you have software-tools available, as that has the ability to double the human trust-factor in your report. Only when it's widely accepted that a specific software tool is able to perfectly check a specific case, I would be considering relying on software verification alone. But fact is, I have yet to meet a case where people didn't ask: "Have you cross-checked those software verification results?" So, in the end I personally always ended up with an additional manual verification to make reports trustworthy. –  e-sushi Oct 10 '13 at 14:41