2
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. $\endgroup$ – e-sushi Dec 17 '17 at 13:17
4
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. $\endgroup$ – e-sushi Dec 17 '17 at 13:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.