SecretGuessing.eca

(* SecretGuessing.eca *)

(* Secret Guessing Game *)

(* This abstract theory provides a guessing game, in which the
   adversary gets a limited number of attempts to guess a secret. *)

prover quorum=2 ["Alt-Ergo" "Z3"].  (* both Alt-Ergo and Z3 must succeed *)

(***************************** Standard Theories ******************************)

require import AllCore FSet Distr Mu_mem.
require import StdOrder. import RealOrder.

(***************************** Theory Parameters ******************************)

(* a secret is a bitstring of length sec_len *)

op sec_len : int.  (* length of a secret *)

axiom sec_len_ge0 : 0 <= sec_len.

type sec.  (* type of secrets *)

op sec_default : sec.  (* default secret *)

op sec_distr : sec distr.  (* uniform, full and lossless distribution on
                              secrets *)

axiom mu1_sec_distr (sec : sec) :
  mu1 sec_distr sec = 1%r / (2 ^ sec_len)%r.

axiom sec_distr_ll : is_lossless sec_distr.

(* guessing limit *)

op limit : int.

axiom limit_ge0 : 0 <= limit.

(************************** End of Theory Parameters **************************)

(* guessing oracle type *)

module type SG_OR = {
  proc init(x : sec) : unit   (* initialize oracle, including secret *)
  proc guess(x : sec) : unit  (* try to guess secret *)
}.

(* guessing oracle *)

module SGOr : SG_OR = {
  var secret : sec    (* secret *)
  var ctr : int       (* counter *)
  var guessed : bool  (* true iff secret already guessed *)

  proc init(sec : sec) : unit = {
    secret <- sec;
    ctr <- 0;
    guessed <- false;
  }

  (* only the first limit calls to guess are taken into account *)

  proc guess(x : sec) : unit = {
    if (ctr < limit) {  (* invariant: ctr <= limit *)
      ctr <- ctr + 1;
      if (x = secret) {
        guessed <- true;
      }
    }
  }
}.

(* adversary type *)

module type SG_ADV(O : SG_OR) = {
  proc main() : unit {O.guess}
}.

(* guessing game *)

module Guessing(SGAdv : SG_ADV) = {
  module A = SGAdv(SGOr)

  proc main() : unit = {
    var sec : sec;
    sec <$ sec_distr;  (* randomly choose secret *)
    SGOr.init(sec);    (* initialize oracle *)
    A.main();          (* let adversary try to guess secret *)
  }
}.

(* see end of section for main lemma, GuessingProb *)

(******************************** Body of Proof *******************************)

(* the probability of a randomly chosen secret being in a set of
   secrets with cardinality n is n%r / (2 ^ sec_len)%r *)

lemma mu_sec_distr_mem (xs : sec fset) :
  mu sec_distr (mem xs) = (card xs)%r / (2 ^ sec_len)%r.
proof.
apply (mu_mem _ _ (1%r / (2 ^ sec_len)%r)) => x mem_xs_x.
apply mu1_sec_distr.
qed.

(* version of above where cardinality of set is upper bounded
   by limit *)

lemma mu_sec_distr_mem_limit (xs : sec fset) :
  card xs <= limit =>
  mu sec_distr (mem xs) <= limit%r / (2 ^ sec_len)%r.
proof.
move => lim.
rewrite mu_sec_distr_mem ler_wpmul2r 1:invr_ge0 le_fromint //.
case (sec_len = 0) => [-> | ne0_sec_len];
  [by rewrite expr0 lez01 | by rewrite IntOrder.expr_ge0].
qed.

section.

declare module SGAdv <: SG_ADV{-SGOr}.

(* version of oracle that simply accumulates guesses *)

local module SGOrAccum : SG_OR = {
  var secret : sec
  var ctr : int
  var guesses : sec fset  (* guesses made so far *)

  proc init(sec : sec) : unit = {
    secret <- sec;
    ctr <- 0;
    guesses <- fset0;
  }

  proc guess(x : sec) : unit = {
    if (ctr < limit) {
      ctr <- ctr + 1;
      guesses <- guesses `|` fset1 x;
    }
  }
}.

local lemma SGOrAccum_guess_Card :
  hoare
  [SGOrAccum.guess :
   SGOrAccum.ctr <= limit /\
   card SGOrAccum.guesses <= SGOrAccum.ctr ==>
   SGOrAccum.ctr <= limit /\
   card SGOrAccum.guesses <= SGOrAccum.ctr].
proof.
proc; auto; progress.
smt().
rewrite fcardU fcard1; smt(fcard_ge0).
qed.

local lemma SGOr_SGOrAccum_guess :
  equiv
  [SGOr.guess ~ SGOrAccum.guess :
   ={x} /\ ={secret, ctr}(SGOr, SGOrAccum) /\
   (SGOr.guessed{1} <=> mem SGOrAccum.guesses{2} SGOrAccum.secret{2}) ==>
   ={secret, ctr}(SGOr, SGOrAccum) /\
   (SGOr.guessed{1} <=> mem SGOrAccum.guesses{2} SGOrAccum.secret{2})].
