(* Exercise 3: Showing Security Fails When One-time Pad is Used
Incorrectly *)
prover ["Z3"]. (* only use Z3 SMT solver *)
require import AllCore Distr StdOrder.
(* minimal axiomatization of bitstrings *)
op n : int. (* length of bitstrings *)
axiom ge1_n : 1 <= n.
type bits. (* type of bit strings of length n *)
op zero : bits. (* the all zero bitstring *)
op (^^) : bits -> bits -> bits. (* pointwise exclusive or *)
axiom xorC (x y : bits) :
x ^^ y = y ^^ x.
axiom xorA (x y z : bits) :
x ^^ y ^^ z = x ^^ (y ^^ z).
axiom xor0_ (x : bits) :
zero ^^ x = x.
lemma xor_0 (x : bits) :
x ^^ zero = x.
proof.
by rewrite xorC xor0_.
qed.
axiom xorK (x : bits) :
x ^^ x = zero.
lemma xor_double_same_right (x y : bits) :
x ^^ y ^^ y = x.
proof.
by rewrite xorA xorK xor_0.
qed.
lemma xor_double_same_left (x y : bits) :
y ^^ y ^^ x = x.
proof.
by rewrite xorK xor0_.
qed.
(* uniform, full and lossless distribution on bitstrings *)
op dbits : bits distr.
(* the following two axioms tell us that the size of
bits is exactly 2 ^ n *)
axiom dbits_ll : is_lossless dbits. (* is a distribution *)
(* every element x of bits has the same weight,
1%r / (2 ^ n)%r *)
axiom dbits1E (x : bits) :
mu1 dbits x = 1%r / (2 ^ n)%r.
(* so we can prove that dbits is full, i.e., every element
of the type has a non-zero weight *)
lemma dbits_fu : is_full dbits.
proof.
move => x.
rewrite /support dbits1E.
by rewrite RField.div1r StdOrder.RealOrder.invr_gt0
lt_fromint StdOrder.IntOrder.expr_gt0.
qed.
(* module type of Adversaries *)
module type ADV = {
(* ask Adversary to initialize itself *)
proc init() : unit
(* ask Adversary for message to securely communicate *)
proc get() : bits
(* let Adversary observe encrypted message being communicated *)
proc obs(x : bits) : unit
(* give Adversary decryption of received message *)
proc put(x : bits) : unit
(* ask Adversary for its boolean judgement - it is trying to
distinguish the real and ideal games *)
proc judge() : bool
}.
(* Real Game, Parameterized by Adversary *)
module GReal (Adv : ADV) = {
var pad : bits (* one-time pad *)
(* generate the one-time pad, sharing with both parties; we're
assuming Adversary observes nothing when this happens *)
proc gen() : unit = {
pad <$ dbits;
}
(* the receiving and sending parties are the same, as encrypting
and decrypting are the same *)
proc party(x : bits) : bits = {
return x ^^ pad;
}
proc main() : bool = {
var b : bool;
var x, y, z : bits;
Adv.init(); (* tell Adversary to initialize itself *)
gen(); (* generate and share to parties one-time pad *)
(* round 1 *)
x <@ Adv.get(); (* get message from Adversary, give to Party 1 *)
y <@ party(x); (* Party 1 encrypts x, yielding y *)
Adv.obs(y); (* y is observed in transit between parties
by Adversary *)
z <@ party(y); (* y is decrypted by Party 2, yielding z *)
Adv.put(z); (* z is given to Adversary by Party 2 *)
(* round 2 *)
x <@ Adv.get(); (* get message from Adversary, give to Party 2 *)
y <@ party(x); (* Party 2 encrypts x, yielding y *)
Adv.obs(y); (* y is observed in transit between parties
by Adversary *)
z <@ party(y); (* y is decrypted by Party 1, yielding z *)
Adv.put(z); (* z is given to Adversary by Party 1 *)
b <@ Adv.judge(); (* Adversary is asked for boolean judgement *)
return b; (* return boolean judgment as game's result *)
}
}.
(* module type of Simulators *)
module type SIM = {
(* choose gets no help to simulate encrypted message; we specify
below that choose can't read/write GReal.pad *)
proc choose() : bits
}.
(* Ideal Game, parameterized by both Simulator and Adversary *)
module GIdeal(Sim : SIM, Adv : ADV) = {
proc main() : bool = {
var b : bool;
var x, y : bits;
Adv.init(); (* tell Adversary to initialize itself *)
(* round 1 *)
x <@ Adv.get(); (* get message from Adversary *)
y <@ Sim.choose(); (* simulate message encryption *)
Adv.obs(y); (* transmission of encryption simulation is
observed by Adversary *)
Adv.put(x); (* x is given back to Adversary *)
(* round 2 *)
x <@ Adv.get(); (* get message from Adversary *)
y <@ Sim.choose(); (* simulate message encryption *)
Adv.obs(y); (* transmission of encryption simulation is
observed by Adversary *)
Adv.put(x); (* x is given back to Adversary *)
b <@ Adv.judge(); (* ask Adversary for its boolean judgement *)
return b; (* return Adversary's boolean judgment *)
}
}.
module Sim : SIM = {
proc choose() : bits = {
var x : bits;
x <$ dbits;
return x;
}
}.
(* In this exercise, you should define a concrete Adversary Adv : ADV,
and prove that for all memories &m,
`|Pr[GReal(Adv).main() @ &m : res] -
Pr[GIdeal(Sim, Adv).main() @ &m : res]|
is strictly greater than 0%r. Ideally, you should prove it
is close to 1%r. *)
(* BEGIN FILL IN *)
(* END FILL IN *)