Why is cryptographic model not considered formal methods?

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?

• Can you give a reference to the second one? Without looking at the actual method one can't really give a correct answer Oct 21, 2016 at 14:31
• 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.
– grochmal
Oct 21, 2016 at 17:01
• The second model is really the standard to evaluate at least primitives. Oct 22, 2016 at 14:43
• 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. Oct 23, 2016 at 11:19