equation forall x:bool; not(not(x)) = x.
equation forall x:bool,y:bool; (not(x && y)) = (not(x) || not(y)).
equation forall x:bool,y:bool; (not(x || y)) = (not(x) && not(y)).
equation not(true) = false.
equation not(false) = true.
equation forall x:bool; (x = true) = x.
equation forall x:bool; (x <> false) = x.
equation forall x:bool; (x <> true) = not(x).
equation forall x:bool; (x = false) = not(x).
equation forall x,y,z:bool; ((x || y) && z) = ((x && z) || (y && z)).
const bottom:bitstringbot.
(******************************** Diffie-Hellman ***************************)
(* DH_basic defines a part common for most Diffie-Hellman assumptions.
G: type of group elements (must be "bounded" or "nonuniform", and "large")
Z: type of exponents (must be "bounded" or "nonuniform", and "large")
g: generator
exp: the exponentiation function
exp': symbol that replaces exp after game transformation
mult: the multiplication function for exponents
The types G and Z must be declared before expanding
this macro. The functions g, exp, exp', and mult are defined by this
macro. They must not be declared elsewhere, and they can be used
only after expanding the macro.
*)
def DH_basic(G, Z, g, exp, exp', mult) {
fun exp(G,Z): G.
fun exp'(G,Z): G.
const g:G.
fun mult(Z,Z): Z.
equation builtin commut(mult).
(* exponents multiply *)
equation forall a:G, x:Z, y:Z;
exp(exp(a,x), y) = exp(a, mult(x,y)).
equation forall a:G, x:Z, y:Z;
exp'(exp'(a,x), y) = exp'(a, mult(x,y)).
}
(* DH_dist_random_group_element_vs_exponent says that the probability
of distinguishing a random group element from an exponentiation
exp(g,x) with a random exponent is at most PDist. The other
arguments are as in DH_basic and must all be defined before. *)
def DH_dist_random_group_element_vs_exponent(G, Z, g, exp, exp', mult, PDist) {
(* replace a random group element with an exponentiation, and conversely. *)
param N, N'.
equiv(group_to_exp_strict(exp))
foreach iX <= N do X <-R G; (OX() := return(X) | foreach iXm <= N' do OXm(m:Z) [useful_change] := return(exp(X,m)))
<=(N * PDist)=> [computational]
foreach iX <= N do x <-R Z; (OX() := return(exp(g,x)) | foreach iXm <= N' do OXm(m:Z) := return(exp(g,mult(x,m)))).
(* This equivalence is very general, apply it only manually, because
otherwise it might be applied too often. The equivalence above is
particular case applied only when X is inside exp, and good for
automatic proofs. *)
equiv(group_to_exp(exp))
foreach iX <= N do X <-R G; OX() := return(X)
<=(N * PDist)=> [manual, computational]
foreach iX <= N do x <-R Z; OX() := return(exp(g,x)).
equiv(exp_to_group(exp))
foreach iX <= N do x <-R Z; OX() := return(exp(g,x))
<=(N * PDist)=> [computational]
foreach iX <= N do X <-R G; OX() := return(X).
equiv(exp'_to_group(exp))
foreach iX <= N do x <-R Z; OX() := return(exp'(g,x))
<=(N * PDist)=> [computational]
foreach iX <= N do X <-R G; OX() := return(X).
}
(* DH_good_group defines Diffie-Hellman assumptions that hold
when
- G is a group of prime order q, with the neutral element excluded.
- the set of exponents Z is {1, ..., q-1}
- g is a generator of G
- mult is the product modulo q in {1, ..., q-1}, i.e. in the group (Z/qZ)*
Warnings:
* It may not be obvious when an element is received on the network
whether it really belongs to the group G generated by g. That should
be checked for the results to apply.
* Random choices of exponents must be made uniformly in {1, ..., q-1}
for the results to apply; random choices in G are also uniform.
The arguments are as in DH_basic.
*)
def DH_good_group(G, Z, g, exp, exp', mult) {
expand DH_basic(G, Z, g, exp, exp', mult).
(* Since the group has prime order,
exp(x,y) = exp(x',y) implies x = x', by raising both sides to y^{-1}.
Note that y is invertible since it belongs to (Z/qZ)* with q prime. *)
equation forall x:G, x':G, y:Z; (exp(x,y) = exp(x',y)) = (x = x').
equation forall x:G, x':G, y:Z; (exp'(x,y) = exp'(x',y)) = (x = x').
equation forall x:G, x':Z, y:Z; (exp(x,y) = exp(g, mult(x',y))) = (x = exp(g,x')).
equation forall x:G, x':Z, y:Z; (exp'(x,y) = exp'(g, mult(x',y))) = (x = exp(g,x')).
(* Injectivity: Since G has prime order, all its elements x are generators.
All elements x^y for y \in Z = { 1, ..., q-1 } are then distinct. *)
equation forall x:G, y:Z, y':Z; (exp(x,y) = exp(x,y')) = (y = y').
equation forall x:G, y:Z, y':Z; (exp'(x,y) = exp'(x,y')) = (y = y').
(* collision between products *)
(* The collision x.y = z happens when x = z/y
(y is invertible since we work in (Z/qZ)* with q prime).
Since z/y is independent of x, this has probability
1/|Z| to happen. *)
collision x <-R Z; forall y: Z, z: Z;
return(mult(x,y) = z) <=(1/|Z|)=> return(false) if y independent-of x && z independent-of x.
collision x <-R Z; y <-R Z; forall z: Z;
return(mult(x,y) = z) <=(1/|Z|)=> return(false) if z independent-of x || z independent-of y.
(* The next collision groups 2 cases:
- mult(x,y) = z with x, y independent of each other, seen above
- mult(x,x) = z. This case is justified as follows.
In (Z/qZ)*, half of the elements are square, and each square
has 2 square roots. If z is not a square, the equality x.x = z is false.
If z is a square z = x'.x', then x.x = x'.x' iff x = x' or x = -x' (mod q),
so with probability 2/|Z|. *)
collision x <-R Z; y <-R Z; [random_choices_may_be_equal] forall z: Z;
return(mult(x,y) = z) <=(2/|Z|)=> return(false) if z independent-of x || z independent-of y.
(* The next collision is a consequence of the previous one, though this requires
some reasoning.
The random choices x1,y1,x2,y2 may be either independent of each other or equal
(because the option "random_choices_may_be_equal" still makes sure that the
array indices of x1,y1,x2,y2 do not depend on x1,y1,x2,y2).
Hence x1 independent-of x2 actually implies that x2 is also independent of x1.
The condition (x1 independent-of x2 || y1 independent-of y2) &&
(x1 independent-of y2 || y1 independent-of x2)
yields 4 cases:
1/ x1 independent-of x2 and x1 independent-of y2
x2 and y2 independent of x1, so mult(x2,y2) independent of x1
Apply previous collision with z = mult(x2,y2)
2/ x1 independent-of x2 and y1 independent-of x2
x1 and y1 independent of x2, so mult(x1,y1) independent of x2
Apply previous collision with z = mult(x1,y1)
3/ y1 independent-of y2 and x1 independent-of y2
x1 and y1 independent of y2, so mult(x1,y1) independent of y2
Apply previous collision with z = mult(x1,y1)
4/ y1 independent-of y2 and y1 independent-of x2
x2 and y2 independent of y1, so mult(x2,y2) independent of y1
Apply previous collision with z = mult(x2,y2)
The formulation below allows CryptoVerif to replace
mult(x1,y1) = mult(x2,y2)
with a condition corresponding to
(x1 = x2 && y1 = y2) || (x1 = y2 && y1 = x2)
where = here means that they are the same random choice (i.e. same
variable with the same indices). This condition is the negation
of the independence condition
(x1 independent-of x2 || y1 independent-of y2) &&
(x1 independent-of y2 || y1 independent-of x2).
It corresponds to the only case that makes the equality
succeed with non-negligible probability. *)
collision x1 <-R Z; y1 <-R Z; x2 <-R Z; y2 <-R Z; [random_choices_may_be_equal]
return(mult(x1,y1) = mult(x2,y2)) <=(2/|Z|)=> return(false)
if (x1 independent-of x2 || y1 independent-of y2) &&
(x1 independent-of y2 || y1 independent-of x2).
(* x is invertible since we work in (Z/qZ)* with q prime *)
equation forall x:Z, y:Z, y':Z;
(mult(x,y) = mult(x,y')) = (y = y').
(* The following properties are true, but CryptoVerif should be able
to infer them from the equations above.
If Y independent of x, g^x = Y succeeds for one value of x,
so with probability 1/|Z|.
collision x <-R Z; forall Y: G;
return(exp(g, x) = Y) <=(1/|Z|)=> return(false) if Y independent-of x.
collision x <-R Z; forall Y: G;
return(exp'(g, x) = Y) <=(1/|Z|)=> return(false) if Y independent-of x.
If Y independent of y, g^(x.y) = Y succeeds for one value of y,
so with probability 1/|Z|.
collision x <-R Z; y <-R Z; forall Y: G;
return(exp(g, mult(x,y)) = Y) <=(1/|Z|)=> return(false) if Y independent-of y.
collision x <-R Z; y <-R Z; forall Y: G;
return(exp'(g, mult(x,y)) = Y) <=(1/|Z|)=> return(false) if Y independent-of y.
*)
(* X^x = Y
X is a generator of the group, so Y = X^y for some y
independent of x. The equality X^x = Y = X^y holds only when
x = y (mod q) with y independent of x,
so this has probability 1/|Z| of happening. *)
collision x <-R Z; forall X: G, Y: G;
return(exp(X, x) = Y) <=(1/|Z|)=> return(false)
if X independent-of x && Y independent-of x.
collision x <-R Z; forall X: G, Y: G;
return(exp'(X, x) = Y) <=(1/|Z|)=> return(false)
if X independent-of x && Y independent-of x.
(* replace a random group element with an exponentiation, and conversely.
This is valid because G is exactly the group generated by g of cardinal q,
and Z = {1, ..., q-1} so when x varies in Z, exp(g,x) covers each element
of G exactly once. *)
letproba PDist = 0.
expand DH_dist_random_group_element_vs_exponent(G, Z, g, exp, exp', mult, PDist).
}
(* Variant of CDH with random self reducibility.
It may yield lower probabilities but requires the rerandomization to be feasible.
pCDH(t): the probability of breaking the CDH assumption in time t
pDistRerandom: the probability that rerandomization can be distinguished from the
original distribution
It is 0 when exponents are chosen uniformly in (Z/qZ)^*.
2^-126 for curve25519
2^-221 for curve448
(see https://tools.ietf.org/html/draft-barnes-cfrg-mult-for-7748-00 for the rerandomization
for curve25519 and curve448).
Other arguments as in DH_basic.
All arguments must be declared before this macro. *)
def CDH_RSR(G, Z, g, exp, exp', mult, pCDH, pDistRerandom) {
(* the CDH assumption *)
param na, naDDH, nb, nbDDH, naDH9, nbDH9.
equiv(cdh(exp))
foreach ia <= na do a <-R Z; (
OA() := return(exp(g,a)) |
Oa() [10] := return(a) |
foreach iaDDH <= naDDH do ODDHa(m:G, j<=nb) [useful_change] := return(m = exp(g, mult(b[j], a))) |
foreach iaDH9 <= naDH9 do ODHa9(x:Z) [2] := return(exp(g, mult(a, x)))
) |
foreach ib <= nb do b <-R Z; (
OB() := return(exp(g,b)) |
Ob() [10] := return(b) |
foreach ibDDH <= nbDDH do ODDHb(m:G, j<=na) := return(m = exp(g, mult(a[j], b))) |
foreach ibDH9 <= nbDH9 do ODHb9(x:Z) [2] := return(exp(g, mult(b, x)))
)
<=((#ODDHa + #ODDHb) * (3*#Oa+1) * (3*#Ob+1) * pCDH(time + (na + nb + (optim-if #Oa = 0 && #Ob = 0 then 0 else #ODDHa + #ODDHb) + 1 + #ODHa9 + #ODHb9) * time(exp)) + (na + nb) * pDistRerandom)=> [computational]
foreach ia <= na do a <-R Z [unchanged]; (
OA() := return(exp'(g,a)) |
Oa() := let ka:bool = true in return(a) |
foreach iaDDH <= naDDH do ODDHa(m:G, j<=nb) :=
if defined(kb[j]) then return(m = exp'(g, mult(b[j], a))) else
if defined(ka) then return(m = exp'(g, mult(b[j], a))) else return(false) |
foreach iaDH9 <= naDH9 do ODHa9(x:Z) := return(exp'(g, mult(a, x)))
) |
foreach ib <= nb do b <-R Z [unchanged]; (
OB() := return(exp'(g,b)) |
Ob() := let kb:bool = true in return(b) |
foreach ibDDH <= nbDDH do ODDHb(m:G, j<=na) :=
if defined(ka[j]) then return(m = exp'(g, mult(a[j], b))) else
if defined(kb) then return(m = exp'(g, mult(a[j], b))) else return(false) |
foreach ibDH9 <= nbDH9 do ODHb9(x:Z) := return(exp'(g, mult(b, x)))
).
}
(* Ideal Cipher Model
cipherkey: type of keys that correspond to the choice of the scheme, must be "bounded" or "nonuniform", typically "fixed".
key: type of keys (typically "large")
blocksize: type of the input and output of the cipher, must be "bounded" or "nonuniform" (to be able to generate random numbers from it; typically "fixed") and "large".
(The modeling of the ideal cipher model is not perfect in that, in
order to encrypt a new message, one chooses a fresh random number,
not necessarily different from previously generated random
numbers. Then CryptoVerif needs to eliminate collisions between
those random numbers, so blocksize must really be "large".)
enc: encryption function
dec: decryption function
WARNING: the encryption and decryption functions take 2 keys as
input: the key of type cipherkey that corresponds to the choice of
the scheme, and the normal encryption/decryption key. The cipherkey
must be chosen once and for all at the beginning of the game and
the encryption and decryption oracles must be made available to the
adversary, by including a process enc_dec_oracle(ck) where
ck is the cipherkey.
qE is the number of calls of the encryption oracle
qD is the number of calls of the decryption oracle
The types cipherkey, key, blocksize must be declared before this
macro is expanded. The functions enc, dec, the process
enc_dec_oracle, and the parameters qE, qD are declared by this
macro. They must not be declared elsewhere, and they can be used
only after expanding the macro.
*)
def ICM_cipher(cipherkey, key, blocksize, enc, dec, enc_dec_oracle, qE, qD) {
fun enc(cipherkey, blocksize, key): blocksize.
fun dec(cipherkey, blocksize, key): blocksize.
equation forall ck:cipherkey, m:blocksize, k:key;
dec(ck, enc(ck, m, k), k) = m.
equation forall ck:cipherkey, m:blocksize, k:key;
enc(ck, dec(ck, m, k), k) = m.
equation forall ck:cipherkey, m1:blocksize, m2:blocksize, k:key;
(dec(ck, m1, k) = dec(ck, m2, k)) = (m1 = m2).
equation forall ck:cipherkey, m1:blocksize, m2:blocksize, k:key;
(enc(ck, m1, k) = enc(ck, m2, k)) = (m1 = m2).
equiv(icm(enc)) special icm(("key", "msg", "local_key"), enc, dec,
(ck, k, me, md, u), ("large")).
equiv(icm_partial(enc)) special icm_partial(("key", "msg", "local_key"),
enc, dec, (ck, k, me, md, u), ("large")) [manual].
(* The difference of probability is the probability of collision between two
random numbers in blocksize among the N+N2 chosen random numbers. *)
param qE, qD [noninteractive].
let enc_dec_oracle(ck: cipherkey) =
(foreach iE <= qE do Oenc(x:blocksize, ke:key) := return(enc(ck,x,ke)))
| (foreach iD <= qD do Odec(m:blocksize, kd:key) := return(dec(ck,m,kd))).
}
(******************************* Hash functions (ROM) ****************************)
(* Hash function in the random oracle model
key: type of the key of the hash function, which models the choice of the hash function, must be "bounded", typically "fixed"
input%: type of the %-th input of the hash function
output: type of the output of the hash function, must be "bounded" or "nonuniform" (typically "fixed").
f: the hash function.
WARNING: f is a keyed hash function.
The key must be generated once and for all at the beginning of the game
and the hash oracle must be made available to the adversary,
by including the process f_oracle(k) where k is the key.
qH is the number of calls to f_oracle.
The types key, input%, and output must be declared before
this macro. The function f, the process f_oracle, and
the parameter qH are defined by this macro. They must not
be declared elsewhere, and they can be used only after expanding the
macro.
*)
def ROM_hash(key, input1, output, f, f_oracle, qH) {
fun f(key, input1):output.
equiv(rom(f)) special rom("key_first", f, (hk, r, x, y, z, u)).
equiv(rom_partial(f)) special rom_partial("key_first", f, (hk, r, x, y, z, u)) [manual].
param qH [noninteractive].
let f_oracle(k: key) =
foreach iH <= qH do
OH(x1: input1) :=
return(f(k, x1)).
}
(* ROM with large output.
The only difference with ROM is that we eliminate collisions on the output.
The interface is the same as for ROMs. *)
def ROM_hash_large(key, input1, output, f, f_oracle, qH) {
fun f(key, input1):output.
equiv(rom(f)) special rom("key_first", f, (hk, r, x, y, z, u), ("large")).
equiv(rom_partial(f)) special rom_partial("key_first", f, (hk, r, x, y, z, u), ("large")) [manual].
param qH [noninteractive].
let f_oracle(k: key) =
foreach iH <= qH do
OH(x1: input1) :=
return(f(k, x1)).
}