(* 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 *)