(* Secure Message Communication via a One-time Pad, Formalized
   in Ordinary (Non-UC) Real/Ideal Paradigm Style *)

prover [""].  (* no use of smt *)

require import AllCore Distr.

(* 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 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, and ask it for its
     boolean judgment (the adversary is trying to differentiate the
     real and ideal games) *)

  proc put(x : bits) : 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

     of course, it's not realistic that a one-time pad can be
     generated and shared with the adversary learning nothing *)

  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;

    x <@ Adv.get();    (* get message from Adversary, give to Party 1 *)
    gen();             (* generate and share to parties one-time pad *)
    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 *)
    b <@ Adv.put(z);   (* z is given to Adversary by Party 2, and
                          Adversary chooses boolean judgment *)
    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 Adv's global variables *)

  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;

    x <@ Adv.get();     (* get message from Adversary *)
    y <@ Sim.choose();  (* simulate message encryption *)
    Adv.obs(y);         (* transmission of encryption simulation is
                           observed by Adversary *)
    b <@ Adv.put(x);    (* x is given back to Adversary *)
    return b;           (* return Adversary's boolean judgment *)
  }    
}.

(* our goal is to prove the following security theorem, saying the
   Adversary (assuming it can't read/write GReal's global variables)
   is completely unable to distinguish the real and ideal games:

lemma Security (Adv <: ADV{-GReal}) &m :
  exists (Sim <: SIM{-Adv}),  (* there is a simulator that can't read/write
                                 Adv's global variables *)
  Pr[GReal(Adv).main() @ &m : res] =
  Pr[GIdeal(Sim, Adv).main() @ &m : res].
*)

(* enter section, so Adversary is in scope *)

section.

(* say Adv and GReal don't read/write each other's globals (GIdeal
   has no globals) *)

declare module Adv <: ADV{-GReal}.

(* define simulator as a local module, as security theorem won't
   depend upon it *)

local module Sim : SIM = {
  proc choose() : bits = {
    var x : bits;
    x <$ dbits;
    return x;
  }
}.

local lemma GReal_GIdeal :
  equiv[GReal(Adv).main ~ GIdeal(Sim, Adv).main :
        ={glob Adv} ==> ={res}].
proof.
proc.
inline*.
seq 1 1 : (={x, glob Adv}).
call (_ : true).  (* because Adv doesn't use oracle, invariant is "true" *)
auto.
seq 1 1 : (={x, glob Adv} /\ x{1} ^^ GReal.pad{1} = x0{2}).
rnd (fun z => x{1} ^^ z).
auto => /> &2.
split => [z _ | _].
by rewrite -xorA xor_double_same_left.
split => [z _ | _ z _].
by rewrite 2!dbits1E.
split => [| _].
apply dbits_fu.
by rewrite -xorA xor_double_same_left.
call (_ : true).  (* last statement of each program must be call *)
wp.
call (_ : true).
auto => />.
by rewrite xor_double_same_right.
qed.

lemma Sec &m :
  exists (Sim <: SIM{-Adv}),
  Pr[GReal(Adv).main() @ &m : res] =
  Pr[GIdeal(Sim, Adv).main() @ &m : res].
proof.
exists Sim.
by byequiv GReal_GIdeal.
qed.

end section.

(* security theorem *)

lemma Security (Adv <: ADV{-GReal}) &m :
  exists (Sim <: SIM{-Adv}),
  Pr[GReal(Adv).main() @ &m : res] =
  Pr[GIdeal(Sim, Adv).main() @ &m : res].
proof.
apply (Sec Adv &m).
qed.