6
$\begingroup$

I have just started looking at different methods for analyzing the security of cryptographic protocols. According to my reading, there are two main approaches in this area. The first approach is so-called Dolev-Yao (or formal) model, where cryptographic messages are represented as symbolic terms in term algebras. The second one is closer to real implementations of cryptographic protocols, where primitives are seen as probabilistic algorithms and the attacker is a polynomial-time probabilistic Turing machine. The security of cryptographic in the latter approach is often defined as security games.

My confusion is that the former approach is referred as formal methods in the literature, but not the second one. Looking at the definition of formal methods in Wikipedia, it says "formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems". According to this definition, I do not see why the second approach cannot be seen as formal methods. In fact, the first one is just one abstract level higher than the second one and provides weaker security guarantees. So to my understanding, they are both formal verification techniques for security protocols, and therefore should be both seen as formal methods. Could anyone help me to clarify this?

Improve this question
$\endgroup$
4
  • $\begingroup$ Can you give a reference to the second one? Without looking at the actual method one can't really give a correct answer $\endgroup$
    – Limit
    Oct 21, 2016 at 14:31
  • $\begingroup$ This is really a full on cryptography question. cryptography.SE should be the place for it, you should flag your own question and ask for it to be moved there. $\endgroup$
    – grochmal
    Oct 21, 2016 at 17:01
  • $\begingroup$ The second model is really the standard to evaluate at least primitives. $\endgroup$
    – SEJPM
    Oct 22, 2016 at 14:43
  • $\begingroup$ Thank you all for the comments! The formal model (the first approach) is sometime preferred due to its nature of simplicity and support for full automation. Security proofs in the second approach are often hard to understand and highly error-prone. As @grochmal pointed out, maybe this question should be moved to cryptography section. I nevertheless appreciate a lot your effort to help me with this confusion. $\endgroup$
    – Nguyen
    Oct 23, 2016 at 11:19

1 Answer 1

Reset to default
3
$\begingroup$

Disclaimer: I'm currently doing a PhD in Formal Methods and Cryptography and I'm not really sure of my answer.

The first application of Formal Methods is to be applied to pieces of software. The goal is to prove security properties on them. These are usually safety critical softwares (those you find in planes, trains, nuclear facilities...) This field is called Software Verification.

I mostly consider Formal Method as a way of arguing, a way of thinking or proving. In this case, Formal means without ambiguity. Thus you could consider any approach with such mindset in the domain of Formal Methods.

To answer your question, [from my point of view,] both approaches qualify as in the Formal Methods (and I don't see why they should not).

E.g. Easycrypt, a tool to make proofs in game based model and probabilistic models is based on Why3. And I'm pretty sure that Why3 is part of the Formal Methods approach using theorems provers and SMT solvers such as Alt-Ergo or Z3.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Formal methods in the literature refer to Dolev-Yao model (or sometimes symbolic model). Cryptographic model (sometimes called computational model) refers to more realistic world, where messages are bitstrings (so there are not symbols). Easycrypt is the tool for providing proofs in computational model which is based on probabilistic games. There are also tools for symbolic verification (Dolev-Yao adversary models) such as Scyther, Tamarin, ProVerif,... $\endgroup$
    – Nguyen
    Oct 24, 2016 at 7:04
  • $\begingroup$ There are a lot of papers on the distinction between these two models and how to bridge the gap between them. You can take a look at this paper: web.cs.ucdavis.edu/~rogaway/papers/equiv.pdf for instance. $\endgroup$
    – Nguyen
    Oct 24, 2016 at 7:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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