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.

  • 1
    $\begingroup$ 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). $\endgroup$
    – SEJPM
    Commented Oct 21, 2016 at 19:48
  • 2
    $\begingroup$ Probably the closest would be cryptol. $\endgroup$
    – mikeazo
    Commented Oct 21, 2016 at 19:56
  • 1
    $\begingroup$ 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. $\endgroup$
    – Maarten Bodewes
    Commented Oct 21, 2016 at 20:40
  • $\begingroup$ @mikeazo and others, is there a reason why there is no formal language or is it just not needed? $\endgroup$
    – Limit
    Commented Oct 22, 2016 at 23:35

1 Answer 1


Disclaimer: I use Coq on daily basis...

About the tools

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 :

PHD : Formal certification of game-based cryptographic proofs

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.

About the formalizations

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.

Because most of those proofs are game based, one of the notion applied in this case is probabilistic couplings.

Some interesting readings:

Given the nature of your project, I would strongly recommend you to have a look at the works of David Basin as they have a software that seems to do what you intend to work on (from what I recall).


Your Answer

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

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