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

module Adv : ADV = {
  var first : bool   (* in first round? *)
  var x1, x2 : bits

  proc init() : unit = {
    first <- true;
  }

  proc get() : bits = {
    return zero;
  }

  proc obs(x : bits) : unit = {
    if (first) {
      x1 <- x;
    }
    else {
      x2 <- x;
    }
  }

  proc put(x : bits) : unit = {
    if (first) {
      first <- false;  (* ready for second round *)
    }
  }

  proc judge() : bool = {
    return x1 = x2;
  }
}.

lemma GReal_Adv_pr &m :
  Pr[GReal(Adv).main() @ &m : res] = 1%r.
proof.
byphoare => //.
proc; inline*; auto; progress.
by rewrite dbits_ll.
qed.

op eps_n : real = 1%r / (2 ^ n)%r.

lemma GIdeal_Sim_Adv_pr &m :
  Pr[GIdeal(Sim, Adv).main() @ &m : res] = eps_n.
proof.
byphoare => //.
proc; inline*; wp.
rnd (pred1 Adv.x1).
wp.
rnd predT.
auto; progress.
by rewrite dbits_ll.
by rewrite dbits1E.
rewrite /pred1 in H4; by rewrite H4.
qed.

lemma gt1_two2n : 1 < 2 ^ n.
proof.
rewrite IntOrder.exprn_egt1 //.
by rewrite (lez_trans 1) // ge1_n.
rewrite IntOrder.ltr0_neq0 // ltzE /= ge1_n.
qed.

lemma gt1_two2n_real : 1%r < (2 ^ n)%r.
proof. rewrite lt_fromint gt1_two2n. qed.

lemma gt0_two2n_real : 0%r < (2 ^ n)%r.
proof.
rewrite (RealOrder.ltr_trans 1%r) // gt1_two2n_real.
qed.

lemma gt0_eps_n : 0%r < eps_n.
proof.
rewrite RealOrder.divr_gt0 // gt0_two2n_real.
qed.

lemma lt1_eps_n : eps_n < 1%r.
proof.
rewrite -RealOrder.ltr_pdivl_mulr 1:gt0_eps_n.
rewrite RealOrder.Domain.div1r RealOrder.Domain.invrK.
rewrite gt1_two2n_real.
qed.

lemma eps_n_mul_two2n_eq_1 : eps_n * (2 ^ n)%r = 1%r.
proof.
by rewrite -divrK 1:RealOrder.gtr_eqF 1:gt0_two2n_real.
qed.

lemma gt0_one_min_eps_n : 0%r < 1%r - eps_n.
proof.
rewrite -eps_n_mul_two2n_eq_1.
have {2}-> : eps_n = eps_n * 1%r by trivial.
rewrite -StdBigop.Bigreal.Num.Domain.mulrBr -fromintB.
rewrite RealOrder.pmulr_rgt0 1:gt0_eps_n.
rewrite lt_fromint IntOrder.ltr_subr_addr /= gt1_two2n.
qed.

lemma insecurity &m :
  `|Pr[GReal(Adv).main() @ &m : res] -
    Pr[GIdeal(Sim, Adv).main() @ &m : res]| =
  1%r - eps_n.
proof.
rewrite (GReal_Adv_pr &m) (GIdeal_Sim_Adv_pr &m).
rewrite -RealOrder.ler_def RealOrder.ltrW lt1_eps_n.
qed.

lemma insecurity_gt0 &m :
  0%r <
  `|Pr[GReal(Adv).main() @ &m : res] -
    Pr[GIdeal(Sim, Adv).main() @ &m : res]|.
proof.
rewrite (insecurity &m) gt0_one_min_eps_n.
qed.

(* END FILL IN *)