proof.
proc; if; auto; progress.
by rewrite in_fsetU1.
rewrite in_fsetU; by left.
smt(in_fsetU1).
qed.

(* G1 is like Guessing, except it uses SGOrAccum not SGOr, and it has
   a global variable, guessed, whose value it calculates using
   SGOrAccum.guesses *)

local module G1 = {
  var guessed : bool

  module A = SGAdv(SGOrAccum)

  proc main() : unit = {
    var sec : sec;
    sec <$ sec_distr;
    SGOrAccum.init(sec);
    A.main();
    guessed <- mem SGOrAccum.guesses sec;
  }
}.

local lemma Guessing_G1_main :
  equiv
  [Guessing(SGAdv).main ~ G1.main :
   ={glob SGAdv} ==>
   ={secret, ctr}(SGOr, SGOrAccum) /\
   (SGOr.guessed{1} <=> G1.guessed{2})].
proof.
proc.
seq 2 2 :
  (={glob SGAdv, sec} /\ sec{1} = SGOr.secret{1} /\ ={secret, ctr}(SGOr, SGOrAccum) /\
   (SGOr.guessed{1} <=> mem SGOrAccum.guesses{2} SGOrAccum.secret{2})).
inline *; auto; progress; by rewrite in_fset0.
wp.
call
  (_ :
   ={glob SGAdv} /\ ={secret, ctr}(SGOr, SGOrAccum) /\
   (SGOr.guessed{1} <=> mem SGOrAccum.guesses{2} SGOrAccum.secret{2}) ==>
   ={res} /\ ={secret, ctr}(SGOr, SGOrAccum) /\
   (SGOr.guessed{1} <=> mem SGOrAccum.guesses{2} SGOrAccum.secret{2})).
proc
  (={secret, ctr}(SGOr, SGOrAccum) /\
   (SGOr.guessed{1} <=> mem SGOrAccum.guesses{2} SGOrAccum.secret{2})) => //.
conseq SGOr_SGOrAccum_guess => //.
auto.
qed.

local lemma Guessing_G1 &m :
  Pr[Guessing(SGAdv).main() @ &m : SGOr.guessed] =
  Pr[G1.main() @ &m : G1.guessed].
proof. by byequiv Guessing_G1_main. qed.

(* in G2, we don't tell SGOrAccum about the chosen secret, and
   secret is chosen just before membership test *)

local module G2 = {
  var guessed : bool

  module A = SGAdv(SGOrAccum)

  proc main() : unit = {
    var sec : sec;
    SGOrAccum.init(sec_default);
    A.main();
    sec <$ sec_distr;
    guessed <- mem SGOrAccum.guesses sec;
  }
}.

local lemma G1_G2_main :
  equiv[G1.main ~ G2.main : ={glob SGAdv} ==> ={guessed}(G1, G2)].
proof.
proc.
swap {2} 3 -2.
seq 2 2 : (={glob SGAdv, sec, SGOrAccum.ctr, SGOrAccum.guesses}).
inline *; auto.
sim.
qed.

local lemma G1_G2 &m :
  Pr[G1.main() @ &m : G1.guessed] = Pr[G2.main() @ &m : G2.guessed].
proof. by byequiv G1_G2_main. qed.

local lemma Guessing_G2 &m :
  Pr[Guessing(SGAdv).main() @ &m : SGOr.guessed] =
  Pr[G2.main() @ &m : G2.guessed].
proof. by rewrite (Guessing_G1 &m) (G1_G2 &m). qed.

(* upper bounding of probabiliy of secret being guessed *)

local lemma G2_Prob &m :
  Pr[G2.main() @ &m : G2.guessed] <=
  limit%r / (2 ^ sec_len)%r.
proof.
byphoare (_ : true ==> G2.guessed) => //.
proc.
seq 2 :
  (SGOrAccum.ctr <= limit /\ card SGOrAccum.guesses <= SGOrAccum.ctr)
  1%r
  (limit%r / (2 ^ sec_len)%r)
  0%r
  1%r => //.
wp; rnd; skip.
progress; rewrite (mu_sec_distr_mem_limit SGOrAccum.guesses{hr}) /#.
hoare; simplify.
call
  (_ :
   SGOrAccum.ctr <= limit /\ card SGOrAccum.guesses <= SGOrAccum.ctr ==>
   SGOrAccum.ctr <= limit /\ card SGOrAccum.guesses <= SGOrAccum.ctr).
proc
  (SGOrAccum.ctr <= limit /\ card SGOrAccum.guesses <= SGOrAccum.ctr) => //.
apply SGOrAccum_guess_Card.
inline *; auto; smt(limit_ge0 fcards0).
qed.

lemma GuessingProb' &m :
  Pr[Guessing(SGAdv).main() @ &m : SGOr.guessed] <=
  limit%r / (2 ^ sec_len)%r.
proof. by rewrite (Guessing_G2 &m) (G2_Prob &m). qed.

end section.

lemma GuessingProb (SGAdv <: SG_ADV{-SGOr}) &m :
  Pr[Guessing(SGAdv).main() @ &m : SGOr.guessed] <=
  limit%r / (2 ^ sec_len)%r.
proof. apply (GuessingProb' SGAdv &m). qed.