(* prg.ec *)

(* security of one-time pad encryption built out of a pseudorandom
   generator (PRG) *)

prover ["Z3"].

require import AllCore Distr.

require BitWord. (* bit strings *)

(* long_len and short_len are strictly positive integers

   gt0_long_len is the lemma saying 0 < long_len
   gt0_short_len is the lemma saying 0 < short_len *)

op long_len : {int | 0 < long_len} as gt0_long_len.
op short_len : {int | 0 < short_len} as gt0_short_len.

(* their relationship *)

axiom le_long_short : short_len <= long_len.

(* long texts: bitstrings of length long_len *)

(* clone (make a copy of) Bitword, setting the length n of bitstrings
   to long_len, and calling the cloned theory Long *)

clone BitWord as Long with
  op n <- long_len
proof gt0_n.
realize gt0_n.

qed.

type long = Long.word.  (* abbreviations *)

op long0 : long = Long.zerow.  (* all 0 long *)

op (+^) : long -> long -> long = Long.(+^).  (* bitwise exclusive or *)

lemma long_xorK (x : long) : x +^ x = long0.
proof. apply Long.xorwK. qed.

lemma long_xorA (x y z : long) : x +^ (y +^ z) = x +^ y +^ z.
proof. apply Long.xorwA. qed.

lemma long_xorC (x y : long) : x +^ y = y +^ x.
proof. apply Long.xorwC. qed.

lemma long_xor_rid (x : long) : x +^ long0 = x.
proof. apply Long.xorw0. qed.

lemma long_xor_lid (x : long) : long0 +^ x = x.
proof. by rewrite Long.xorwC long_xor_rid. qed.

(* full/uniform/lossless distribution *)

op dlong : long distr = Long.DWord.dunifin.

(* all long element are in support *)
lemma dlong_fu : is_full dlong.
proof. apply Long.DWord.dunifin_fu. qed.

(* all elements of support have uniform probabilities *)
lemma dlong_uni : is_uniform dlong.
proof. apply Long.DWord.dunifin_uni. qed.

(* dlong is a distribution - i.e., sum of probabilities is 1 *)
lemma dlong_ll : is_lossless dlong.
proof. apply Long.DWord.dunifin_ll. qed.

(* probability of any given x being chosen *)
lemma mu1_dlong (x : long) : mu1 dlong x = 1%r / (2 ^ long_len)%r.
proof. by rewrite Long.DWord.dunifin1E Long.word_card. qed.

(* short texts: bitstrings of length short_len *)

clone BitWord as Short with
  op n <- short_len
proof gt0_n by apply gt0_short_len.

type short = Short.word.

op short0 : short = Short.zerow.  (* all 0 short *)

(* full/uniform/lossless distribution *)

op dshort : short distr = Short.DWord.dunifin.

lemma dshort_fu : is_full dshort.
proof. apply Short.DWord.dunifin_fu. qed.

lemma dshort_uni : is_uniform dshort.
proof. apply Short.DWord.dunifin_uni. qed.

lemma dshort_ll : is_lossless dshort.
proof. apply Short.DWord.dunifin_ll. qed.

lemma mu1_dshort (x : short) : mu1 dshort x = 1%r / (2 ^ short_len)%r.
proof. by rewrite Short.DWord.dunifin1E Short.word_card. qed.

(* pseudorandom generator *)

op PRG : short -> long.

(* Random Generators *)

module type RG = {
  proc f() : long
}.

(* Random Generator based on PRG *)

module PRG : RG = {
  proc f() : long = {
    var sh : short;
    sh <$ dshort;
    return PRG sh;
  }
}.

(* Random Generator based on true randomness *)

module TRG : RG = {
  proc f() : long = {
    var lng : long;
    lng <$ dlong;
    return lng;
  }
}.

(* Random Generator Adversary *)

module type RG_ADV (RG : RG) = {
  proc * main() : bool
}.

(* Random Generator Game *)

module G_RG (RG : RG, RG_Adv : RG_ADV) = {
  module A = RG_Adv(RG)

