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