9
$\begingroup$

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.

$\endgroup$
  • 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 Oct 21 '16 at 19:48
  • 2
    $\begingroup$ Probably the closest would be cryptol. $\endgroup$ – mikeazo Oct 21 '16 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 Oct 21 '16 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 Oct 22 '16 at 23:35
12
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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