31
$\begingroup$

I have seen in some places that people use formal verification and/or computer-aided verification for cryptography (tools like ProVerif, CryptoVerif, etc.).

How do these approaches work?

Improve this question
$\endgroup$
1
  • 2
    $\begingroup$ Don't forget about Cryptol and SAW! Automatic formal verification of high assurance crypto formal specifications and implementations in C, LLVM, and JVM at your fingertips. And BSD licensed, no less! $\endgroup$
    – user33849
    Apr 28, 2016 at 16:47

2 Answers 2

Reset to default
39
$\begingroup$

Disclaimer: I use Coq on daily basis...

I have seen in some places that people use formal verification and/or computer-aided verification for cryptography.

To my knowledge, there aren't that many places that do such a thing.

First, let's define our concepts:

Formal Verification: The act of proving the correctness of algorithms with respect to a certain formal specification or property, using formal methods of mathematics.

Computer-assisted proof: A proof that has been at least partially generated by computer.

Some examples (in cryptography):

And some reading:

How does it work?

In formal methods (whatever the domain) there are two approaches:

  1. Specification $\rightarrow$ Software
  2. Specification $\wedge$ Software $\rightarrow$ Prove the software's correctness.

In most cases, the first method is the one used. Why? Because it is easier to start with a formal specification and then, incrementally, through proven steps, eventually get to the software (which is therefore proven). As an example, this certified compiler: enter image description here

For example in the Method B, the process is the following: $$DEFINE\ /\ SPECIFY \rightarrow PROVE \rightarrow REFINE \rightarrow PROVE \rightarrow \ldots \rightarrow IMPLEMENT$$

Formal verification uses the Hoare logic, a set of rules that allows us to reason about programs. It is based on sequent calculus and natural deduction. It relies on the Hoare triple: $$\{P\}\ C\ \{Q\}$$ When the precondition $\{P\}$ is met, the execution of the command $C$ establish the postcondition $\{Q\}$. If the command $C$ goes from a state $s$ to a state $s'$. $$C: s \rightarrow s'$$ Then you will have to prove: $$\forall\ s\ s', P[s] \implies C : s \rightarrow s' \implies Q[s']$$ But we prefer the Hoare triple notation (lighter).

As an example, this is the rule for $SKIP$ (aka do nothing): $$\frac{}{\{P\}\ SKIP\ \{P\}}$$

And this is the rule for the sequence : $$\frac{\{P\}\ C_1\ \{Q\}\ \ \ \ \ \ \ \{Q\}\ C_2\ \{R\}}{\{P\}\ C_1 ; C_2\ \{R\}}$$ This notation is read as : "If $\{P\}\ C_1\ \{Q\}$ (is $\text{True}$) and if $\{Q\}\ C_2\ \{R\}$, I can infer $\{P\}\ C_1 ; C_2\ \{R\}$.

A proof is therefore built from bottom to top : if you want to prove $\{P\}\ C_1 ; C_2\ \{R\}$, you will need to prove there is $Q$ such as $\{P\}\ C_1\ \{Q\}$ and $\{Q\}\ C_2\ \{R\}$.

Some readings on Hoare logic:

The tools

In formal methods, there are two kinds of tools:

  • the fully-automated prover
  • the proof assistants

The first are mainly based on SMT (satisfiability modulo theories) such as Atelier B and Alt-Ergo.

The second ones are based on pure logic. You provide it with lemmas (helping theorems), and this will make sure that every step you do in your proof is right. It is a very thorough process, quite slow. But at the end you know how your proof works and that it is correct because you did not miss a hypothesis. The process, which can be frustrating, will make sure that the proof works. The main proof assistants are the following: Coq, Isabelle, Agda, Fstar and HOL.

The tools you mentioned (ProVerif, CryptoVerif) are not dedicated to cryptographic primitives, but protocol verification. I do not know them, so I will not comment. Other tools on the same subject do exist. For example:

And yes, they are based on Coq.

In C, in order to be able to verify your code matches your specification (such as what has been done for $\text{SHA-}256$), one need to extract the semantic from the code. This could be done using the Verifiable Tool Chain or Why3. The first one will provide you a Coq file from which you will be able to start your proofs. The second one, given C ASCL instrumented code, will use frama-c and try to prove the properties with the SMT provers named above. On failure, it generates goals and asks you to prove them with Coq.

In Cryptography (and Mathematics)

I already mentioned the idea of proving protocols (cf EasyCrypt et al.), for cryptographic proofs, the idea is basically the same. Specify using logic properties.

Coq example (trivial to prove by hand for a undergrad student): $$\forall\ f g, f \text{ is injective} \implies g \text{ is injective} \implies g \circ f \text{ is injective}$$

Require Import Coq.Sets.Image.

Theorem injective_trans:
forall A B C (f: A -> B) (g:B -> C) (h:A -> C),
(forall x, h x = g (f x)) -> injective A B f -> injective B C g -> injective A C h.
Proof.
intros A B C f g h H_h_equal_g_f H_f_injective H_g_injective.
unfold injective in *.
intros x y H_h_x_y.
apply H_f_injective.
apply H_g_injective.
rewrite <- H_h_equal_g_f.
rewrite <- H_h_equal_g_f.
apply H_h_x_y.
Qed.

Here is a list of famous proven theorem in Coq.

Final words

Security bounds in Keccak has been proven with the aid of a computer. But their process was different: they exhaustively generated the trails and showed the properties. Thus it was computer aided, but not verified.

And finally, a recent paper from FSE 2016: Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC

As SEJPM pointed out, this paper is also another kind of approach (more game based). They created an analyzer that generated a cipher scheme that satisfied the AE scheme. However, I don't know whether they have proven their properties by hand or used a proof assistant (which might be possible given that they used Ocaml to code their analyzer).

You might also be interested in the course Gilles Barthe (EasyCrypt team) has done here.

I do not know if my answer has been helpful. I know it is not mainly focused on cryptography, but I hope it will give you a some idea of how things work.

Improve this answer
$\endgroup$
9
  • 1
    $\begingroup$ I'm not sure if you saw this paper (PDF), but it's related to this answer (I hope). $\endgroup$
    – SEJPM
    Apr 7, 2016 at 15:15
  • 1
    $\begingroup$ Another interesting source is the recent series of real-world attacks on the TLS protocols (see prosecco.gforge.inria.fr), in which formal methods apparently played a significant part. $\endgroup$
    – morten
    Apr 28, 2016 at 9:38
  • 1
    $\begingroup$ A great thorough answer nicely done! $\endgroup$
    – Mr. Stone
    Apr 28, 2016 at 20:11
  • 1
    $\begingroup$ Maybe worth noting that there has been a push towards more formal proofs for cryptographic primitives in recent years. It will raise the bar for the whole field. $\endgroup$
    – Yorick de Wid
    Mar 4, 2020 at 14:04
  • 1
    $\begingroup$ @YorickdeWid I know, I'm trying to get a paper at USENIX in that field. :) $\endgroup$
    – Biv
    Apr 15, 2020 at 14:36
4
$\begingroup$

Formal verification is used to verify the security services of your algorithm or your protocol. It uses specific high level modeling specification to specify your security solution and uses a back end formal verification tools to see whether or not there are security breaches or not. The outcome of the formal verification will tell you if your protocol is safe or unsafe. I suggest you to have a look at AVISPA which is one of the most common used to verify security properties of internet protocol

Improve this answer
$\endgroup$

Your Answer

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