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.
$\begingroup$
$\endgroup$
4
-
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$– SEJPMCommented Oct 21, 2016 at 19:48
-
2$\begingroup$ Probably the closest would be cryptol. $\endgroup$– mikeazoCommented 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$– LimitCommented Oct 22, 2016 at 23:35
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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 :
- Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols
- Formal certification of ElGamal encryption
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 :
- Computer Verification in Cryptography
- Probabilistic Relational Verification for Cryptographic Implementations
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:
- Introduction to Symbolic Verification Methods, David Basin, ETH Zurich
- Computer-aided cryptographic proofs, Gilles Barthe, IMDEA
- Human Errors in Security Protocols, David Basin, ETH Zurich
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).