  proc main() : bool = {
    var b : bool;
    b <@ A.main();
    return b;
  }
}.

(* Under some circumstances

  `|Pr[G_RG(PRG, RG_Adv).main() @ &m : res] -
    Pr[G_RG(TRG, RG_Adv).main() @ &m : res]|

   will be negligible. This will depend on:

  (+) whether operator PRG is "good";

  (+) how much bigger long_len is than short_len;

  (+) how much computation RG_Adv is allowed to do *)

(* One-time Pad Encryption

   What's unrealistic about the following is how the sender and
   receiver can share the one-time-pads. But we'll ignore this
   issue. *)

module type ENC = {
  proc enc(x : long) : long
}.

(* Build One-time Pad Encryption out of Random Generator RG *)

module Enc(RG : RG) : ENC = {
  proc enc(x : long) : long = {
    var y : long;
    y <@ RG.f();
    return x +^ y;
  }
}.

(* Adversary *)

module type ADV (E : ENC) = {
  proc * main() : bool
}.

(* Encryption Game *)

module G_Enc (E : ENC, Adv : ADV) = {
  module A = Adv(E)

  proc main() : bool = {
    var b : bool;
    b <@ A.main();
    return b;
  }
}.

(* Encryption Ignoring Plaintext

   When G_Enc(EncIndep, Adv).main() runs, each time Adv calls
   EncIndep.f with a plaintext x, it gets back a random result y that
   has no relation to x *)

module EncIndep : ENC = {
  proc enc(x : long) : long = {
    var y : long;
    y <$ dlong;
    return y;
  }
}.

(* Our goal is to show an upper bound on the ability of an encryption
   adversary Adv to tell Enc(PRG) from EncIndep:

  lemma enc_security (Adv <: ADV) &m :
    `|Pr[G_Enc(Enc(PRG), Adv).main() @ &m : res] -
      Pr[G_Enc(EncIndep, Adv).main() @ &m : res]| <= ...Adv...
*)

(* convert an Encryption Adversary Adv into a Random Generator
   Adversary *)

module Adv_To_RG_Adv (Adv : ADV, RG : RG) = {

}.

(* in a section, we can declare an Adv : ADV, which lemmas (or
   local modules) can use;

   once we exit the section, (Adv <: Adv) will be added to any
   non-local lemmas *)

section.

declare module Adv : ADV.

local lemma TRG_Indep_eq &m :
  Pr[G_Enc(Enc(TRG), Adv).main() @ &m : res] =
  Pr[G_Enc(EncIndep, Adv).main() @ &m : res].
proof.

qed.

(* in the following, we say RG (e.g., PRF or TRG) and Adv can't
   interfere with each other's states *)

local lemma RG_eq (RG <: RG{Adv}) &m :
  Pr[G_Enc(Enc(RG), Adv).main() @ &m : res] =
  Pr[G_RG(RG, Adv_To_RG_Adv(Adv)).main() @ &m : res].
proof.

qed.

lemma sec &m :
  `|Pr[G_Enc(Enc(PRG), Adv).main() @ &m : res] -
    Pr[G_Enc(EncIndep, Adv).main() @ &m : res]| =
  `|Pr[G_RG(PRG, Adv_To_RG_Adv(Adv)).main() @ &m : res] -
    Pr[G_RG(TRG, Adv_To_RG_Adv(Adv)).main() @ &m : res]|.
proof.

qed.

end section.

(* try:

   print sec.
*)

(* if Adv is efficient, then so is Adv_To_RG_Adv *)

lemma enc_security (Adv <: ADV) &m :
  `|Pr[G_Enc(Enc(PRG), Adv).main() @ &m : res] -
    Pr[G_Enc(EncIndep, Adv).main() @ &m : res]| =
  `|Pr[G_RG(PRG, Adv_To_RG_Adv(Adv)).main() @ &m : res] -
    Pr[G_RG(TRG, Adv_To_RG_Adv(Adv)).main() @ &m : res]|.
proof.

qed.