Exploring EasyCrypt (2024-09-26)
This semester (Fall 2024), I am in a special topics class exploring the intersection of programming languages and cryptography. As part of this class I came across EasyCrypt. There are very little resources surrounding examples.
I am by no means an expert in EasyCrypt but this serves as a way of cataloguing my steps to learning it.
What even is EasyCrypt? Why does it exist?
EasyCrypt is a software developed for computer verified proofs. Typical paper proofs even when thoroughly reviewed can contain logical leaps and errors. Computer verified proofs allow users to create logically sound claims.
Cryptography proofs often involve games and reasoning about adversarial advantage in order to prove a desired security property. EasyCrypt provides a framework for creating these games and reasoning about adversarial-games through probabilistic computations.
Code Walkthrough
Let's get right into it and walk through this example! Note that this is an in-depth version of the example mentioned in chapter 2.5 of the EasyCrypt reference.
require import Bool DBool.
module G1 = {
proc f() : bool = {
var x : bool;
x <$ {0,1};
return x;
}
}.
module G2 = {
proc f() : bool = {
var x,y : bool;
x <$ {0,1};
y <$ {0,1};
return x ^^ y;
}
}.
The first line require import Bool DBool. imports the packages we will be using, in this case: booleans (Bool) and boolean distributions (DBool). At its core, EasyCrypt has build-in types for booleans, integers, reals,
and a unit (which can be thought of as an empty execution or ()). There are also some cryptographic primatives being
developed and reasoned about / verified available as an import.
Each type, both built-in and created, will automatically have an associated distribution type.
The follow lines establish module G1 and G2, with a procedure f which when called will either return true or false.
The line x <$ {0,1}; say to take with uniform probability from either 0 or 1 (false or true) and assign this to x.
G1.f will return this value, but G2.f will also get a value y in a similar fashion and return the exclusive or (xor, also denoted by ^^) of x and y.
The xor operation returns true if either x or y is true, but false if both or neither is true.
Both G1.f and G2.f should return 0 with 0.5 probability and 1 with 0.5 probaiblity. This is what we will be proving; That is tossing a coin once and recording whether it was H or T follows the same distribution as flipping a coin twice and seeing when
the results differ or are the same.
Helper Lemma
We will now prove our first proof, well lemma, that will be useful to us soon.
lemma xor_equiv (x y : bool) : y ^^ x ^^ x = y
That given two booleans, and if we xor by twice, it is equivalent to . The proof for this in EasyCrypt is as follows:
lemma xor_equiv (x y : bool) : y ^^ x ^^ x = y.
proof.
rewrite xorA.
rewrite xorK.
rewrite xor_false.
trivial.
qed.
We accomplish proving this lemma rewriting the goal with rewriting the goal through lemmas provided in the EasyCrypt bool
definition. The first, xorA, is the associative property of exclusive or which gives us the new goal of y ^^ (x ^^ x) = y.
We do this to allow the prover to utilize the next rewrite step, xorK, which
states that for any boolean , xor'd with itself is false. From here we have y ^^ false = y and can finish
through xor_false which states exactly this. From that line we are left with false = false and we state that it's trivially correct.
With that we've finished the only helper lemma we need for this proof.
Equivalent Distribution Proof
The first part is understanding how to represent the lemma for equating these two probabilities.
lemma G1_G2_f : equiv[G1.f ~ G2.f : true ==> ={res}].
In EasyCrypt this is approached as such. The above states that executing G1.f and G2.f with no preconditions to memory implies that the results of both will be the same.
The full proof looks like the following
lemma G1_G2_f : equiv[G1.f ~ G2.f : true ==> ={res}].
proof.
proc.
seq 0 1 : true.
rnd {2}.
skip.
trivial.
rnd (fun (z : bool) => z ^^ x{2}).
skip.
simplify.
move => &2.
split.
move => z _.
rewrite xor_equiv //.
move => &3 x _.
split.
rewrite xor_equiv //.
move => h.
rewrite xorC xor_equiv //.
qed.
The first step proc, says to break down the two programs to their code. Giving us a current goal of
Type variables: <none>
------------------------------------------------------------------------
&1 (left ) : {x : bool}
&2 (right) : {x, y : bool}
pre = true
x <$ {0,1} (1) x <$ {0,1}
(2) y <$ {0,1}
post = x{1} = x{2} ^^ y{2}
The next step, seq 0 1 : true, will split up the proof into two sections of length 0 and 1 respectively with a post
of true for the first goal and precondition of true with the original post for the second. Our new goal is then.
Current goal (remaining: 2)
Type variables: <none>
------------------------------------------------------------------------
&1 (left ) : {x : bool}
&2 (right) : {x, y : bool}
pre = true
(1) x <$ {0,1}
post = true
Note that there is now two goals to the proof (as we split it in two). This portion is trivial
since we have a pre- and post-condition of true. We do rnd{2} to introduce a for all statement for the possible values of x (where 2 refers to the second, right-side program).
This transforms our goal to the following.
pre = true
post = forall (x0 : bool), (x0 \in {0,1})%Distr => true
We skip to rewrite the condition to pre => post, which gives us true => true which is trivially true for
all values of x, and finish of the first goal with a trival.
We now need to finish the second goal:
Type variables: <none>
------------------------------------------------------------------------
&1 (left ) : {x : bool}
&2 (right) : {x, y : bool}
pre = true
x <$ {0,1} (1) y <$ {0,1}
post = x{1} = x{2} ^^ y{2}
Similar to above, our first step is to give random variables an assignment, to do this we
use rnd (fun (z : bool) => z ^^ x{2}) which gives a random assignment to the programs through this
isomorphic function between the two distributions (fun (z : bool) => z ^^ x{2}). The post condition
now has two steps to it, proving that it is an isomorphism and that the original post condition holds with the
assignments. Our current goal after the rnd is now
Type variables: <none>
------------------------------------------------------------------------
&1 (left ) : {x : bool}
&2 (right) : {x, y : bool}
pre = true
post =
(forall (yR : bool), (yR \in {0,1})%Distr => yR = yR ^^ x{2} ^^ x{2}) &&
forall (xL : bool),
(xL \in {0,1})%Distr =>
xL = xL ^^ x{2} ^^ x{2} && xL = x{2} ^^ (xL ^^ x{2})
We use skip as before to turn the pre- and post-condition into an implication. Afterwords
we use move as a way of moving the conditons of implications into our known state.
split is a way of splitting an and statement into two goals, allowing us to prove the and
statement by proving each sub goal. After the move => z _. we are in the state below:
Type variables: <none>
&2: {x, y : bool}
z: bool
------------------------------------------------------------------------
z = z ^^ x{2} ^^ x{2}
and can utilize our helper lemma by rewrite xor_equiv // which is shorthand for rewrite xor_equiv followed by trivial.
This solves our first sub-goal.
We use move again through move => &3 x _. to simplify
Type variables: <none>
&2: {x, y : bool}
------------------------------------------------------------------------
(forall (yR : bool), (yR \in {0,1})%Distr => yR = yR ^^ x{2} ^^ x{2}) =>
forall (xL : bool),
(xL \in {0,1})%Distr =>
xL = xL ^^ x{2} ^^ x{2} && xL = x{2} ^^ (xL ^^ x{2})
to
Type variables: <none>
&2: {x, y : bool}
&3: forall (yR : bool), (yR \in {0,1})%Distr => yR = yR ^^ x{2} ^^ x{2}
x: bool
------------------------------------------------------------------------
x = x ^^ x{2} ^^ x{2} && x = x{2} ^^ (x ^^ x{2})
From here we utilize split again, which for && will create two goals similar to
^ but differing in the second goal being an implication.
Thus the rest of our proof handles the rewriting and moving
rewrite xor_equiv //.
move => h.
rewrite xorC xor_equiv //.
and ultimately end with qed. I would recommend stepping through the proof through the
interactive proof mode in EasyCrypt.