# Is there a formal language to define a cryptographic protocol?

I wanted to work on a personal project where I would attempt to identify the flaws in a cryptographic protocol. Now for that to work properly, the program should understand the syntax of protocol definition (if any). So I wanted to know if there is any formal language to define a cryptographic protocol.
I found a paper but I don't know if everyone actually follows this or not.

• There are a bunch of protocol verification tools (with their own languages), but there's no standard for protocol description like ASN.1 AFAIK (-> I don't know for sure -> no answer). – SEJPM Oct 21 '16 at 19:48
• Probably the closest would be cryptol. – mikeazo Oct 21 '16 at 19:56
• I'd suggest the use of languages used for finding cryptographic proofs (SAT solvers). They also require the problem to be specified formally. I haven't used them much though. – Maarten Bodewes Oct 21 '16 at 20:40
• @mikeazo and others, is there a reason why there is no formal language or is it just not needed? – Limit Oct 22 '16 at 23:35

Disclaimer: I use Coq on daily basis...

As you are looking for a formal verification, I would advise you to take a look at Coq. Even though mainly used by Academics, it provides a logical framework and an interface to write formal and interactive proofs.

Based this language there exists some libraries dedicated to cryptographic proof :

Example of proof :

Other formal tools (interactive provers) can be used such as Isabelle, Agda, Fstar and HOL. And some more readings :

As Mikeazo said, Cryptol might be an other possibility, but I can't say more on it.

I would also suggest you to have a look at the $\pi$-calculus which is mainly used to explore the verification of concurrent programs, but could be applied in the case of protocols.