https://github.com/EasyCrypt/easycrypt
Revision 9f6a2f9c698e6c47fa841a0b040bc45d82a601c5 authored by Benjamin Gregoire on 07 July 2016, 06:32:45 UTC, committed by Benjamin Gregoire on 07 July 2016, 06:32:45 UTC
1 parent 776af38
Tip revision: 9f6a2f9c698e6c47fa841a0b040bc45d82a601c5 authored by Benjamin Gregoire on 07 July 2016, 06:32:45 UTC
add make
add make
Tip revision: 9f6a2f9
PSS.ec
timeout 0.
(** This proof is naively adapted from
"Making RSA-PSS secure against non-random faults"
As such, it may contain some weird quirks that are
due to that more complex context.
**)
require import Pair.
require import Option.
require import Int.
require import Real.
require import Distr.
(*---*) import Dprod.
(*---*) import Dapply.
require import FMap.
require import ABitstring.
require import FSet.
(*---*) import Interval.
require ISet.
(*---*) import ISet.Finite.
require import Sum. (* for the FEL tactic *)
(*---*) import Monoid.Mrplus.
require List.
(* Generics that we clone later *)
require AWord.
require ROM.
require PKS.
require OW.
(** We want to build a public-key signature scheme
from arbitrary-length bitstrings to
fixed-(k)-length bitstrings *)
type message = bitstring.
op k: int.
axiom leq4_k: 4 <= k.
type signature.
type padded = signature.
op signature: padded distr.
clone import AWord as Signature with
type word <- signature,
op length <- k,
op Dword.dword <- signature
proof
leq0_length by smt.
op from_signature: signature -> bitstring = Signature.to_bits.
op to_signature: bitstring -> signature = Signature.from_bits.
lemma signature_finite: finite ISet.univ<:signature> by [].
(* We only convert to and from integers on full k-length bitstrings.
In the absence of a concrete implementation of the conversion,
we axiomatize the additional property we need for our proof to
go through: that integers below 2^(k - 1) are exactly those
whose representation have a leading zero. *)
op i2osp = Signature.from_int.
op os2ip = Signature.to_int.
lemma os2ip_bnd x: 0 <= os2ip x < 2^k.
proof. by rewrite /os2ip -to_from from_to; smt. qed.
lemma can_i2osp_os2ip x: i2osp (os2ip x) = x
by [].
lemma pcan_os2ip_i2osp x:
0 <= x < 2^k =>
os2ip (i2osp x) = x
by [].
axiom msb0_bnd s:
sub (from_signature s) 0 1 = zeros 1 <=>
os2ip s < 2^(k - 1).
(*** We rely on RSA (we may be able to generalize, but it
looks like the proof requires very strong homomorphic
and invertibility properties). We axiomatize RSA as
abstractly as possible below. *)
(** Keys are left partially abstract *)
type pkey.
op p_n: pkey -> int.
op p_e: pkey -> int.
axiom finite_pkey : finite (ISet.univ <:pkey>).
type skey.
op s_d: skey -> int.
op s_p: skey -> int.
op s_q: skey -> int.
op s_n: skey -> int = fun sk,
s_p sk * s_q sk.
axiom finite_skey : finite (ISet.univ <:skey>).
(** They are generated by sampling in this distribution *)
type keypair = pkey * skey.
op keypairs: keypair distr.
axiom keypairsL: mu keypairs True = 1%r.
(* Necessary conditions for (pk,sk) to be a valid keypair:
* - the public and private modulus are identical, and
* - the modulus is exactly k bits long *)
axiom valid_keypairs pk sk:
support keypairs (pk,sk) =>
p_n pk = s_n sk /\
2^(k - 1) <= p_n pk < 2^k.
(** The permutations *)
op rsap pk (m:int) =
let e = p_e pk in
let n = p_n pk in
(m^e) %% n axiomatized by rsapE.
op rsas sk (m:int) =
let d = s_d sk in
let n = s_n sk in
(m^d) %% n axiomatized by rsasE.
(** Validity conditions and axioms *)
op rsap_dom pk m =
0 <= m < p_n pk.
op rsas_dom sk m =
0 <= m < s_n sk.
axiom rsap_range pk m:
rsap_dom pk m =>
rsap_dom pk (rsap pk m).
axiom rsas_range sk m:
rsas_dom sk m =>
rsas_dom sk (rsas sk m).
axiom rsap_rsas pk sk m:
support keypairs (pk,sk) =>
rsap_dom pk m =>
rsap pk (rsas sk m) = m.
axiom rsas_rsap pk sk m:
support keypairs (pk,sk) =>
rsap_dom pk m =>
rsas sk (rsap pk m) = m.
lemma rsap_rsas_dom pk sk:
support keypairs (pk,sk) =>
rsap_dom pk = rsas_dom sk.
proof.
move=> vkeys; apply valid_keypairs in vkeys.
move: vkeys=> [eq_N _].
by rewrite /rsas_dom -eq_N.
qed.
lemma rsap_range_sk pk sk m:
support keypairs (pk,sk) =>
rsas_dom sk m =>
rsas_dom sk (rsap pk m).
proof.
move=> vkeys.
rewrite -(rsap_rsas_dom pk) // => m_in_dom.
by rewrite rsap_range.
qed.
lemma rsas_range_pk pk sk m:
support keypairs (pk,sk) =>
rsap_dom pk m =>
rsap_dom pk (rsas sk m).
proof.
move=> vkeys.
rewrite (rsap_rsas_dom pk sk) // => m_in_dom.
by rewrite rsas_range.
qed.
(** Additional properties of RSA. *)
op invertible: pkey -> int -> bool.
axiom card_noninvertible pk sk:
support keypairs (pk,sk) =>
card (filter (!(invertible pk)) (interval 0 (p_n pk - 1))) = s_p sk + s_q sk - 1.
(* We also need a bound on the probability of sampling a
non-invertible element (from Z/nZ) in [0..2^(k - 1)).
Non-invertible elemtns in Z/nZ are multiples of p and
multiples of q. There are at most 2^(k - 1) /% p
multiples of p in [0..2^(k - 1)) (and symmetrically for
q), and we can upper-bound 2^(k - 1) /% p by 2^(k /% 2 - 1).
The bound we use is twice that (multiples of p and
multiples of q). *)
axiom card_noninvertible_2k1 pk sk:
support keypairs (pk,sk) =>
card (filter (!(invertible pk)) (interval 0 (2^(k - 1) - 1))) <= 2^(k /% 2).
op inv: pkey -> int -> int.
op mulzp: pkey -> int -> int -> int.
op ( ** ) (x y:int) pk = mulzp pk x y.
axiom inv_range pk m:
rsap_dom pk m =>
rsap_dom pk (inv pk m).
axiom mulzp_range pk x y:
rsap_dom pk x =>
rsap_dom pk y =>
rsap_dom pk ((x ** y) pk).
axiom mulzp1 (x:int) (pk:pkey):
rsap_dom pk x =>
(1 ** x) pk = x.
axiom mulzpV (x:int) (pk:pkey):
rsap_dom pk x =>
invertible pk x =>
(x ** (inv pk x)) pk = 1.
axiom mulzpC x y pk:
rsap_dom pk x =>
rsap_dom pk y =>
(x ** y) pk = (y ** x) pk.
axiom mulzpA x y z pk:
rsap_dom pk x =>
rsap_dom pk y =>
rsap_dom pk z =>
(((x ** y) pk) ** z) pk = (x ** ((y ** z) pk)) pk.
axiom rsap_morphism_mulzp (x y:int) (pk:pkey):
rsap_dom pk x =>
rsap_dom pk y =>
rsap pk ((x ** y) pk) = ((rsap pk x) ** (rsap pk y)) pk.
axiom rsas_morphism_mulzp (x y:int) (pk:pkey) (sk:skey):
support keypairs (pk,sk) =>
rsap_dom pk x =>
rsap_dom pk y =>
rsas sk ((x ** y) pk) = ((rsas sk x) **(rsas sk y)) pk.
axiom invertible_mulzp x y pk:
(invertible pk x /\ invertible pk y) <=> invertible pk ((x ** y) pk).
axiom invertible_inv x pk:
invertible pk x <=> invertible pk (inv pk x).
(* The following axioms are consequences... They are left as axioms because
proving them is not the object of this effort. *)
axiom rsap_dom1 pk: rsap_dom pk 1.
axiom rsap_morphism0 (pk:pkey):
rsap pk 0 = 0.
axiom rsap_morphism1 (pk:pkey):
rsap pk 1 = 1.
axiom invertible_rsap (pk:pkey) (sk:skey) x:
support keypairs (pk,sk) =>
invertible pk x <=> invertible pk (rsap pk x).
axiom invertible_rsas (pk:pkey) (sk:skey) x:
support keypairs (pk,sk) =>
invertible pk x <=> invertible pk (rsas sk x).
axiom rsap_morphism_inv (x:int) (pk:pkey):
rsap_dom pk x =>
rsap pk (inv pk x) = inv pk (rsap pk x).
axiom rsas_morphism_inv (x:int) (pk:pkey) (sk:skey):
support keypairs (pk,sk) =>
rsap_dom pk x =>
rsas sk (inv pk x) = inv pk (rsas sk x).
(** The challenge distribution *)
op challenge (pk:pkey) = [0..p_n pk - 1].
lemma challenge_valid pk c:
in_supp c (challenge pk) <=> rsap_dom pk c
by [].
lemma challengeL pk sk:
support keypairs (pk,sk) =>
mu (challenge pk) True = 1%r.
proof.
move=> vkp; apply valid_keypairs in vkp.
cut:= Dinter.weight_def 0 (p_n pk - 1).
rewrite /challenge /weight (_: 0 <= p_n pk - 1) //=.
smt. (* 0 <= p_n pk - 1 *)
qed.
(* A lemma on the probability of sampling a challenge
whose most significant bit is 0 *)
lemma mu_challenge0 pk sk:
support keypairs (pk,sk) =>
mu (challenge pk) (fun x, mem x (interval 0 (2^(k - 1) - 1))) = (2 ^ (k - 1))%r / (p_n pk)%r.
proof.
move=> vkeys.
rewrite /challenge -Dinter_uni.dinter_is_dinter. (* Oh, look! Finite sets! *)
rewrite Dinter_uni.mu_def_nz; first smt.
rewrite Interval.card_interval_max (_: max (p_n pk - 1 - 0 + 1) 0 = p_n pk); first smt.
cut ->: filter (fun x, mem x (interval 0 (2^(k - 1) - 1))) (interval 0 (p_n pk - 1)) =
interval 0 (2^(k - 1) - 1).
by apply set_ext=> x; rewrite mem_filter /= !mem_interval; smt.
by rewrite card_interval_max (_: max (2^(k - 1) - 1 - 0 + 1) 0 = 2^(k - 1)); first smt.
qed.
clone OW as RSA with
type t <- int,
type pkey <- pkey,
type skey <- skey,
op keypairs <- keypairs,
op challenge <- challenge,
op f <- rsap,
op finv <- rsas
proof
keypairsL by apply keypairsL,
challengeL by (move=> pk; case=> sk; apply challengeL),
challengeU by (move=> pk _; apply Dinter.dinterU),
finv_correct,
fofinv by smt,
finvof by smt.
realize finv_correct.
move=> pk sk m vkp; cut:= vkp=> vkp'; apply valid_keypairs in vkp.
case=> x; rewrite /f_rng /f_dom=> -[vch ->].
rewrite rsas_rsap // /rsap_dom.
smt.
qed.
(*-*) import RSA.
(* Additional Facts useful for this particular setting of RSA *)
(* factor things *)
axiom s_p_bounds (sk:skey):
valid_skey sk =>
2^(k /% 2 - 1) <= s_p sk < 2^(k /% 2).
axiom s_q_bounds (sk:skey):
valid_skey sk =>
2^(k /% 2 - 1) <= s_q sk < 2^(k /% 2).
lemma rsap_dom_in_2k pk:
valid_pkey pk =>
rsap_dom pk <= (fun x, 0 <= x < 2^k)
by [].
lemma rsas_dom_in_2k sk:
valid_skey sk =>
rsas_dom sk <= (fun x, 0 <= x < 2^k)
by [].
(** We instantiate the PKS library with the appropriate types to define security *)
clone import PKS as PKSa
with
type pkey <- pkey,
type skey <- skey,
type message <- message,
type signature <- signature.
import NM_CMA.
module UF_CMA = NM_CMA.
(** Now we can set things up for the definition of PSS *)
(* Setting up the random salts *)
op k0:int.
axiom leq0_k0: 0 < k0.
type salt.
op salt: salt distr.
clone import AWord as Salt with
type word <- salt,
op length <- k0,
op Dword.dword <- salt
proof
leq0_length by smt.
op from_salt: salt -> bitstring = Salt.to_bits.
op to_salt: bitstring -> salt = Salt.from_bits.
(* Setting up H *)
op kh:int.
axiom leq0_kh: 0 < kh.
type htag.
op htag: htag distr.
axiom htagL: mu htag True = 1%r.
axiom htagU: isuniform htag.
axiom htagF x: support htag x.
axiom mux_htag: mu htag ((=) witness) = 1%r / (2^kh)%r.
clone import AWord as HTag with
type word <- htag,
op length <- kh,
op Dword.dword <- htag
proof
leq0_length by smt.
op from_htag: htag -> bitstring = HTag.to_bits.
op to_htag: bitstring -> htag = HTag.from_bits.
lemma htag_finite: finite ISet.univ<:htag> by [].
(* A note on using "message * salt" as domain for H.
This is my way of forcing the bad guy to call H with at least k0 bits.
It is easy to see the following if we let the adversary call H with less than k0 bits:
- the two oracles can be separated with no possibility of query-level collision,
- the probability of a response-level collision is the same. *)
clone ROM.Lazy as Ht with
type from <- message * salt,
type to <- htag,
op dsample <- fun (x:message * salt), htag.
module H = Ht.RO.
(* Setting up G *)
op kg:int.
axiom lt_0_kg: 0 < kg.
type gtag.
op gtag: gtag distr.
axiom gtagL: mu gtag True = 1%r.
axiom gtagU: isuniform gtag.
axiom gtagF x: support gtag x.
axiom mux_gtag: mu gtag ((=) witness) = 1%r / (2^kg)%r.
clone import AWord as GTag with
type word <- gtag,
op length <- kg,
op Dword.dword <- gtag
proof
leq0_length by smt.
op from_gtag: gtag -> bitstring = GTag.to_bits.
op to_gtag: bitstring -> gtag = GTag.from_bits.
lemma gtag_finite: finite ISet.univ<:gtag> by [].
clone ROM.LazyEager as Gt with
type from <- htag,
type to <- gtag,
op dsample <- fun (x:htag), gtag.
module G = Gt.Lazy.RO.
module Ge = Gt.Eager.RO.
(** Constraints on lengths k, k0, kh, kg *)
axiom k_constraints:
k0 <= kg /\
k = 1 + kh + kg.
(** PSS96 definition *)
op Delta: int distr. (* we need to know things about this *)
axiom DeltaL: mu Delta True = 1%r.
module PSS96(H:Ht.Types.Oracle,G1:Gt.Types.Oracle): Scheme = {
proc init(): unit = {
H.init();
G.init();
}
proc keygen(): (pkey * skey) = {
var pk, sk;
(pk,sk) = $keypairs;
return (pk,sk);
}
proc sign(sk:skey, m:message): signature = {
var r, w, g, rs, em;
var s;
r = $salt;
w = H.o(m,r);
g = G.o(w);
rs = g ^ (to_gtag (from_salt r || zeros (kg - k0)));
em = to_signature (zeros 1 || (from_htag w) || (from_gtag rs));
s = i2osp (rsas sk (os2ip em));
return s;
}
proc verify(pk:pkey, m:message, s:signature): bool = {
var re;
var y, b, w, rs, g, ga, r, w';
re = false;
if (0 <= os2ip s < p_n pk) {
y = from_signature (i2osp (rsap pk (os2ip s)));
b = sub y 0 1;
w = to_htag (sub y 1 kh);
rs = to_gtag (sub y (1 + kh) kg);
g = G.o(w);
r = sub (from_gtag (g ^ rs)) 0 k0;
ga = sub (from_gtag (g ^ rs)) k0 (kg - k0);
w' = H.o(m,to_salt r);
re = (b = zeros 1 /\ w' = w /\ ga = zeros (kg - k0));
}
return re;
}
}.
(* Some types to make things easier on ourselves *)
type hmap = (message * salt,bool * htag * int) map.
type gmap = (htag,gtag) map.
(* CMA adversary with 2 random oracles *)
module type PSS_AdvCMA (H:Ht.Types.ARO,G:Gt.Types.ARO,O:AdvOracles) = {
proc forge(pk:pkey): message * signature
}.
(* Bounding the adversary *)
op qH:int.
axiom leq0_qH: 0 <= qH.
op qG:int.
axiom leq0_qG: 0 < qG.
op qS:int.
axiom leq0_qS: 0 <= qS.
module Bounded_PSS_Adv(A:PSS_AdvCMA,H:Ht.Types.ARO,G:Gt.Types.ARO,O:AdvOracles) = {
var cH, cG, cS, cF:int
module Hc = {
proc o(mr:message * salt): htag = {
var r = witness;
if (cH < qH) {
r = H.o(mr);
cH = cH + 1;
}
return r;
}
}
module Gc = {
proc o(w:htag): gtag = {
var r = witness;
if (cG < qG) {
r = G.o(w);
cG = cG + 1;
}
return r;
}
}
module Oc = {
proc sign(m:message): signature = {
var r = witness;
if (cS < qS) {
r = O.sign(m);
cS = cS + 1;
}
return r;
}
}
module Ac = A(Hc,Gc,Oc)
proc forge(pk:pkey): message * signature = {
var r;
cH = 0;
cG = 0;
cS = 0;
cF = 0;
r = Ac.forge(pk);
return r;
}
}.
(** Defining complex distributions for the proof: we will switch
from sampling in the uniform distribution over the
preimage of [0..2^(k - 1)[ by the function simul defined
below to sampling in challenge until the value is within
the preimage of [0..2^(k - 1)[ as desired. *)
op simul (pk:pkey) (sk:skey) (b:bool) (x u:int) =
if b then ((rsap pk x) ** (rsap pk u)) pk
else rsap pk u.
(* For simplicity in the formal proof, we will instead
consider the uniform distribution on the image of
[0..2^(k - 1)[ by the inverse permutation (when it is
a permutation) defined as follows. This is strictly
equivalent (and can be proved equivalent). *)
op simul_inv (pk:pkey) (sk:skey) (b:bool) (x z:int) =
if b then ((inv pk x) ** (rsas sk z)) pk
else rsas sk z.
op sigd (pk:pkey) (sk:skey) (b:bool) (x:int): int distr =
dapply (simul_inv pk sk b x) ([0..2^(k - 1) - 1]).
(* We prove lots of lemmas that are useful along the way. *)
lemma simul_range (pk:pkey) (sk:skey) (b:bool) (x u:int):
support keypairs (pk,sk) =>
rsap_dom pk x =>
rsap_dom pk u =>
rsap_dom pk (simul pk sk b x u).
proof.
move=> vkeys x_bnd u_bnd.
case b; rewrite /simul /=; last by move=> _; apply rsap_range; smt.
by move=> _; rewrite mulzp_range ?rsap_range.
qed.
lemma simul_inv_range (pk:pkey) (sk:skey) (b:bool) (x u:int):
support keypairs (pk,sk) =>
rsap_dom pk x =>
rsap_dom pk u =>
rsap_dom pk (simul_inv pk sk b x u).
proof.
move=> vkeys x_bnd u_bnd.
case b; rewrite /simul_inv /=; last by move=> _; apply rsas_range_pk; smt.
by move=> _; rewrite mulzp_range 1:inv_range // 1:rsas_range_pk.
qed.
lemma simulK (pk:pkey) (sk:skey) (b:bool) (x u:int):
support keypairs (pk,sk) =>
rsap_dom pk x =>
rsap_dom pk u =>
(b => invertible pk x) =>
simul_inv pk sk b x (simul pk sk b x u) = u.
proof.
move=> vkeys x_bnd u_bnd x_nonzero.
rewrite /simul /simul_inv; case b; last by rewrite rsas_rsap.
move=> bt; rewrite rsas_morphism_mulzp ?rsap_range //.
apply x_nonzero in bt.
rewrite !rsas_rsap //.
rewrite -mulzpA 1:inv_range //.
by rewrite (mulzpC _ x) 1:inv_range // mulzpV // mulzp1.
qed.
lemma simul_invK (pk:pkey) (sk:skey) (b:bool) (x u:int):
support keypairs (pk,sk) =>
rsap_dom pk x =>
rsap_dom pk u =>
(b => invertible pk x) =>
simul pk sk b x (simul_inv pk sk b x u) = u.
proof.
move=> vkeys x_bnd u_bnd x_nonzero.
rewrite /simul /simul_inv; case b; last by rewrite rsap_rsas.
move=> bt; rewrite rsap_morphism_mulzp ?rsap_range // 1:inv_range // 1:rsas_range_pk //.
apply x_nonzero in bt.
rewrite !rsap_rsas //.
rewrite -mulzpA ?rsap_range // 1:inv_range //.
by rewrite -rsap_morphism_mulzp // 1:inv_range // mulzpV // rsap_morphism1 mulzp1.
qed.
lemma supp_sigd pk sk b x s:
valid_keys (pk,sk) =>
rsap_dom pk x =>
(b => invertible pk x) =>
in_supp s (sigd pk sk b x) <=> (rsap_dom pk s /\ 0 <= simul pk sk b x s < 2^(k - 1)).
proof.
rewrite /valid_keys=> vkeys x_bnd x_nonzero.
rewrite /sigd supp_def.
split.
elim=> y [->]; rewrite Dinter.supp_def=> supp_y.
by rewrite simul_invK //; first 2 smt.
move=> [supp_s supp_simul]; exists (simul pk sk b x s); split.
by rewrite simulK.
by rewrite Dinter.supp_def; smt.
qed.
lemma sigdX_interX pk sk b x u:
valid_keys (pk,sk) =>
support (sigd pk sk b x) u =>
rsap_dom pk x =>
(b => invertible pk x) =>
mu (sigd pk sk b x) ((=) u) = mu [0..2^(k - 1) - 1] ((=) (simul pk sk b x u)).
proof.
move=> vkeys supp_u x_bnd x_nonzero; rewrite /sigd.
rewrite mu_def (mu_support (fun x0, u = simul_inv pk sk b x x0)) (mu_support ((=) (simul pk sk b x u))).
apply mu_eq=> y /=; rewrite eq_iff /Pred.(/\) /=; split=> //.
by move=> [->] sup_y; split=> //; rewrite simul_invK //; first smt.
by move=> [<-] sup_y; split=> //; rewrite simulK //; first smt.
qed.
lemma sigdU pk sk b x:
valid_keys (pk,sk) =>
rsap_dom pk x =>
(b => invertible pk x) =>
isuniform (sigd pk sk b x).
proof.
move=> vkeys x_bnd x_nonzero s0 s1 supp_s0 supp_s1.
rewrite /mu_x.
do 2!rewrite sigdX_interX //.
by apply Dinter.dinterU; rewrite /in_supp /mu_x -sigdX_interX.
qed.
lemma sigdL pk sk b x: mu (sigd pk sk b x) True = 1%r.
proof. by rewrite /sigd -/(weight _) Dapply.lossless Dinter.weight_def; smt. qed.
lemma sigdX pk sk b x u:
valid_keys (pk,sk) =>
rsap_dom pk x =>
support (sigd pk sk b x) u =>
(b => invertible pk x) =>
mu (sigd pk sk b x) ((=) u) = 1%r/(2^(k - 1))%r.
proof.
move=> vkeys x_bnd u_bnd x_nonzero.
rewrite sigdX_interX //.
by rewrite -/(mu_x _ _) Dinter.mu_x_def_in; smt.
qed.
lemma mu_challenge_in_pim pk sk b x:
support keypairs (pk,sk) =>
rsap_dom pk x =>
(b => invertible pk x) =>
mu (challenge pk)
(fun y, 0 <= simul pk sk b x y < 2^(k - 1))
= (2^(k - 1))%r / (p_n pk)%r.
proof.
move=> vkeys x_in_dom x_invertible.
pose f:= fun y, simul pk sk b x y.
pose finv:= fun y, simul_inv pk sk b x y.
cut ->: (fun y, 0 <= simul pk sk b x y < 2^(k - 1)) = Fun.preim f (fun x, 0 <= x < 2^(k - 1))
by beta.
rewrite -Dapply.dapply_preim.
cut supp_eq: support (dapply f (challenge pk)) = support (challenge pk).
apply fun_ext=> x'; rewrite /challenge /support Dapply.supp_def eq_iff; split.
move=> [y [->]]; rewrite -/(rsap_dom _ _) !Dinter.supp_def.
cut H2: forall x y, 0 <= x <= y - 1 = 0 <= x < y by smt.
by rewrite !H2 -/(rsap_dom _ _) -/(rsap_dom _ _) /f=> {H2}; apply simul_range.
rewrite Dinter.supp_def.
cut H2: forall x y, 0 <= x <= y - 1 = 0 <= x < y by smt.
rewrite H2 -/(rsap_dom _ _)=> x'_in_dom.
exists (finv x'); split.
by rewrite /f /finv simul_invK=> //.
by rewrite Dinter.supp_def H2 -/(rsap_dom _ _) /finv; apply simul_inv_range.
cut ->: dapply f (challenge pk) = challenge pk.
apply uniform_unique=> //.
by rewrite Dapply.mu_def.
move=> x' y'; progress.
rewrite !Dapply.mu_x_def (mu_support (fun x0, x' = f x0)) (mu_support (fun x0, y' = f x0)).
cut invert: forall x, support (challenge pk) x =>
((fun x0, x = f x0) /\ support (challenge pk))
= ((=) (finv x) /\ support (challenge pk)).
progress; rewrite /Pred.(/\) /= -fun_ext=> x1 /=; rewrite eq_iff; split.
by move=> [-> x1_in_supp]; rewrite /f /finv simulK //; smt.
by move=> [<- x1_in_supp]; rewrite /f /finv simul_invK //; smt.
rewrite invert 1:-supp_eq 1:/support //.
rewrite invert 1:-supp_eq 1:/support //.
rewrite -!mu_support.
apply challengeU; first smt.
by cut:= H; rewrite -/(support _ _) supp_eq /support !challenge_valid /finv simul_inv_range //; smt.
by cut:= H0; rewrite -/(support _ _) supp_eq /support !challenge_valid /finv simul_inv_range //; smt.
by apply challengeU; exists sk.
cut ->: (fun x, 0 <= x < 2^(k - 1)) = (fun x, mem x (interval 0 (2^(k - 1) - 1))).
by apply fun_ext=> z //=; rewrite mem_interval; smt.
by apply (mu_challenge0 _ sk).
qed.
(*** Some useful notations *)
op pi3_1 (x:'a * 'b * 'c) = x.`1.
op pi3_2 (x:'a * 'b * 'c) = x.`2.
op pi3_3 (x:'a * 'b * 'c) = x.`3.
(*** The inverter *)
type caller = [ Adv | Sig ].
module Inverter(A:PSS_AdvCMA): RSA.Inverter = {
var h:(message * salt,htag * caller * int) map
var g:(htag,gtag * caller) map
var pk:pkey
var ystar:int
var cH, cG, cS, cF:int
module G = {
proc o(w:htag): gtag = {
var r;
r = $gtag;
if (!mem w (dom g)) g.[w] = (r,Adv);
return fst (oget g.[w]);
}
}
module Ga = {
proc o(w:htag): gtag = {
var r;
if (cG < qG) {
r = G.o(w);
cG = cG + 1;
}
else r = witness;
return r;
}
}
module Ha = {
proc o(mr:message * salt): htag = {
var m, r, w, st, u, z, i;
(m,r) = mr;
u = 0;
w = witness;
st = witness;
i = 0;
z = 2^k - 1;
if (cH < qH) {
if (invertible pk ystar) {
while (!0 <= z < 2^(k - 1) /\ i < k0 + 1) {
u = $challenge pk;
z = (ystar ** (rsap pk u)) pk;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
i = i + 1;
}
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (0 <= z < 2^(k - 1) /\ invertible pk u) {
if (!mem (m,r) (dom h)) {
if (!mem w (dom g)) {
h.[(m,r)] = (w,Adv,u);
g.[w] = (st,Adv);
}
} else
w = pi3_1 (oget h.[(m,r)]);
} else
w = witness;
}
cH = cH + 1;
}
return w;
}
}
module S = {
proc sign(m:message): signature = {
var r, w, st, u, z, i, s;
s = witness;
i = 0;
z = 2^k - 1;
r = $salt;
u = 0;
w = witness;
st = witness;
if (cS < qS) {
while (!0 <= z < 2^(k - 1) /\ i < k0 + 1) {
u = $challenge pk;
z = rsap pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
i = i + 1;
}
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (0 <= z < 2^(k - 1)) {
if (!mem (m,r) (dom h)) {
if (!mem w (dom g)) {
h.[(m,r)] = (w,Sig,u);
g.[w] = (st,Sig);
}
s = i2osp u;
}
}
cS = cS + 1;
}
return s;
}
}
module A = A(Ha,Ga,S)
proc invert(pk:pkey, c:int): int = {
var m, s, y, w, st, w', st', r, c', u, x;
Inverter.h = FMap.empty;
Inverter.g = FMap.empty;
Inverter.pk = pk;
Inverter.ystar = c;
Inverter.cF = 0;
Inverter.cS = 0;
Inverter.cG = 0;
Inverter.cH = 0;
u = 1;
(m,s) = A.forge(pk);
y = from_signature (i2osp (rsap pk (os2ip s)));
w = to_htag (sub y 1 kh);
st = to_gtag (sub y (1 + kh) kg);
st' = G.o(w);
r = to_salt (sub (from_gtag (st ^ st')) 0 k0);
w' = $htag;
if (mem (m,r) (dom h))
(w',c',u) = oget h.[(m,r)];
x = ((os2ip s) ** (inv pk u)) pk;
return x;
}
}.
(*** Games and transitions *)
section.
declare module A: PSS_AdvCMA {H,G,Ge,Wrap(PSS96(H,G)),Bounded_PSS_Adv,
Inverter}.
axiom A_forge_ll (H <: Ht.Types.ARO {A}) (G <: Gt.Types.ARO {A}) (O <: AdvOracles {A}):
islossless H.o =>
islossless G.o =>
islossless O.sign =>
islossless A(H,G,O).forge.
(* This is the memory that is used by the concrete adversary during the proof *)
(* In the final transition, we rewrite the concrete adversary into an
adversary against OW, and therefore drop the secret key from its state. *)
local module Mem = {
var pk:pkey
var sk:skey
var qs:(message * signature) set
var fs:(message * signature) set
var cH, cG, cS:int
proc init(ks:pkey * skey): unit = {
(pk,sk) = ks;
qs = FSet.empty;
fs = FSet.empty;
cH = 0;
cG = 0;
cS = 0;
}
}.
(* The oracle H is split between adversary queries,
and queries made by the signature oracle *)
module type SplitOracle = {
proc init(ks:pkey * skey):unit { }
proc o(c:caller,m:message,r:salt):htag option
proc v(m:message,r:salt):htag (* for use by the experiment *)
}.
(** Since the proof mostly works by modifying H,
with some eager-style interactions with G,
we will mostly reason in terms of a concrete
adversary trying to distinguish various
implementations of G and H through the signing
oracle. This should allow some abstraction in the
proof, and in particular in the two eager steps
on G. **)
module type Gadv (H:SplitOracle, G:Gt.Types.ARO) = {
proc main (ks:pkey * skey): bool {H.o G.o H.v}
}.
local module Gen (Gadv:Gadv, H:SplitOracle, G:Gt.Types.Oracle) = {
module GA = Gadv(H,G)
proc main () : bool = {
var keys, b;
keys = $keypairs;
G.init();
H.init(keys);
b = GA.main(keys);
return b;
}
}.
local module GAdv(H:SplitOracle, G:Gt.Types.ARO) = {
(* Wrapping a split oracle for direct use by the adversary *)
module Ha = {
proc o(m:message * salt): htag = {
var r = None;
if (Mem.cH < qH) {
r = H.o(Adv,fst m,snd m);
Mem.cH = Mem.cH + 1;
}
return oget r;
}
}
(* Wrapping a split oracle for use by the signing oracle *)
module Hs = {
proc o(m:message * salt): htag option = {
var r;
r = H.o(Sig,fst m,snd m);
return r;
}
}
(* Counting queries to G *)
module Ga = {
proc o(w:htag): gtag = {
var r = witness;
if (Mem.cG < qG) {
r = G.o(w);
Mem.cG = Mem.cG + 1;
}
return r;
}
}
(* Signing oracle *)
module S = {
proc sign(m:message): signature = {
var r, wo, w, g, rs, em;
var s = witness;
if (Mem.cS < qS) {
r = $salt;
wo = Hs.o(m,r);
if (wo = None)
s = witness;
else {
w = oget wo;
g = G.o(w);
rs = g ^ (to_gtag (from_salt r || zeros (kg - k0)));
em = to_signature (zeros 1 || (from_htag w) || (from_gtag rs));
s = i2osp (rsas Mem.sk (os2ip em));
Mem.qs = add (m,s) Mem.qs;
}
Mem.cS = Mem.cS + 1;
}
return s;
}
proc fresh(m:message, s:signature): bool = {
return !mem (m,s) Mem.qs;
}
}
module A = A(Ha, Ga, S)
proc main (ks:pkey*skey): bool = {
var m, s;
var y, w, st, g, rs, r, w';
Mem.init(ks);
(m,s) = A.forge(Mem.pk);
y = from_signature (i2osp (rsap Mem.pk (os2ip s)));
w = to_htag (sub y 1 kh);
st = to_gtag (sub y (1 + kh) kg);
g = G.o(w);
rs = from_gtag (st ^ g);
r = to_salt (sub rs 0 k0);
w' = H.v(m,r);
return sub y 0 1 = zeros 1 /\ w = w' /\ sub rs k0 (kg - k0) = zeros (kg - k0) /\
0 <= os2ip s < p_n Mem.pk /\ !mem (m,s) Mem.qs;
}
}.
(* Generic losslessness lemmas for wrapped split oracles *)
local lemma GAdvHa_o_ll (H <: SplitOracle {GAdv}) (G <: Gt.Types.ARO {GAdv}):
islossless H.o => islossless GAdv(H,G).Ha.o.
proof. by move=> H_o_ll; proc; sp; if=> //; wp; call H_o_ll. qed.
local lemma GAdvHs_o_ll (H <: SplitOracle {GAdv}) (G <: Gt.Types.ARO {GAdv}):
islossless H.o => islossless GAdv(H,G).Hs.o.
proof. by move=> H_o_ll; proc; call H_o_ll. qed.
local lemma GAdvGa_o_ll (H <: SplitOracle {GAdv}) (G <: Gt.Types.ARO {GAdv}):
islossless G.o => islossless GAdv(H,G).Ga.o.
proof. by move=> G_o_ll; proc; sp; if=> //; wp; call G_o_ll. qed.
(* Generic losslessness lemma for refactored PSS *)
local lemma GAdv_main_ll (H <: SplitOracle {GAdv}) (G <: Gt.Types.ARO {GAdv}):
islossless H.o => islossless G.o => islossless H.v => islossless GAdv(H, G).main.
proof.
move=> H_o_ll G_o_ll H_v_ll; proc.
call H_v_ll.
wp; call G_o_ll.
wp; call (A_forge_ll (<:GAdv(H,G).Ha) (<:GAdv(H,G).Ga) (<:GAdv(H,G).S) _ _ _).
by apply (GAdvHa_o_ll H G _)=> //.
by apply (GAdvGa_o_ll H G _)=> //.
proc; sp; if=> //; seq 2: true=> //.
by call (GAdvHs_o_ll H G _)=> //; rnd; skip; smt.
if; first by wp.
wp; call G_o_ll.
by wp.
by call (_: true)=> //; wp.
qed.
(** A module to store the globals used
in most variants of H, along with
some useful equality predicates *)
local module Hmem = {
var pk:pkey
var sk:skey
var xstar:int
var ystar:int
proc init(ks:pkey*skey): unit = {
(pk,sk) = ks;
xstar = $challenge pk;
ystar = rsap pk xstar;
}
}.
local module Hmap = {
var m:(message * salt,htag * caller * int) map
proc init(ks:pkey*skey) : unit = {
Hmem.init(ks);
m = FMap.empty;
}
}.
(* We pass on as much information as possible to make later proofs easier. *)
local equiv Hmem_init:
Hmem.init ~ Hmem.init: ={ks} /\ valid_keys ks{2} ==>
={glob Hmem} /\
valid_keys (Hmem.pk,Hmem.sk){2} /\
rsap_dom Hmem.pk{2} Hmem.xstar{2} /\
rsap_dom Hmem.pk{2} Hmem.ystar{2} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
Hmem.xstar{2} = rsas Hmem.sk{2} Hmem.ystar{2}.
proof.
proc; auto.
move=> &1 &2 /=; elim/tuple2_ind (ks{2})=> ks2 pk sk ks2_def [ks1_def vkeys] /=; subst.
by progress; expect 5 smt.
qed.
lemma divrM (r1 r2 r3:real): 0%r <= r1 => 0%r < r3 <= r2 => r1 / r2 <= r1 / r3.
proof.
move=> lt0r1 [lt0r3 ler3r2].
rewrite !(div_def r1) ~3:smt !(Real.Comm.Comm r1); apply mulrMle=> //.
cut ->: 1%r / r2 = inv r2 by smt.
cut ->: 1%r / r3 = inv r3 by smt.
by apply inv_le; first smt.
qed.
local lemma Hmem_init_bad:
phoare [Hmem.init: support keypairs ks ==>
!invertible Hmem.pk Hmem.xstar] <= (1%r/(2^(k /% 2 - 2))%r).
proof.
proc; wp; rnd (!invertible Hmem.pk); wp; skip=> //= &hr.
elim/tuple2_ind (ks{hr})=> ks pk sk ks_def //=; progress=> //.
cut vpk: valid_pkey pk by exists sk.
rewrite /challenge -Dinter_uni.dinter_is_dinter.
rewrite Dinter_uni.mu_def_nz; first by apply (Int.Trans _ (2^(k-1) - 1)); smt.
rewrite (card_noninvertible pk sk) //.
rewrite card_interval_max (_: max (p_n pk - 1 - 0 + 1) 0 = p_n pk); first smt.
cut p_q_2k: s_p sk + s_q sk - 1 <= 2^(k /% 2 + 1) by smt.
cut k2_pq: 2^(k - 1) <= p_n pk by smt.
apply (Trans _ ((2^(k /% 2 + 1))%r/(2^(k - 1))%r)).
apply (Trans _ ((s_p sk + s_q sk - 1)%r/(2 ^ (k - 1))%r )).
apply divrM; last smt.
cut: 0 < s_p sk + s_q sk - 1; last smt.
cut: 0 < s_p sk /\ 0 < s_q sk; last by smt.
cut H0: forall (x y:int), 0 <= x => 0 <= y => 0 < x * y => 0 < x /\ 0 < y by smt.
apply H0.
by cut: 2^(k /%2 - 1) <= s_p sk; smt.
by cut: 2^(k /%2 - 1) <= s_q sk; smt.
smt.
cut H0: forall (x y z:real), 0%r < z => x <= y => x / z <= y / z by smt.
by apply H0; smt.
rewrite Real.PowerInt.pow_div_den; first smt.
cut ->: k - 1 - (k /% 2 + 1) = k - k /% 2 - 2 by smt.
cut leq: k /% 2 - 2 <= k - k /% 2 - 2 by smt.
apply (_: forall (x y:real), 0%r < x <= y => 1%r / y <= 1%r / x); first smt.
split; first smt.
by rewrite FromInt.from_intMle; smt.
qed.
local equiv Hmap_init:
Hmap.init ~ Hmap.init: ={ks} /\ valid_keys ks{2} ==>
={glob Hmap} /\
valid_keys (Hmem.pk,Hmem.sk){2} /\
rsap_dom Hmem.pk{2} Hmem.xstar{2} /\
rsap_dom Hmem.pk{2} Hmem.ystar{2} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
Hmem.xstar{2} = rsas Hmem.sk{2} Hmem.ystar{2}.
proof. by proc; wp; call Hmem_init. qed.
(** Partial equalities between simple and extended maps *)
(* extending a single output map to triple output *)
pred hmap_preq (m0:('a,'b) map) (m1:('a,'b * 'c * 'd) map) =
forall x, m0.[x] = omap pi3_1 m1.[x].
lemma hmap_preq_dom m0 (m1:('a,'b * 'c * 'd) map) x:
hmap_preq m0 m1 =>
mem x (dom m0) <=> mem x (dom m1).
proof.
rewrite /hmap_preq=> m0_m1.
cut: !mem x (dom m0) <=> !mem x (dom m1); last smt.
by rewrite !mem_dom /= m0_m1 none_omap.
qed.
lemma hmap_preq_get m0 (m1:('a,'b * 'c * 'd) map) x:
hmap_preq m0 m1 =>
m0.[x] = omap pi3_1 m1.[x].
proof. by move=> hmap_eq; cut:= hmap_eq x. qed.
(* extending a single output map to pair output *)
pred gmap_preq (m0:('a,'b) map) (m1:('a,'b * 'c) map) = forall x,
m0.[x] = omap fst m1.[x].
lemma gmap_preq_dom m0 (m1:('a,'b * 'c) map) x:
gmap_preq m0 m1 =>
mem x (dom m0) <=> mem x (dom m1).
proof.
rewrite /gmap_preq=> m0_m1.
cut: !mem x (dom m0) <=> !mem x (dom m1); last smt.
by rewrite !mem_dom /= m0_m1 none_omap.
qed.
lemma gmap_preq_get m0 (m1:('a,'b * 'c) map) x:
gmap_preq m0 m1 =>
m0.[x] = omap fst m1.[x].
proof. by move=> gmap_eq; cut:= gmap_eq x. qed.
lemma gmap_preq_set m0 (m1:('a,'b * 'c) map) x y z:
gmap_preq m0 m1 =>
gmap_preq m0.[x <- y] m1.[x <- (y,z)].
proof.
move=> gmap_eq x0; case (x = x0).
by move=> ->; rewrite !get_set_eq.
by move=> neq; rewrite !get_set_neq 3:gmap_eq.
qed.
(* partial equality of maps with range triples where we consider
only the first two elements *)
pred hmap_peq (m0 m1:('a,'b * 'c * 'd) map) = forall x,
(omap (fun (x:'b * 'c * 'd), (x.`1,x.`2)) m1.[x] = omap (fun (x:'b * 'c * 'd), (x.`1,x.`2)) m0.[x]).
lemma hmap_peq_dom (m0 m1:('a,'b * 'c * 'd) map) x:
hmap_peq m0 m1 =>
mem x (dom m0) <=> mem x (dom m1).
proof.
move=> hmap_peq; cut: !mem x (dom m0) <=> !mem x (dom m1); last smt.
rewrite !mem_dom /=.
cut:= hmap_peq x.
by case (m0.[x])=> //=; [apply none_omap | case (m1.[x])].
qed.
lemma hmap_peq_set (m0 m1:('a,'b * 'c * 'd) map) x b c d d':
hmap_peq m0 m1 =>
hmap_peq m0.[x <- (b,c,d)] m1.[x <- (b,c,d')].
proof.
move=> hmap_peq x0.
case (x = x0).
by move=> <-; rewrite !get_set_eq.
by move=> neq_x0_x; rewrite !get_set_neq // hmap_peq.
qed.
lemma hmap_peq_get1 (m0 m1:('a,'b * 'c * 'd) map) x:
hmap_peq m0 m1 =>
pi3_1 (oget m0.[x]) = pi3_1 (oget m1.[x]).
proof.
move=> hmap_peq; cut:= hmap_peq x.
by case (m0.[x])=> //=; case (m1.[x])=> //=; smt.
qed.
lemma hmap_peq_get2 (m0 m1:('a,'b * 'c * 'd) map) x:
hmap_peq m0 m1 =>
pi3_2 (oget m0.[x]) = pi3_2 (oget m1.[x]).
proof.
move=> hmap_peq; cut:= hmap_peq x.
by case (m0.[x])=> //=; case (m1.[x])=> //=; smt.
qed.
(** Zeroth Transition:
We rewrite PSS into an adversary against Gen with G and a trivial split oracle H0. *)
(* More or less Coron's Game0 *)
local module H0: SplitOracle = {
proc init(ks:pkey*skey): unit = {
Hmap.init(ks);
}
proc o(c:caller,m:message,r:salt):htag option = {
var w;
w = $htag;
if (!mem (m,r) (dom Hmap.m))
Hmap.m.[(m,r)] = (w,c,2^k - 1);
return omap pi3_1 Hmap.m.[(m,r)];
}
proc v(m:message,r:salt):htag = {
var w;
w = $htag;
if (mem (m,r) (dom Hmap.m))
w = pi3_1 (oget Hmap.m.[(m,r)]);
return w;
}
}.
local module Game0 = Gen(GAdv,H0,G).
local equiv PSS96_Game0_H: H.o ~ H0.o:
x{1} = (m,r){2} /\ hmap_preq H.m{1} Hmap.m{2} ==> res{2} = Some res{1} /\ hmap_preq H.m{1} Hmap.m{2}.
proof.
proc; inline H0.o.
case ((mem x (dom Ht.RO.m)){1}).
rcondf{1} 2; first by progress; rnd.
rcondf{2} 2; first by progress; rnd; skip; progress; rewrite -(hmap_preq_dom Ht.RO.m{m}).
conseq (_: _ ==> hmap_preq H.m{1} Hmap.m{2}).
progress.
rewrite H; cut: mem (m,r){2} (dom Hmap.m{2}) by rewrite -(hmap_preq_dom Ht.RO.m{1}).
by rewrite mem_dom; case (Hmap.m.[(m,r)]{2}).
by rnd.
rcondt{1} 2; first by progress ;rnd.
rcondt{2} 2; first by progress; rnd; skip; progress; rewrite -(hmap_preq_dom Ht.RO.m{m}).
conseq (_: _ ==> mem (m,r){2} (dom Hmap.m){2} /\ hmap_preq H.m{1} Hmap.m{2}).
progress.
by rewrite H2; cut:= H1; rewrite mem_dom; case (m_R.[(m,r)]{2}).
wp; rnd; skip; progress.
by rewrite dom_set mem_add; right.
rewrite /hmap_preq=> x; case ((m,r){2} = x)=> [<- | neq_mr_x].
by rewrite !get_set_eq.
by rewrite !get_set_neq 3:H.
qed.
local equiv PSS96_Game0_Hv: H.o ~ H0.v:
x{1} = (m,r){2} /\ hmap_preq H.m{1} Hmap.m{2} ==> ={res}.
proof. by proc; inline H0.o; wp; rnd; skip; progress; smt. qed.
local equiv PSS96_Game0_equiv:
UF_CMA(Wrap(PSS96(H,G)),Bounded_PSS_Adv(A,H,G)).main ~ Game0.main: ={glob A} ==> ={res}.
proof.
proc.
inline Gen(GAdv,H0,Gt.Lazy.RO).GA.main Wrap(PSS96(Ht.RO,Gt.Lazy.RO)).fresh
Wrap(PSS96(Ht.RO,Gt.Lazy.RO)).verify PSS96(Ht.RO,Gt.Lazy.RO).verify
UF_CMA(Wrap(PSS96(Ht.RO,Gt.Lazy.RO)),Bounded_PSS_Adv(A,Ht.RO,Gt.Lazy.RO)).A.forge.
seq 8 6: (={glob G, m, s} /\
hmap_preq H.m{1} Hmap.m{2} /\
Wrap.qs{1} = Mem.qs{2} /\
Wrap.pk{1} = Mem.pk{2} /\
Wrap.sk{1} = Mem.sk{2} /\
Bounded_PSS_Adv.cH{1} = Mem.cH{2} /\
Bounded_PSS_Adv.cG{1} = Mem.cG{2} /\
Bounded_PSS_Adv.cS{1} = Mem.cS{2}).
wp; call (_: ={glob G} /\
hmap_preq H.m{1} Hmap.m{2} /\
Wrap.qs{1} = Mem.qs{2} /\
Wrap.pk{1} = Mem.pk{2} /\
Wrap.sk{1} = Mem.sk{2} /\
Bounded_PSS_Adv.cH{1} = Mem.cH{2} /\
Bounded_PSS_Adv.cG{1} = Mem.cG{2} /\
Bounded_PSS_Adv.cS{1} = Mem.cS{2}).
(* sign *)
proc; inline Wrap(PSS96(Ht.RO,Gt.Lazy.RO)).sign
PSS96(Ht.RO,Gt.Lazy.RO).sign.
sp; if=> //.
inline GAdv(H0,Gt.Lazy.RO).Hs.o.
swap{1} 4 -3.
seq 5 4: (={glob G, m} /\
m0{1} = m{2} /\
r0{1} = r{2} /\
hmap_preq H.m{1} Hmap.m{2} /\
Wrap.qs{1} = Mem.qs{2} /\
Wrap.pk{1} = Mem.pk{2} /\
Wrap.sk{1} = Mem.sk{2} /\
sk{1} = Wrap.sk{1} /\
wo{2} = Some w{1} /\
Bounded_PSS_Adv.cH{1} = Mem.cH{2} /\
Bounded_PSS_Adv.cG{1} = Mem.cG{2} /\
Bounded_PSS_Adv.cS{1} = Mem.cS{2}).
by wp; call PSS96_Game0_H; wp; rnd; wp.
rcondf{2} 1=> //.
by wp; call (_: ={glob G}); auto; smt.
(* G *)
by proc; sp; if=> //; wp; call (_: ={glob G}); auto; smt.
(* H *)
proc*.
inline Bounded_PSS_Adv(A,Ht.RO,Gt.Lazy.RO,Wrap(PSS96(Ht.RO,Gt.Lazy.RO))).Hc.o
GAdv(H0,Gt.Lazy.RO).Ha.o.
sp; if=> //; last by wp.
by wp; call PSS96_Game0_H; skip; progress; rewrite -pairS.
(* Initialization code *)
inline Wrap(PSS96(Ht.RO,Gt.Lazy.RO)).init PSS96(Ht.RO,Gt.Lazy.RO).keygen PSS96(Ht.RO,Gt.Lazy.RO).init
Mem.init Ht.RO.init H0.init Hmap.init Hmem.init.
swap{1} 4 -3.
swap{1} 3 -1.
wp; rnd{2} True; wp.
call (Gt.Lazy.RO_init_eq).
rnd.
skip; progress.
by apply challengeL; rewrite /valid_pkey; exists pk2skL.`2; smt.
smt.
sp; if{1}; first last.
by inline *; auto; progress; smt.
wp; call PSS96_Game0_Hv=> //=.
wp; call (_: ={glob G}); first by sim.
wp; skip; progress.
by rewrite xorwC.
by rewrite (eq_sym result_R0) xorwC eq_iff; smt.
qed.
local lemma PSS96_Game0 &m:
Pr[UF_CMA(Wrap(PSS96(H,G)),Bounded_PSS_Adv(A,H,G)).main() @ &m: res] = Pr[Game0.main() @ &m: res]
by byequiv PSS96_Game0_equiv.
(*** Game1: - Eliminate collisions on calls to H and G
made by the signing oracles.
- Anticipate calls to G on H's output and
returns both results to signing oracles.
- Split G between adversary queries and
queries made by signing oracles. *)
(** We first define new global state and wrappers *)
local module Gmap = {
var m:(htag,gtag * caller) map
proc init(): unit = {
m = FMap.empty;
}
}.
module type SplitOracle1 = {
proc init(ks:pkey * skey):unit { }
proc o(c:caller,m:message,r:salt):(htag * gtag) option
proc v(m:message,r:salt):htag
}.
module type Gadv1 (H:SplitOracle1, G:Gt.Types.ARO) = {
proc main (ks:pkey * skey): bool {H.o G.o H.v}
}.
local module Gen1 (Gadv:Gadv1, H:SplitOracle1, G:Gt.Types.Oracle) = {
module GA = Gadv(H,G)
proc main () : bool = {
var keys, b;
keys = $keypairs;
G.init();
H.init(keys);
b = GA.main(keys);
return b;
}
}.
local module GAdv1(H:SplitOracle1, G:Gt.Types.ARO) = {
(* Wrapping a split oracle for direct use by the adversary *)
module Ha = {
proc o(m:message * salt): htag = {
var r = None;
if (Mem.cH < qH) {
r = H.o(Adv,fst m,snd m);
Mem.cH = Mem.cH + 1;
}
return oget (omap fst r);
}
}
(* Wrapping a split oracle for use by the signing oracle *)
module Hs = {
proc o(m:message * salt): (htag*gtag) option = {
var r;
r = H.o(Sig,fst m,snd m);
return r;
}
}
(* Counting queries to G *)
module Ga = {
proc o(w:htag): gtag = {
var r = witness;
if (Mem.cG < qG) {
r = G.o(w);
Mem.cG = Mem.cG + 1;
}
return r;
}
}
(* Signing oracle *)
module S = {
proc sign(m:message): signature = {
var r, wo, w, g, rs, em;
var s = witness;
if (Mem.cS < qS) {
r = $salt;
wo = Hs.o(m,r);
if (wo = None)
s = witness;
else {
(w,g) = oget wo;
rs = g ^ (to_gtag (from_salt r || zeros (kg - k0)));
em = to_signature (zeros 1 || (from_htag w) || (from_gtag rs));
s = i2osp (rsas Mem.sk (os2ip em));
Mem.qs = add (m,s) Mem.qs;
}
Mem.cS = Mem.cS + 1;
}
return s;
}
proc fresh(m:message, s:signature): bool = {
return !mem (m,s) Mem.qs;
}
}
module A = A(Ha, Ga, S)
proc main (ks:pkey*skey): bool = {
var m, s;
var y, w, st, g, rs, r, w';
Mem.init(ks);
(m,s) = A.forge(Mem.pk);
y = from_signature (i2osp (rsap Mem.pk (os2ip s)));
w = to_htag (sub y 1 kh);
st = to_gtag (sub y (1 + kh) kg);
g = G.o(w);
rs = from_gtag (st ^ g);
r = to_salt (sub rs 0 k0);
w' = H.v(m,r);
return sub y 0 1 = zeros 1 /\ w = w' /\ sub rs k0 (kg - k0) = zeros (kg - k0) /\
0 <= os2ip s < p_n Mem.pk /\ !mem (m,s) Mem.qs;
}
}.
local lemma GAdv1Ha_o_ll (H <: SplitOracle1 {GAdv}) (G <: Gt.Types.ARO {GAdv}):
islossless H.o => islossless GAdv1(H,G).Ha.o.
proof. by move=> H_o_ll; proc; sp; if=> //; wp; call H_o_ll. qed.
local lemma GAdv1Hs_o_ll (H <: SplitOracle1 {GAdv}) (G <: Gt.Types.ARO {GAdv}):
islossless H.o => islossless GAdv1(H,G).Hs.o.
proof. by move=> H_o_ll; proc; call H_o_ll. qed.
local lemma GAdv1Ga_o_ll (H <: SplitOracle1 {GAdv}) (G <: Gt.Types.ARO {GAdv}):
islossless G.o => islossless GAdv1(H,G).Ga.o.
proof. by move=> G_o_ll; proc; sp; if=> //; wp; call G_o_ll. qed.
local lemma GAdv1_main_ll (H <: SplitOracle1 {GAdv}) (G <: Gt.Types.ARO {GAdv}):
islossless H.o => islossless G.o => islossless H.v => islossless GAdv1(H, G).main.
proof.
move=> H_o_ll G_o_ll H_v_ll; proc.
call H_v_ll.
wp; call G_o_ll.
wp; call (A_forge_ll (<:GAdv1(H,G).Ha) (<:GAdv1(H,G).Ga) (<:GAdv1(H,G).S) _ _ _).
by apply (GAdv1Ha_o_ll H G _)=> //.
by apply (GAdv1Ga_o_ll H G _)=> //.
proc; sp; if=> //; seq 2: true=> //.
by call (GAdv1Hs_o_ll H G _)=> //; rnd; skip; smt.
if; first by wp.
by wp.
by call (_: true)=> //; wp.
qed.
(** We can now define Game1 *)
local module G1 = {
proc init = Gmap.init
proc o(w:htag): gtag = {
var g;
g = $gtag;
if (!mem w (dom Gmap.m)) Gmap.m.[w] = (g,Adv);
return fst (oget Gmap.m.[w]);
}
}.
local module H1: SplitOracle1 = {
proc init = H0.init
proc o(c:caller,m:message,r:salt): (htag *gtag) option = {
var w, st, ho;
w = $htag;
st = $gtag;
st = st ^ (GTag.from_bits (from_salt r || zeros (kg - k0)));
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,2^k - 1);
Gmap.m.[w] = (st,c);
}
ho = Some(w,st);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
return ho;
}
proc v = H0.v
}.
local module Game1 = Gen1(GAdv1,H1,G1).
(** Game0.1: Anticipate calls to G in H *)
local module H0'1:SplitOracle = {
proc init = H0.init
proc o(c:caller,m:message,r:salt): htag option = {
var w, st;
w = $htag;
if (!mem (m,r) (dom Hmap.m)) {
Hmap.m.[(m,r)] = (w,c,2^k - 1);
st = G.o(w);
}
return omap pi3_1 Hmap.m.[(m,r)];
}
proc v = H0.v
}.
local module Game0'1 = Gen(GAdv,H0'1,G).
(* We refactor PSS into a distinguisher for random oracles *)
(* - Game0_D0 refactors *
* - D0_D0e applies the generic eager transformation (lazy to eager) *
* - D0e_D1e adds the call to G in H (in the eager world) *
* - D1e_D1 applies the generic eager transformation (eager to lazy) *
* - D1_Game1'1 defactors *)
(* Game0_1'1 combines all 5 steps into a single abstract equiv *)
module type PSplitOracle (G:Gt.Types.ARO) = {
proc init(ks:pkey * skey): unit
proc o(c:caller,m:message,r:salt): htag option {G.o}
proc v(m:message,r:salt): htag {}
}.
local module H0e (G:Gt.Types.ARO): PSplitOracle(G) = {
proc init(ks:pkey*skey): unit = {
Hmap.init(ks);
}
proc o(c:caller,m:message,r:salt):htag option = {
var w;
w = $htag;
if (!mem (m,r) (dom Hmap.m))
Hmap.m.[(m,r)] = (w,c,2^k - 1);
return omap pi3_1 Hmap.m.[(m,r)];
}
proc v(m:message,r:salt):htag = {
var w;
w = $htag;
if (mem (m,r) (dom Hmap.m))
w = pi3_1 (oget Hmap.m.[(m,r)]);
return w;
}
}.
local module H0'1e (G:Gt.Types.ARO): PSplitOracle(G) = {
proc init = H0.init
proc o(c:caller,m:message,r:salt): htag option = {
var w, st;
w = $htag;
if (!mem (m,r) (dom Hmap.m)) {
Hmap.m.[(m,r)] = (w,c,2^k - 1);
st = G.o(w);
}
return omap pi3_1 Hmap.m.[(m,r)];
}
proc v = H0.v
}.
local module D (Ga:Gadv, H:PSplitOracle, G:Gt.Types.ARO) = {
module H = H(G)
module Ga = Ga(H,G)
proc distinguish(): bool = {
var b:bool;
var ks:pkey * skey;
ks = $keypairs;
H.init(ks);
b = Ga.main(ks);
return b;
}
}.
local equiv Game0_D0 (Ga <: Gadv {G,Hmap}):
Gen(Ga,H0,G).main ~ Gt.Eager.Types.IND(G,D(Ga,H0e)).main: ={glob Ga} ==> ={res}.
proof.
proc.
inline Gt.Eager.Types.IND(Gt.Lazy.RO,D(Ga,H0e)).D.distinguish; swap{1} 1 1.
by sim.
qed.
local equiv D0_D0e (Ga <: Gadv {G,Ge,Hmap}):
Gt.Eager.Types.IND(G,D(Ga,H0e)).main ~ Gt.Eager.Types.IND(Ge,D(Ga,H0e)).main: ={glob D(Ga,H0e)} ==> ={res}.
proof. by apply (Gt.eagerRO (D(Ga,H0e)) _ _); [apply htag_finite | apply gtagL]. qed.
local equiv D0e_D1e (Ga <: Gadv {Ge,Hmap}):
Gt.Eager.Types.IND(Ge,D(Ga,H0e)).main ~ Gt.Eager.Types.IND(Ge,D(Ga,H0'1e)).main: ={glob D(Ga,H0e)} ==> ={res}.
proof.
proc; call (_: ={glob Gt.Eager.RO, glob D(Ga,H0e)} /\ forall x, mem x (dom Ge.m{1})).
call (_: ={glob Gt.Eager.RO, glob Hmap} /\ forall x, mem x (dom Ge.m{1})).
(* H *)
proc; case ((mem (m,r) (dom Hmap.m)){2}).
rcondf{1} 2; first by progress; rnd.
rcondf{2} 2; first by progress; rnd.
by rnd; skip; smt.
rcondt{1} 2; first by progress; rnd.
rcondt{2} 2; first by progress; rnd.
by inline Gt.Eager.RO.o; wp; rnd; skip; smt.
(* G *)
by proc; auto.
(* Hv *)
by conseq (_: ={glob Hmap, m, r} ==> ={glob Hmap, res})=> //; sim.
call (_: ={ks} ==> ={glob Hmap}); first by sim.
by rnd; skip; smt.
call (_: true ==> ={glob Ge} /\ forall x, mem x (dom Ge.m){1}).
by conseq (Gt.Eager.RO_init_eq _) (Gt.Eager.RO_init_full _); last 2 apply htag_finite.
by skip; smt.
qed.
local equiv D0'1e_D0'1 (Ga <: Gadv {G,Ge}):
Gt.Eager.Types.IND(Ge,D(Ga,H0'1e)).main ~ Gt.Eager.Types.IND(G,D(Ga,H0'1e)).main: ={glob D(Ga,H0'1e)} ==> ={res}.
proof.
symmetry.
conseq (_: ={glob D(Ga,H0'1e)} ==> ={res}).
done.
smt. (* should be trivial but substitution sucks *)
apply (Gt.eagerRO (D(Ga,H0'1e)) _ _).
by apply htag_finite.
by apply gtagL.
qed.
local equiv D0'1_Game0'1 (Ga <: Gadv {G,Hmap}):
Gt.Eager.Types.IND(G,D(Ga,H0'1e)).main ~ Gen(Ga,H0'1,G).main: ={glob Ga} ==> ={res}.
proof.
proc.
inline Gt.Eager.Types.IND(Gt.Lazy.RO,D(Ga,H0'1e)).D.distinguish; swap{1} 1 1.
by sim.
qed.
local equiv Game0_0'1_abstract (Ga <: Gadv {G,Ge,Hmap}):
Gen(Ga,H0,G).main ~ Gen(Ga,H0'1,G).main: ={glob Ga} ==> ={res}.
proof.
bypr (res{1}) (res{2})=> // &1 &2 a eq_Ga.
apply (eq_trans _ Pr[Gt.Eager.Types.IND(G,D(Ga,H0e)).main() @ &1: a = res]);
first by byequiv (Game0_D0 Ga).
apply (eq_trans _ Pr[Gt.Eager.Types.IND(Ge,D(Ga,H0e)).main() @ &1: a = res]);
first by byequiv (D0_D0e Ga).
apply (eq_trans _ Pr[Gt.Eager.Types.IND(Ge,D(Ga,H0'1e)).main() @ &1: a = res]);
first by byequiv (D0e_D1e Ga).
apply (eq_trans _ Pr[Gt.Eager.Types.IND(G,D(Ga,H0'1e)).main() @ &1: a = res]);
first by byequiv (D0'1e_D0'1 Ga).
by byequiv (D0'1_Game0'1 Ga).
qed.
local lemma Game0_0'1 &m:
Pr[Game0.main() @ &m: res] = Pr[Game0'1.main() @ &m: res].
proof.
byequiv (_: ={glob GAdv} ==> ={res})=> //.
by apply (Game0_0'1_abstract GAdv).
qed.
(** H returns both w and st, unless called directly by the adversary *)
local module HG0'1:SplitOracle1 = {
proc init = H0.init
proc o(c:caller,m:message,r:salt): (htag *gtag) option = {
var w, st;
w = $htag;
if (!mem (m,r) (dom Hmap.m)) {
Hmap.m.[(m,r)] = (w,c,2^k - 1);
st = G.o(w);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
if (c = Adv) st = witness;
else st = G.o(w);
}
return Some (w,st);
}
proc v = H0.v
}.
local module GameG0'1 = Gen1(GAdv1,HG0'1,G).
local lemma Game0'1_G0'1 &m: Pr[Game0'1.main() @ &m: res] = Pr[GameG0'1.main() @ &m: res].
proof.
byequiv (_: ={glob A} ==> ={res})=> //; proc.
seq 3 3: (={glob A, glob Hmap, glob G, keys} /\
Hmap.m{1} = FMap.empty /\
G.m{1} = FMap.empty);
first by inline*; auto.
call (_: ={glob A, glob Hmap, glob G, ks} /\
Hmap.m{1} = FMap.empty /\
G.m{1} = FMap.empty ==>
={res})=> //; proc.
conseq (_: _ ==> ={y, w, w', rs, m, s, Mem.pk, Mem.qs})=> //.
sim.
seq 1 1: (={glob A, glob Hmap, glob G, glob Mem, ks} /\
Hmap.m{1} = FMap.empty /\
G.m{1} = FMap.empty);
first by inline*; auto.
call (_: ={glob Hmap, glob G, glob Mem} /\
(forall x,
mem x (dom Hmap.m{2}) =>
mem (pi3_1 (oget Hmap.m.[x])){2} (dom G.m{2}))).
(* sign *)
proc; sp; if=> //.
inline *.
seq 1 1: (={glob Hmap, glob G, glob Mem, m, r, s} /\
(forall x,
mem x (dom Hmap.m{2}) =>
mem (pi3_1 (oget Hmap.m.[x])){2} (dom G.m{2})));
first by rnd.
rcondf{1} 9.
progress; case (mem (m,r) (dom Hmap.m)).
by rcondf 6; auto; progress; smt.
by rcondt 6; auto; progress; smt.
rcondf{2} 9.
progress; case (mem (m,r) (dom Hmap.m)).
rcondf 6; first by auto.
by rcondf 7; auto.
by rcondt 6; auto.
case ((mem (m,r) (dom Hmap.m)){2}).
rcondf{1} 6; first by auto.
rcondf{2} 6; first by auto.
rcondf{2} 7; first by auto.
by auto; progress; smt.
rcondt{1} 6; first by auto.
rcondt{2} 6; first by auto.
rcondf{1} 16.
auto; progress.
by rewrite -pairS get_set_eq oget_omap_some // mem_dom /oget /pi3_1 /= get_set_eq.
by rewrite -pairS get_set_eq oget_omap_some.
wp; rnd{1} True; auto; progress.
smt.
by rewrite -pairS get_set_eq /oget /pi3_1 /= get_set_eq /oget /oget.
by rewrite -pairS get_set_eq /oget /pi3_1 /= get_set_eq /oget /oget.
move: H8; rewrite -pairS=> H10; case ((m,r){2} = x1).
by move=> <-; rewrite get_set_eq /oget /pi3_1 /= mem_dom get_set_eq.
move=> neq_mr_x1; rewrite get_set_neq // mem_dom get_set_neq.
by cut:= H10; rewrite mem_dom get_set_neq //; smt.
rewrite -mem_dom; apply H.
by cut:= H10; rewrite mem_dom get_set_neq //; smt.
smt.
by rewrite -pairS !get_set_eq /oget /pi3_1.
by rewrite -pairS !get_set_eq /oget /pi3_1.
move: H8; rewrite -pairS=> H10; case ((m,r){2} = x1).
by move=> <-; rewrite get_set_eq /oget /pi3_1.
move=> neq_mr_x1; rewrite get_set_neq //.
apply H.
by cut:= H10; rewrite mem_dom get_set_neq //; smt.
(* Ga *)
by proc; inline *; sp; if=> //; auto; progress; smt.
(* Ha *)
proc; sp; if=> //.
inline H0'1.o HG0'1.o; case ((mem m (dom Hmap.m)){1}).
rcondf{1} 5; first by auto; smt.
rcondf{2} 5; first by auto; smt.
by rcondt{2} 6; auto.
rcondt{1} 5; first by auto; smt.
rcondt{2} 5; first by auto; smt.
inline G.o; auto; progress.
by rewrite -pairS get_set_eq.
move: H7; rewrite -pairS=> H9; case (m{2} = x0).
by move=> <-; rewrite get_set_eq /oget /pi3_1 /= mem_dom get_set_eq.
move=> neq_m_x0; rewrite get_set_neq // mem_dom get_set_neq.
by cut:= H9; rewrite mem_dom get_set_neq //; smt.
rewrite -mem_dom; apply H.
by cut:= H9; rewrite mem_dom get_set_neq //; smt.
by rewrite -pairS get_set_eq.
move: H7; rewrite -pairS=> H7; case (m{2} = x0).
by move=> <-; rewrite get_set_eq.
move=> neq_m_x0; rewrite get_set_neq //; apply H.
by cut:= H7; rewrite mem_dom get_set_neq //; smt.
by skip; smt.
qed.
(** Game0'2: - Abort if H calls G on a non-fresh input,
with Pr[Game1'2: H1'2.badg] <= (qS + qF + qH) * (qS + qF + qH + qG)%r * 2^-kh
- Abort if one of the signing oracles queries H
on some non-fresh input despite freshly sampling r,
with Pr[Game1'2: H1'2.bad] <= (qS + qF) * (qS + qF + qH) * 2^-k0 *)
local module H0'2: SplitOracle1 = {
var badg, badh:bool
proc init(ks:pkey * skey): unit = {
Hmap.init(ks);
badg = false;
badh = false;
}
proc o(c:caller,m:message,r:salt): (htag *gtag) option = {
var w, st, ho;
w = $htag;
st = $gtag;
st = st ^ (GTag.from_bits (from_salt r || zeros (kg - k0)));
badg = badg \/ mem w (dom Gmap.m);
badh = badh \/ (mem (m,r) (dom Hmap.m) /\ !c = Adv);
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,2^k - 1);
Gmap.m.[w] = (st,c);
}
ho = Some(w,st);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
return ho;
}
proc v = H0.v
}.
local module Game0'2 = Gen1(GAdv1,H0'2,G1).
(* proving near-equivalence of ROM programming *)
local equiv GameG0'1_0'2_H: HG0'1.o ~ H0'2.o:
!H0'2.badg{2} /\ !H0'2.badh{2} /\
={glob Hmap, c, m, r} /\ G.m{1} = FMap.map fst Gmap.m{2} ==>
!(H0'2.badg{2} \/ H0'2.badh{2}) =>
( ={glob Hmap, res} /\ G.m{1} = FMap.map fst Gmap.m{2}).
proof.
proc.
swap{2} [4..5] -2.
seq 1 3 : (={glob Hmap, c, m, r, w} /\ G.m{1} = FMap.map fst Gmap.m{2} /\
(H0'2.badg = mem w (dom Gmap.m)){2} /\
(H0'2.badh = (mem (m,r) (dom Hmap.m) /\ ! c = Adv)){2});
first by auto; smt.
case (H0'2.badg{2} \/ H0'2.badh{2}).
conseq (_ : _ ==> true)=> //.
by wp; rnd{2}; inline G.o; if{1}; wp; [ | sp; if{1}]; auto; progress; expect 3 smt.
case ((mem (m,r) (dom Hmap.m)){1}).
rcondf{1} 1=> //; rcondf{2} 3; first by auto; smt.
sp; elim * => wL; if{1}; first by auto; smt.
by inline G.o; auto; smt.
rcondt{1} 1=> //; rcondt{2} 3; first by auto; smt.
inline *; swap{1} 3 -2.
case (mem w{2} (dom Gmap.m{2})); first by conseq (_: _ ==> true); auto; smt.
rcondt{2} 3; first by auto; smt.
rcondt{1} 4.
auto;progress.
move: H0; rewrite !mem_dom get_map; smt.
wp; rnd ((^) (GTag.from_bits (from_salt r || zeros (kg - k0)))){2}; auto; progress; try algebra.
by apply gtagU; apply gtagF.
by apply gtagF.
by rewrite get_set_eq /oget /=; congr; split=> //; algebra.
by rewrite map_set /fst /=; congr; algebra.
qed.
local lemma GameG0'1_0'2_abstract (Ga <: Gadv1 {G, HG0'1, H0'2}):
(forall (H <: SplitOracle1 {Ga}) (G <: Gt.Types.ARO {Ga}),
islossless H.o => islossless G.o => islossless H.v => islossless Ga(H,G).main) =>
equiv [Gen1(Ga,HG0'1,G).main ~ Gen1(Ga,H0'2,G1).main:
={glob Ga} ==> !(H0'2.badg \/ H0'2.badh){2}=> ={res}].
proof.
move=> Ga_main_ll; proc.
call (_: (H0'2.badg \/ H0'2.badh), ={glob Hmap} /\ G.m{1} = FMap.map fst Gmap.m{2}).
(* H *)
by conseq GameG0'1_0'2_H; smt.
progress; proc; seq 1: true=> //;
first by auto; smt.
if=> //.
by call (Gt.Lazy.RO_o_ll _); [apply gtagL | auto].
sp; if; first by auto.
by call (Gt.Lazy.RO_o_ll _); first apply gtagL.
by progress; proc; auto; smt.
(* G *)
conseq (_ : _ ==> ={res} /\ G.m{1} = map fst Gmap.m{2})=> //.
proc.
seq 1 1 : (x{1} = w{2} /\ y{1} = g{2} /\ G.m{1} = map fst Gmap.m{2});first by auto.
if.
by progress [-split]; rewrite !mem_dom get_map; smt.
by auto; smt.
by auto; smt.
by move=> _ _; conseq (Gt.Lazy.RO_o_ll _); apply gtagL.
by move=> _ /=; proc; auto; smt.
(* Hv *)
by proc; auto.
by progress; proc; auto; smt.
by progress; proc; auto; smt.
by inline *; auto; smt.
qed.
(* end proof *)
(* computing the probability of badg *)
local module H0'2'badg: SplitOracle1 = {
var cHs:int
proc init(ks:pkey * skey): unit = {
Hmap.init(ks);
H0'2.badg = false;
cHs = 0;
}
proc o(c:caller,m:message,r:salt): (htag *gtag) option = {
var w, st, ho;
if (cHs < qH + qS /\ card (dom Gmap.m) < qH + qG + qS) {
w = $htag;
st = $gtag;
st = st ^ (GTag.from_bits (from_salt r || zeros (kg - k0)));
H0'2.badg = H0'2.badg \/ mem w (dom Gmap.m);
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,2^k - 1);
Gmap.m.[w] = (st,c);
}
ho = Some(w,st);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
cHs = cHs + 1;
}
return ho;
}
proc v = H0.v
}.
local module Game0'2'badg = Gen1(GAdv1, H0'2'badg, G1).
local equiv H0'2_H0'2'badg : H0'2.o ~ H0'2'badg.o :
={c, m, r, glob Hmap, glob Gmap, glob Mem, H0'2.badg} /\
H0'2'badg.cHs{2} = Mem.cH{1} + Mem.cS{1} /\
Mem.cG{1} <= qG /\ Mem.cH{1} + Mem.cS{1} < qH + qS /\
card (dom Gmap.m{1}) <= Mem.cG{1} + Mem.cH{1} + Mem.cS{1} ==>
={res, glob Hmap, glob Gmap, glob Mem, H0'2.badg} /\
H0'2'badg.cHs{2} = Mem.cH{1} + Mem.cS{1} + 1 /\
card (dom Gmap.m{1}) <= Mem.cG{1} + Mem.cH{1} + Mem.cS{1} + 1.
proof.
proc; rcondt{2} 1; first by auto; smt.
seq 5 4: (={w, st, c, m, r, glob Hmap, glob Gmap, glob Mem, H0'2.badg} /\
H0'2'badg.cHs{2} = Mem.cH{1} + Mem.cS{1} /\
Mem.cG{1} <= qG /\ Mem.cH{1} + Mem.cS{1} < qH + qS /\
card (dom Gmap.m{1}) <= Mem.cG{1} + Mem.cH{1} + Mem.cS{1});
first by auto.
by if=> //; auto; progress; expect 3 smt.
qed.
local lemma Game0'2_0'2'badg &m:
Pr[Game0'2.main() @ &m: H0'2.badg] = Pr[Game0'2'badg.main() @ &m: H0'2.badg /\ H0'2'badg.cHs <= qS + qH].
proof.
byequiv (_: ={glob GAdv} ==> ={H0'2.badg} /\ H0'2'badg.cHs{2} <= qS + qH)=> //.
proc.
inline Gen1(GAdv1, H0'2, G1).GA.main Gen1(GAdv1, H0'2'badg, G1).GA.main; auto.
call (_: true ==> true); first by proc; auto.
wp; call (_: true ==> true); first by proc; auto.
wp.
call (_: ={glob Hmap, glob Gmap, glob Mem, H0'2.badg} /\
H0'2'badg.cHs{2} = Mem.cH{1} + Mem.cS{1} /\
card (dom Gmap.m){1} <= Mem.cG{1} + Mem.cH{1} + Mem.cS{1} /\
Mem.cG{1} <= qG /\
Mem.cH{1} <= qH /\
Mem.cS{1} <= qS).
(* sign *)
proc; sp=> //; if=> //.
seq 2 2: (={glob Hmap, glob Gmap, glob Mem, H0'2.badg, wo, s, r, m} /\
H0'2'badg.cHs{2} = Mem.cH{1} + Mem.cS{1} + 1 /\
card (dom Gmap.m){1} <= Mem.cG{1} + Mem.cH{1} + Mem.cS{1} + 1 /\
Mem.cG{1} <= qG /\
Mem.cH{1} <= qH /\
Mem.cS{1} < qS);
last by if; auto; smt.
inline GAdv1(H0'2, G1).Hs.o GAdv1(H0'2'badg, G1).Hs.o; wp.
by call H0'2_H0'2'badg; auto; smt.
(* Ga *)
by proc; inline *; sp; if=> //; auto; smt.
(* Ha *)
by proc; sp; if=> //; wp; call H0'2_H0'2'badg; auto; smt.
by inline *; auto; smt.
qed.
local lemma Game0'2'badg &m:
Pr[Game0'2'badg.main() @ &m: H0'2.badg /\ H0'2'badg.cHs <= qS + qH]
<= (qS + qH)%r * (qS + qH + qG - 1)%r / (2^kh)%r.
proof.
fel 3 (H0'2'badg.cHs)
(fun x, (qS + qH + qG - 1)%r / (2^kh)%r)
(qS + qH)
(H0'2.badg)
[H0'2'badg.o: (H0'2'badg.cHs < qS + qH /\ card (dom Gmap.m) < qH + qG + qS)] => //.
(*-*) rewrite /int_sum (Monoid.Mrplus.NatMul.sum_const ((qS + qH + qG - 1)%r /(2^kh)%r)) //.
rewrite /intval card_interval_max (_: qS + qH - 1 - 0 + 1 = qS + qH); first smt.
rewrite /max (_: qS + qH < 0 = false) /=; first smt.
by rewrite /Monoid.Mrplus.NatMul.( * ); smt.
(*-*) by inline *; auto.
(*-*) proc.
cut bnd_pos: 0%r <= (qS + qH + qG - 1)%r / (2^kh)%r.
cut leq: 0%r <= (qS + qH + qG - 1)%r by smt.
cut lt: 0%r < (2^kh)%r by smt.
cut H: forall (x y z:real), x <= y => 0%r < z => x / z <= y / z by smt.
cut ->: 0%r = 0%r / (2^kh)%r by smt.
smt.
if; last by hoare.
wp.
seq 1: (mem w (dom Gmap.m)) ((qS + qH + qG - 1)%r / (2 ^ kh)%r) 1%r _ 0%r (!H0'2.badg) => //;
first by auto.
rnd; skip; progress.
rewrite -/(cpMem _) (mu_cpMem _ _ (1%r / (2^kh)%r)); first smt.
cut ->: forall x, x * (1%r / (2^kh)%r) = x / (2^kh)%r by smt.
by apply (_: forall (x y z:real), x <= y => 0%r < z => x / z <= y / z); smt.
(*-*) by hoare; conseq (_ : _ ==> true) => //; smt.
(*-*) by progress; proc; rcondt 1; auto; smt.
(*-*) by progress; proc; rcondf 1; auto; smt.
qed.
(* end computation *)
(* computing the probability Pr[Game0'2.main() @ &m: H0'2.badh] *)
local module Game0'2'badh = {
var cHs:int
module H = {
proc init = H0'2.init
proc o(c:caller,m:message,r:salt): (htag *gtag) option = {
var w, st, ho;
H0'2.badh = H0'2.badh \/ (mem (m,r) (dom Hmap.m) /\ !c = Adv);
w = $htag;
st = $gtag;
st = st ^ (GTag.from_bits (from_salt r || zeros (kg - k0)));
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,2^k - 1);
Gmap.m.[w] = (st,c);
}
ho = Some(w,st);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
return ho;
}
proc v = H0.v
}
module Hss = {
proc o (c:caller,m:message): (htag * gtag * salt) option = {
var r;
var wo = None;
var ho = None;
if (cHs < qS /\ card (dom Hmap.m) < qH + qS) {
r = $salt;
wo = H.o(c,m,r);
ho = omap (fun x, let (a,b) = x in (a,b,r)) wo;
cHs = cHs + 1;
}
return ho;
}
}
module Ha = {
proc o (mr:message * salt): htag = {
var m, r, st;
var w = witness;
if (Mem.cH < qH) {
(m,r) = mr;
w = $htag;
st = $gtag;
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,Adv,2^k - 1);
Gmap.m.[w] = (st ^ (GTag.from_bits (from_salt r || zeros (kg - k0))), Adv);
}
} else
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
Mem.cH = Mem.cH + 1;
}
return w;
}
}
module Ga = {
proc o (w:htag): gtag = {
var g = witness;
if (Mem.cG < qG) {
g = G1.o(w);
Mem.cG = Mem.cG + 1;
}
return g;
}
}
module S = {
proc sign(m:message): signature = {
var r, wo, w, g, rs, em;
var s = witness;
if (Mem.cS < qS) {
wo = Hss.o(Sig,m);
if (wo = None)
s = witness;
else {
(w,g,r) = oget wo;
rs = g ^ (to_gtag (from_salt r || zeros (kg - k0)));
em = to_signature (zeros 1 || (from_htag w) || (from_gtag rs));
s = i2osp (rsas Mem.sk (os2ip em));
Mem.qs = add (m,s) Mem.qs;
}
Mem.cS = Mem.cS + 1;
}
return s;
}
proc fresh(m:message, s:signature): bool = {
return !mem (m,s) Mem.qs;
}
}
module A = A(Ha,Ga,S)
proc main(): unit = {
var ks, m, s;
ks = $keypairs;
G1.init();
H0'2.init(ks);
Mem.init(ks);
cHs = 0;
(m, s) = A.forge(Mem.pk);
}
}.
local lemma Game0'2_0'2'badh &m:
Pr[Game0'2.main() @ &m: H0'2.badh] = Pr[Game0'2'badh.main() @ &m: H0'2.badh /\ Game0'2'badh.cHs <= qS].
proof.
byequiv (_: ={glob GAdv} ==> ={H0'2.badh} /\ Game0'2'badh.cHs{2} <= qS)=> //.
proc; inline Gen1(GAdv1,H0'2,G1).GA.main.
wp; call{1} (_: true ==> true); first by proc; auto; smt.
wp; call{1} (_: true ==> true); first by proc; auto; smt.
wp.
call (_: ={glob Hmap, glob Gmap, glob Mem, H0'2.badh} /\
Game0'2'badh.cHs{2} = Mem.cS{1} /\
card (dom Hmap.m){1} <= Mem.cH{1} + Mem.cS{1} /\
Mem.cG{1} <= qG /\
Mem.cH{1} <= qH /\
Mem.cS{1} <= qS).
(* sign *)
proc; sp=> //; if=> //.
seq 2 1: (={glob Hmap, glob Gmap, glob Mem, H0'2.badh, s, m} /\
wo{2} = omap (fun x, let (a,b) = x in (a,b,r{1})) wo{1} /\
Game0'2'badh.cHs{2} = Mem.cS{1} + 1 /\
card (dom Hmap.m){1} <= Mem.cH{1} + Mem.cS{1} + 1 /\
Mem.cG{1} <= qG /\
Mem.cH{1} <= qH /\
Mem.cS{1} < qS).
inline GAdv1(H0'2,G1).Hs.o Game0'2'badh.Hss.o; wp.
rcondt{2} 5; first by auto; smt.
wp; call (_: ={glob Hmap, glob Gmap, glob Mem, H0'2.badh, c, m, r} /\
c{2} = Sig /\
Game0'2'badh.cHs{2} = Mem.cS{1} /\
card (dom Hmap.m){1} <= Mem.cH{1} + Mem.cS{1} /\
Mem.cG{1} <= qG /\
Mem.cH{1} <= qH /\
Mem.cS{1} < qS ==>
={glob Hmap, glob Gmap, Mem.cG, H0'2.badh, res} /\
Game0'2'badh.cHs{2} = Mem.cS{1} /\
card (dom Hmap.m){1} <= Mem.cH{1} + Game0'2'badh.cHs{2} + 1 /\
Mem.cS{1} < qS).
by proc; auto; progress; smt.
by auto; progress; smt.
by if; auto; progress; smt.
(* Ga *)
proc; sp; if=> //.
wp; call (_: ={glob Gmap, glob Mem, w} ==>
={glob Gmap, glob Mem, res}).
by proc; auto; smt.
by skip; smt.
(* Ha *)
by proc; inline *; sp; if=> //; auto; progress; expect 22 smt.
by inline *; auto; smt.
qed.
local lemma Game0'2'badh &m:
Pr[Game0'2'badh.main() @ &m: H0'2.badh /\ Game0'2'badh.cHs <= qS]
<= qS%r * (qS + qH)%r / (2^k0)%r.
proof.
fel 5 (Game0'2'badh.cHs)
(fun x, (qS + qH)%r / (2^k0)%r)
qS
(H0'2.badh)
[Game0'2'badh.Hss.o: (Game0'2'badh.cHs < qS /\ card (dom Hmap.m) < qH + qS)].
(*-*) rewrite /int_sum (Monoid.Mrplus.NatMul.sum_const ((qS + qH)%r / (2^k0)%r)) //.
rewrite /intval card_interval_max (_: qS - 1 - 0 + 1 = qS); first smt.
rewrite /max (_: qS < 0 = false) /=; first smt.
by rewrite /Monoid.Mrplus.NatMul.( * ); smt.
(*-*) smt.
(*-*) inline Mem.init.
by wp; call (_: true ==> !H0'2.badh);
first proc; wp; call (_: true).
(*-*) proc.
cut H: forall (x y z:real), x <= y => 0%r < z => x / z <= y / z by smt.
cut bnd1_pos: 0%r <= 1%r / (2^k0)%r.
cut leq: 0%r <= 1%r by smt.
cut lt: 0%r < (2^k0)%r by smt.
cut ->: 0%r = 0%r / (2^k0)%r by smt.
smt.
cut bnd_pos: 0%r <= (qS + qH)%r / (2^k0)%r.
cut leq: 0%r <= (qS + qH)%r by smt.
cut lt: 0%r < (2^k0)%r by smt.
cut ->: 0%r = 0%r / (2^k0)%r by smt.
smt.
sp; if.
seq 1: (mem (m,r) (dom Hmap.m) /\ c <> Adv) ((qH + qS)%r/(2^k0)%r) (1%r) _ 0%r (!H0'2.badh)=> //.
by rnd.
rnd (fun r, mem (m,r) (dom Hmap.m)); skip; progress.
cut <-: mu ((Dunit.dunit m{hr}) * salt) (cpMem (dom Hmap.m{hr}))
= mu salt (fun r, mem (m{hr},r) (dom Hmap.m{hr})).
cut ->: mu ((Dunit.dunit m{hr}) * salt) (cpMem (dom Hmap.m{hr}))
= mu ((Dunit.dunit m{hr}) * salt) (fun x, (fun a, a = m{hr}) (fst x) /\
(fun b, mem (m{hr},b) (dom Hmap.m{hr})) (snd x)).
rewrite mu_support /support /Pred.(/\) /cpMem; apply mu_eq=> x //=.
by rewrite Dprod.supp_def Dunit.supp_def; smt.
by rewrite Dprod.mu_def Dunit.mu_def /charfun /=.
apply (Trans _ ((card (dom Hmap.m{hr}))%r * (1%r / (2^k0)%r))).
apply mu_cpMem_le.
move=> x mem_x; rewrite /mu_x.
cut ->: mu ((Dunit.dunit m{hr}) * salt) ((=) x)
= mu ((Dunit.dunit m{hr}) * salt) (fun y, (fun a, a = fst x) (fst y) /\
(fun b, b = snd x) (snd y))
by (apply mu_eq; smt).
rewrite Dprod.mu_def Dunit.mu_def /charfun /=.
case (m{hr} = fst x).
pose r:= snd x; cut ->: (fun x, x = r) = ((=) r) by (apply fun_ext; smt).
by rewrite -/(mu_x _ _); smt.
smt.
cut ->: forall x, x * (1%r / (2^k0)%r) = x / (2^k0)%r by smt.
by apply H; smt.
hoare; inline Game0'2'badh.H.o; auto; smt.
smt.
by hoare.
(*-*) progress; proc; rcondt 3; first by auto.
seq 3: (Game0'2'badh.cHs < qS /\
card (dom Hmap.m) < qH + qS /\
c = Game0'2'badh.cHs);
first by rnd; wp.
inline Game0'2'badh.H.o; auto; smt.
(*-*) by progress; proc; rcondf 3; auto.
qed.
(* Game 0.1 -> Game 0.2 *)
local lemma Game0'1_0'2 &m:
Pr[Game0'1.main() @ &m: res]
<= Pr[Game0'2.main() @ &m: res]
+ (qS + qH)%r * (qS + qH + qG - 1)%r / (2^kh)%r
+ qS%r * (qS + qH)%r / (2^k0)%r.
proof.
rewrite (Game0'1_G0'1 &m).
cut: Pr[GameG0'1.main() @ &m: res] <= Pr[Game0'2.main() @ &m: res \/ H0'2.badg \/ H0'2.badh].
byequiv (_: ={glob GAdv1} ==> !(H0'2.badg \/ H0'2.badh){2} => ={res}); last 2 smt.
by (apply (GameG0'1_0'2_abstract GAdv1); apply GAdv1_main_ll).
rewrite Pr [mu_or] Pr [mu_or] (Game0'2_0'2'badg &m) (Game0'2_0'2'badh &m).
by cut:= Game0'2'badg &m; cut:= Game0'2'badh &m; smt.
qed.
(* end computation *)
(**** Current status *)
local lemma PSS96_Game1 &m:
Pr[UF_CMA(Wrap(PSS96(H,G)),Bounded_PSS_Adv(A,H,G)).main() @ &m: res]
<= Pr[Game1.main() @ &m: res]
+ (qS + qH)%r * (qS + qH + qG - 1)%r / (2^kh)%r
+ qS%r * (qS + qH)%r / (2^k0)%r.
proof.
rewrite (PSS96_Game0 &m) (Game0_0'1 &m).
cut <-: Pr[Game0'2.main() @ &m: res] = Pr[Game1.main() @ &m: res].
by byequiv (_: ={glob A} ==> ={res})=> //; sim.
by apply (Game0'1_0'2 &m).
qed.
(*** Game2: Sample the signature then fix the random oracles
1) to make verification succeed when called by signature oracle,
2) to let the adversary break one-way otherwise. *)
local module H2: SplitOracle1 = {
proc init = H0.init
proc o(c:caller,m:message,r:salt): (htag * gtag) option = {
var w, st, u, z, ho;
u = 0;
z = 0;
ho = None;
if (invertible Hmem.pk Hmem.xstar \/ c <> Adv) {
u = $sigd Hmem.pk Hmem.sk (c = Adv) Hmem.xstar;
z = if c = Adv
then (Hmem.ystar ** (rsap Hmem.pk u)) Hmem.pk
else rsap Hmem.pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,u);
Gmap.m.[w] = (st,c);
}
ho = Some (w,st);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
}
return ho;
}
proc v = H0.v
}.
local module Game2 = Gen1(GAdv1,H2,G1).
(* We push the sampling operations out of H
so we can reason about them abstractly.
At the same time, we let Ha do work only when
the (global) one-way challenge is invertible. *)
module type H1Sample = {
proc sample(c:caller): htag * gtag
}.
local module GenH1(S:H1Sample): SplitOracle1 = {
proc init = H0.init
proc o(c:caller,m:message,r:salt): (htag * gtag) option = {
var w, st, ho;
ho = None;
if (invertible Hmem.pk Hmem.xstar \/ c <> Adv) {
(w,st) = S.sample(c);
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,2^k - 1);
Gmap.m.[w] = (st,c);
}
ho = Some (w,st);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
}
return ho;
}
proc v = H0.v
}.
local module SampleWST = {
proc sample(c:caller): htag * gtag = {
var w, st;
w = $htag;
st = $gtag;
return (w,st);
}
}.
local module Game1'1 = Gen1(GAdv1,GenH1(SampleWST),G1).
(* proof of refactoring (upto sampling a non-invertible one-way challenge) *)
local equiv Game1_1'1_H: H1.o ~ GenH1(SampleWST).o:
={glob Hmap, glob Gmap, c, m, r} /\
(c{2} = Adv => invertible Hmem.pk{2} Hmem.xstar{2}) ==>
={glob Hmap, glob Gmap, res}.
proof.
proc.
rcondt{2} 2; first by auto; smt.
by inline SampleWST.sample; auto.
qed.
local lemma Game1_1'1_abstract (Ga <: Gadv1 {Gmap,Hmap}):
(forall (H <: SplitOracle1 {Ga}) (G <: Gt.Types.ARO {Ga}),
islossless H.o => islossless G.o => islossless H.v => islossless Ga(H,G).main) =>
equiv [Gen1(Ga,H1,G1).main ~ Gen1(Ga,GenH1(SampleWST),G1).main:
={glob Ga} ==>
={res} \/ !invertible Hmem.pk{2} Hmem.xstar{2}].
proof.
move=> GAdv_main_ll; proc.
seq 3 3: (={glob Ga, glob Gmap, glob Hmap, keys});
first by sim.
case (!invertible Hmem.pk{2} Hmem.xstar{2}).
call{1} (GAdv_main_ll H1 G1 _ _ _).
by proc; auto; smt.
by proc; auto; smt.
by proc; auto; smt.
call{2} (GAdv_main_ll (GenH1(SampleWST)) G1 _ _ _).
by proc; inline SampleWST.sample; sp; if=> //; auto; smt.
by proc; auto; smt.
by proc; auto; smt.
by skip; smt.
call (_: ={glob Gmap, glob Hmap} /\ invertible Hmem.pk{2} Hmem.xstar{2}).
by conseq Game1_1'1_H.
by conseq (_: _ ==> ={glob Gmap, res}); last sim.
by conseq (_: _ ==> ={res}); last sim.
by inline *; auto.
qed.
(* computation of probability of sampling a non-invertible element *)
local lemma Game1'1_bad &m:
Pr[Game1'1.main() @ &m: !invertible Hmem.pk Hmem.xstar] <= 1%r/(2^(k /% 2 - 2))%r.
proof.
byphoare (_: true ==> !invertible Hmem.pk Hmem.xstar)=> //.
proc.
seq 3: (!invertible Hmem.pk Hmem.xstar) (1%r/(2^(k /% 2 - 2))%r) 1%r _ 0%r=> //.
inline GenH1(SampleWST).init Hmap.init G1.init Gmap.init.
wp; call Hmem_init_bad.
by auto.
by hoare; call (_: true).
qed.
(* end of computation *)
(* end of refactoring proof *)
local module SampleU = {
proc sample(c:caller): htag * gtag = {
var u, z, w, st;
u = $sigd Hmem.pk Hmem.sk (c = Adv) Hmem.xstar;
z = simul Hmem.pk Hmem.sk (c = Adv) Hmem.xstar u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
return (w,st);
}
}.
local module Game1'2 = Gen1(GAdv1,GenH1(SampleU),G1).
(* proof of distribution equality *)
local equiv Game1'1_1'2_sample: SampleWST.sample ~ SampleU.sample:
={c} /\
(c{2} = Adv => invertible Hmem.pk{2} Hmem.xstar{2}) /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
rsap_dom Hmem.pk{2} Hmem.xstar{2} /\
valid_keys (Hmem.pk,Hmem.sk){2} ==>
={res}.
proof.
bypr (res{1}) (res{2})=> //.
progress.
cut ->: Pr[SampleWST.sample(c{1}) @ &1: a = res] = 1%r/(2^(kg + kh))%r.
byphoare (_: true ==> a = res)=> //; proc.
seq 1: (w = a.`1) (1%r/(2^kh)%r) (1%r/(2^kg)%r) _ 0%r=> //.
rnd; skip; progress.
cut ->: (fun x, x = a.`1) = ((=) a.`1) by apply fun_ext; smt.
smt.
by rnd ((=) a.`2); skip; progress; smt.
by hoare; rnd; skip; smt.
progress; cut ->: (2^kh)%r * (2^kg)%r = (2^kh * 2^kg)%r by smt.
by rewrite pow_add; smt.
rewrite Logic.eq_sym.
byphoare (_: (c = Adv => invertible Hmem.pk Hmem.xstar) /\
Hmem.ystar = rsap Hmem.pk Hmem.xstar /\
rsap_dom Hmem.pk Hmem.xstar /\
valid_keys (Hmem.pk,Hmem.sk) ==>
a = res)=> //.
proc; elim/tuple2_ind a=> a w0 st0 a_def.
wp 2.
conseq (_: _ ==>
z = os2ip (to_signature (zeros 1 || from_htag w0 || from_gtag st0)))
(_: _ ==> 0 <= z < 2^(k-1)) => //;first by (auto;smt).
progress; rewrite /from_htag /to_htag /from_gtag /to_gtag /from_signature
/to_signature; last 2 by smt.
cut [_ <-] := msb0_bnd (i2osp z0);first by smt.
rewrite /from_signature HTag.pcan_to_from 1:smt.
rewrite GTag.pcan_to_from 1:smt.
rewrite sub_app_sub //;first 3 smt.
rewrite app_sub;first 3 smt.
by rewrite Signature.can_from_to; smt.
wp; rnd; skip; progress.
rewrite /sigd mu_def /=.
rewrite mu_support /Pred.(/\) /=.
pose x0:= os2ip (to_signature (zeros 1 || from_htag w0 || from_gtag st0)).
cut x0_bnd: 0 <= x0 < 2^(k - 1) by smt.
cut ->: (fun x, simul Hmem.pk{hr} Hmem.sk{hr} (c{hr} = Adv) Hmem.xstar{hr}
(simul_inv Hmem.pk{hr} Hmem.sk{hr} (c{hr} = Adv) Hmem.xstar{hr} x)
= x0 /\ support [0..2^(k - 1) - 1] x)
= ((=) x0).
apply fun_ext=> x /=; rewrite eq_iff; split.
by rewrite andC=> -[supp_x]; rewrite simul_invK //; first smt.
by move=> <-; rewrite simul_invK //; smt.
by rewrite -/(mu_x _ _) Dinter.mu_x_def_in; smt.
qed.
local equiv Game1'1_1'2_H: GenH1(SampleWST).o ~ GenH1(SampleU).o:
={glob Hmap, glob Gmap, c, m, r} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
rsap_dom Hmem.pk{2} Hmem.xstar{2} /\
valid_keys (Hmem.pk,Hmem.sk){2} ==>
={glob Hmap, glob Gmap, res}.
proof. by proc; sp; if=> //; wp; call Game1'1_1'2_sample; auto; progress; elim H1=> //=; smt. qed.
local equiv Game1'1_1'2_abstract (Ga <: Gadv1 {Gmap,Hmap}):
Gen1(Ga,GenH1(SampleWST),G1).main ~ Gen1(Ga,GenH1(SampleU),G1).main:
={glob Ga} ==> ={res}.
proof.
proc.
call (_: ={glob Hmap, glob Gmap} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
rsap_dom Hmem.pk{2} Hmem.xstar{2} /\
valid_keys (Hmem.pk,Hmem.sk){2}).
by conseq Game1'1_1'2_H.
by proc; auto.
by proc; auto.
by inline*; auto; smt.
qed.
(* proof of defactoring and storing u in Hmap *)
local equiv Game1'2_2_H: GenH1(SampleU).o ~ H2.o:
={glob Hmem, glob Gmap, c, m, r} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
hmap_peq Hmap.m{1} Hmap.m{2} ==>
={glob Hmem, glob Gmap, res} /\ hmap_peq Hmap.m{1} Hmap.m{2}.
proof.
proc; inline SampleU.sample.
sp; if=> //.
seq 7 5: (={w, ho, u, z, st, glob Hmem, glob Gmap, c, m, r} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
hmap_peq Hmap.m{1} Hmap.m{2});
first by auto.
if => //.
progress.
by rewrite -(hmap_peq_dom Hmap.m{1}).
by rewrite (hmap_peq_dom _ Hmap.m{2}).
auto; progress.
by apply hmap_peq_set.
auto; progress.
cut indom1: mem (m,r){2} (dom Hmap.m){1} by smt.
cut:= indom1; rewrite (hmap_peq_dom _ Hmap.m{2}) //.
move: indom1.
rewrite !mem_dom /oget /pi3_1.
cut:= H (m,r){2}.
case (Hmap.m{1}.[(m,r)]{2})=> //=.
case (Hmap.m.[(m,r)]{2})=> //=.
smt.
qed.
local equiv Game1'2_2_abstract (Ga <: Gadv1 {Gmap,Hmap}):
Gen1(Ga,GenH1(SampleU),G1).main ~ Gen1(Ga,H2,G1).main:
={glob Ga} ==> ={res}.
proof.
proc.
call (_: ={glob Hmem, glob Gmap} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
hmap_peq Hmap.m{1} Hmap.m{2}).
by conseq Game1'2_2_H.
by conseq (_: _ ==> ={glob Gmap, res})=> //; sim.
by proc; auto; smt.
inline GenH1(SampleU).init H2.init.
call Hmap_init.
wp; call (_: true ==> ={glob Gmap}); first by sim.
by rnd; skip; smt.
qed.
(* end of proof *)
(**** Current status *)
local lemma PSS96_Game2 &m:
Pr[UF_CMA(Wrap(PSS96(H,G)),Bounded_PSS_Adv(A,H,G)).main() @ &m: res]
<= Pr[Game2.main() @ &m: res]
+ (qS + qH)%r * (qS + qH + qG - 1)%r / (2^kh)%r
+ qS%r * (qS + qH)%r / (2^k0)%r
+ 1%r / (2^(k /% 2 - 2))%r.
proof.
cut <-: Pr[Game1'2.main() @ &m: res] = Pr[Game2.main() @ &m: res].
by byequiv (Game1'2_2_abstract GAdv1).
cut <-: Pr[Game1'1.main() @ &m: res] = Pr[Game1'2.main() @ &m: res].
by byequiv (Game1'1_1'2_abstract GAdv1).
cut: Pr[Game1.main() @ &m: res] <= Pr[Game1'1.main() @ &m: res \/ !invertible Hmem.pk Hmem.xstar].
byequiv (_: ={glob GAdv} ==> ={res} \/ !invertible Hmem.pk{2} Hmem.xstar{2}); last 2 smt.
by apply (Game1_1'1_abstract GAdv1 _); apply GAdv1_main_ll.
by rewrite Pr [mu_or]; smt.
qed.
(* Game 3: cleaning the games up and preparing for the reduction *)
local module GAdv3(H:SplitOracle1, G:Gt.Types.ARO) = {
(* Wrapping a split oracle for direct use by the adversary *)
module Ha = {
proc o(m:message * salt): htag = {
var r = None;
if (Mem.cH < qH) {
r = H.o(Adv,fst m,snd m);
Mem.cH = Mem.cH + 1;
}
return oget (omap fst r);
}
}
(* Wrapping a split oracle for use by the signing oracle *)
module Hs = {
proc o(m:message * salt): (htag*gtag) option = {
var r;
r = H.o(Sig,fst m,snd m);
return r;
}
}
(* Counting queries to G *)
module Ga = {
proc o(w:htag): gtag = {
var r = witness;
if (Mem.cG < qG) {
r = G.o(w);
Mem.cG = Mem.cG + 1;
}
return r;
}
}
(* Signing oracle *)
module S = {
proc sign(m:message): signature = {
var r, wo, w, g, rs, em;
var s = witness;
if (Mem.cS < qS) {
r = $salt;
wo = Hs.o(m,r);
if (wo = None)
s = witness;
else {
(w,g) = oget wo;
rs = g ^ (to_gtag (from_salt r || zeros (kg - k0)));
em = to_signature (zeros 1 || (from_htag w) || (from_gtag rs));
s = i2osp (rsas Mem.sk (os2ip em));
Mem.qs = add (m,s) Mem.qs;
}
Mem.cS = Mem.cS + 1;
}
return s;
}
proc fresh(m:message, s:signature): bool = {
return !mem (m,s) Mem.qs;
}
}
module A = A(Ha, Ga, S)
var lucky:bool
proc main (ks:pkey*skey): bool = {
var m, s;
var y, w, st, g, rs, r, w';
Mem.init(ks);
(m,s) = A.forge(Mem.pk);
y = from_signature (i2osp (rsap Mem.pk (os2ip s)));
w = to_htag (sub y 1 kh);
st = to_gtag (sub y (1 + kh) kg);
g = G.o(w);
rs = from_gtag (st ^ g);
r = to_salt (sub rs 0 k0);
lucky = !mem (m,r) (dom Hmap.m);
w' = H.v(m,r);
return sub y 0 1 = zeros 1 /\ w = w' /\ sub rs k0 (kg - k0) = zeros (kg - k0) /\
0 <= os2ip s < p_n Mem.pk /\ !mem (m,s) Mem.qs;
}
}.
local module H3: SplitOracle1 = {
proc init = Hmap.init
proc o(c:caller,m:message,r:salt): (htag*gtag) option = {
var w, st, u, z, ho;
u = 0;
z = 0;
ho = None;
if (invertible Hmem.pk Hmem.xstar \/ c <> Adv) {
u = $sigd Hmem.pk Hmem.sk (c = Adv) Hmem.xstar;
z = if c = Adv
then (Hmem.ystar ** (rsap Hmem.pk u)) Hmem.pk
else rsap Hmem.pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,u);
Gmap.m.[w] = (st,c);
}
ho = Some (w,st);
}
else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
}
return ho;
}
proc v = H0.v
}.
local module Game3 = Gen1(GAdv3,H3,G1).
local lemma Game2_3 &m:
Pr[Game2.main() @ &m: res] = Pr[Game3.main() @ &m: res].
proof.
byequiv (_: ={glob A} ==> ={res})=> //.
by proc; inline *; sim.
qed.
(* Game 3.1: abort if a u-value sampled by H during a query made by the adversary is non-invertible *)
local module H3'1: SplitOracle1 = {
var bad:bool
proc init(ks:keypair): unit = {
Hmap.init(ks);
bad = false;
}
proc o(c:caller,m:message,r:salt): (htag*gtag) option = {
var w, st, u, z, ho;
u = 0;
z = 0;
ho = None;
if (invertible Hmem.pk Hmem.xstar \/ c <> Adv) {
u = $sigd Hmem.pk Hmem.sk (c = Adv) Hmem.xstar;
z = if c = Adv
then (Hmem.ystar ** (rsap Hmem.pk u)) Hmem.pk
else rsap Hmem.pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
bad = bad \/ (c = Adv /\ !invertible Hmem.pk u);
if (c <> Adv \/ invertible Hmem.pk u) {
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,u);
Gmap.m.[w] = (st,c);
}
ho = Some (w,st);
}
else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
}
}
return ho;
}
proc v = H0.v
}.
local module Game3'1 = Gen1(GAdv3,H3'1,G1).
local equiv Game3_3'1_H: H3.o ~ H3'1.o:
!H3'1.bad{2} /\ ={glob Hmap, glob Gmap, c, m, r} ==>
!H3'1.bad{2} => ={glob Hmap, glob Gmap, res}.
proof.
proc; sp; if=> //.
seq 5 5: (!H3'1.bad{2} /\
(c{1} = Adv => invertible Hmem.pk{1} Hmem.xstar{1}) /\
={glob Hmap, glob Gmap, c, m, r, u, z, w, st, ho} /\ ho{1} = None);
first by auto.
case ((c = Adv /\ !invertible Hmem.pk u){2}).
by rcondf{2} 2; auto; smt.
rcondt{2} 2; first by auto; smt.
sp 0 1; if; first smt.
by sim.
by wp.
qed.
local equiv Game3_3'1: Game3.main ~ Game3'1.main:
={glob A} ==> !H3'1.bad{2} => ={res}.
proof.
proc.
call (_: !H3'1.bad{2} /\ ={glob A, glob Hmap, glob Gmap, ks} /\
support keypairs ks{1} ==>
!H3'1.bad{2} => ={res}).
proc.
inline H3.v H3'1.v G1.o; auto.
call (_: H3'1.bad,
={glob Hmap, glob Gmap, glob Mem} /\
support keypairs (Mem.pk,Mem.sk){1},
={Mem.pk, Mem.sk} /\
support keypairs (Mem.pk,Mem.sk){1}).
by progress; apply (A_forge_ll H G O).
proc; sp; if=> //.
inline GAdv3(H3,G1).Hs.o GAdv3(H3'1,G1).Hs.o.
wp; call Game3_3'1_H.
by auto; smt.
by progress; proc; inline*; sp; if=> //; rcondt 9; auto; smt.
by progress; proc; inline*; sp; if=> //; rcondt 9; auto; smt.
by progress; proc; inline*; sp; if=> //; auto; smt.
by progress; proc; inline*; sp; if=> //; auto; smt.
by progress; proc; inline *; sp; if=> //; auto; smt.
by progress; proc; inline *; sp; if=> //; sp; if=> //; auto.
by progress; proc; inline *; sp; if=> //; sp; if=> //; auto; smt.
by progress; proc; inline *; sp; if=> //; sp; if=> //; auto; smt.
by inline *; auto; smt.
by inline *; auto.
qed.
(* computing the probability of H3'1.bad *)
local module Game3'1'bad = {
module Ha = {
proc o(mr:message * salt): htag = {
var m, r, w, st, u, z, h;
(m,r) = mr;
u = 0;
z = 0;
h = witness;
if (Mem.cH < qH) {
if (invertible Hmem.pk Hmem.xstar /\
support keypairs (Hmem.pk,Hmem.sk) /\
0 <= Hmem.xstar < p_n Hmem.pk) {
u = $sigd Hmem.pk Hmem.sk true Hmem.xstar;
z = simul Hmem.pk Hmem.sk true Hmem.xstar u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
H3'1.bad = H3'1.bad \/ !invertible Hmem.pk u;
if (invertible Hmem.pk u) {
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,Adv,u);
Gmap.m.[w] = (st,Adv);
}
h = w;
}
else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
h = w;
}
}
}
Mem.cH = Mem.cH + 1;
}
return h;
}
}
module Ga = {
proc o(w:htag): gtag = {
var r = witness;
if (Mem.cG < qG) {
r = G1.o(w);
Mem.cG = Mem.cG + 1;
}
return r;
}
}
module Hs = {
proc o(m:message,r:salt): (htag * gtag) option = {
var w, st, u, z, ho;
u = 0;
z = 0;
ho = None;
u = $sigd Hmem.pk Hmem.sk false Hmem.xstar;
z = rsap Hmem.pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,Sig,u);
Gmap.m.[w] = (st,Sig);
}
ho = Some (w,st);
}
else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = None;
}
return ho;
}
}
module S = {
proc sign(m:message): signature = {
var r, wo, w, g, rs, em;
var s = witness;
if (Mem.cS < qS) {
r = $salt;
wo = Hs.o(m,r);
if (wo = None)
s = witness;
else {
(w,g) = oget wo;
rs = g ^ (to_gtag (from_salt r || zeros (kg - k0)));
em = to_signature (zeros 1 || (from_htag w) || (from_gtag rs));
s = i2osp (rsas Mem.sk (os2ip em));
Mem.qs = add (m,s) Mem.qs;
}
Mem.cS = Mem.cS + 1;
}
return s;
}
proc fresh(m:message, s:signature): bool = {
return !mem (m,s) Mem.qs;
}
}
module A = A(Ha, Ga, S)
var lucky:bool
proc main (): unit = {
var m, s, ks;
ks = $keypairs;
G1.init();
H3'1.init(ks);
Mem.init(ks);
(m,s) = A.forge(Mem.pk);
}
}.
local equiv Game3'1_3'1'bad: Game3'1.main ~ Game3'1'bad.main: ={glob A} ==>
H3'1.bad{1} = (H3'1.bad /\ Mem.cH <= qH){2}.
proof.
proc.
inline Gen1(GAdv3,H3'1,G1).GA.main.
inline H3'1.v G1.o; auto.
conseq (_: _ ==> ={H3'1.bad} /\ Mem.cH{2} <= qH); first smt.
call (_: ={glob H3'1, glob Gmap, glob Mem} /\
Mem.cH{2} <= qH /\
support keypairs (Hmem.pk,Hmem.sk){1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1}).
proc; sp; if=> //; auto.
call (_: ={glob H3'1, glob Gmap} /\ m{1} = (m,r){2} ==> ={glob H3'1, glob Gmap, res}).
proc; inline H3'1.o.
rcondt{1} 7; first by auto.
rcondt{1} 13; first by auto.
by auto.
by auto.
by proc; inline *; sp; if=> //; auto.
proc; sp; if=> //.
inline H3'1.o; sp; if=> //; first smt.
by auto; progress; expect 26 smt.
by auto; progress; smt.
by inline *; auto; progress; smt.
qed.
local lemma Pr_Game3'1'bad &m:
Pr[Game3'1'bad.main() @ &m: H3'1.bad /\ Mem.cH <= qH] <= qH%r * 1%r/(2^(k /% 2 - 1))%r.
proof.
fel 4 (Mem.cH)
(fun x, 1%r / (2^(k /% 2 - 1))%r)
(qH)
(H3'1.bad)
[Game3'1'bad.Ha.o: (Mem.cH < qH)].
(*-*) rewrite /int_sum (Monoid.Mrplus.NatMul.sum_const (1%r / (2^(k /% 2 - 1))%r)) //.
rewrite /intval card_interval_max (_: qH - 1 - 0 + 1 = qH); first smt.
rewrite /max (_: qH < 0 = false) /=; first smt.
by rewrite /Monoid.Mrplus.NatMul.( * ); smt.
(*-*) smt.
(*-*) by inline *; auto.
(*-*) cut H: forall (x y z:real), x <= y => 0%r < z => x / z <= y / z by smt.
cut bnd1_pos: 0%r <= 1%r / (2^(k /% 2 - 1))%r.
cut leq: 0%r <= 1%r by smt.
cut lt: 0%r < (2^(k /% 2 - 1))%r by smt.
cut ->: 0%r = 0%r / (2^(k /% 2 - 1))%r by smt.
smt.
proc.
sp; if=> //; last by hoare; skip; smt.
sp; if=> //; last by hoare; auto.
seq 1: (!invertible Hmem.pk u) (1%r / (2^(k /% 2 - 1))%r) 1%r _ 0%r (!H3'1.bad)=> //.
by rnd.
rnd; skip; progress.
rewrite /sigd.
pose f:= simul Hmem.pk{hr} Hmem.sk{hr} true Hmem.xstar{hr}.
pose finv:= simul_inv Hmem.pk{hr} Hmem.sk{hr} true Hmem.xstar{hr}.
cut ->: mu (dapply finv [0..2^(k - 1) -1]) (fun x, !invertible Hmem.pk{hr} x)
= mu [0..2^(k - 1) - 1] (fun x, !invertible Hmem.pk{hr} x).
rewrite Dapply.mu_def /=.
rewrite (mu_support (fun x, !invertible Hmem.pk{hr} x))
(mu_support (fun x, !invertible Hmem.pk{hr} (finv x))).
apply mu_eq=> x; rewrite /Pred.(/\) /= eq_iff; split.
by rewrite /finv /simul_inv /= -invertible_mulzp -invertible_inv H3 -invertible_rsas.
by progress; rewrite /finv /simul_inv /= -invertible_mulzp -invertible_inv H3 -invertible_rsas.
rewrite -Dinter_uni.dinter_is_dinter Dinter_uni.mu_def_nz; first smt.
cut ->: (fun x, !invertible Hmem.pk{hr} x) = !invertible Hmem.pk{hr} by apply fun_ext.
apply (Trans _ ((2^(k /% 2))%r / (2^(k - 1))%r)).
rewrite card_interval_max /max (_: 2^(k - 1) - 1 - 0 + 1 = 2^(k - 1)); first smt.
cut ->: 2^(k - 1) < 0 = false by smt.
simplify.
cut:= card_noninvertible_2k1 Hmem.pk{hr} Hmem.sk{hr} _=> // bound_den.
by apply (_: forall (x y z:real), 0%r < z => x <= y => x / z <= y / z)=> //; smt.
rewrite Real.PowerInt.pow_div_den; first smt.
apply (_: forall (x y:real), 0%r < x <= y => 1%r / y <= 1%r / x); first smt.
split; first smt.
by rewrite FromInt.from_intMle; smt.
by hoare; auto; smt.
(*-*) progress; proc; rcondt 5; first by auto.
by sp; if; auto; progress; expect 4 smt.
(*-*) progress; proc; rcondf 5; auto.
qed.
(** We refactor the game into an adversary against the sampling of u in H
then use the GenDice generic argument to replace the restricted sampling
with a (non-PTIME) loop *)
module type LoopSampling = {
proc sample(i:pkey * skey * bool * int, dflt:int): int
}.
local module GenH3(S:LoopSampling) = {
proc init = Hmap.init
proc o(c:caller,m:message,r:salt): (htag*gtag) option = {
var w, st, u, z, ho;
u = 0;
z = 0;
ho = None;
if (invertible Hmem.pk Hmem.xstar \/ c <> Adv) {
u = S.sample((Hmem.pk,Hmem.sk,c = Adv,Hmem.xstar),2^k - 1);
z = if c = Adv
then (Hmem.ystar ** (rsap Hmem.pk u)) Hmem.pk
else rsap Hmem.pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (c <> Adv \/ invertible Hmem.pk u) {
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,u);
Gmap.m.[w] = (st,c);
}
ho = Some (w,st);
}
else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
}
}
return ho;
}
proc v = H0.v
}.
local module Direct = {
proc sample(i:pkey * skey * bool * int, dflt:int): int = {
var r, pk, sk, b, x;
(pk,sk,b,x) = i;
r = $sigd pk sk b x;
return r;
}
}.
local equiv Game3'1_GenH3_H: H3'1.o ~ GenH3(Direct).o:
={glob Hmap, glob Gmap, c, m, r} ==>
={glob Hmap, glob Gmap, res}.
proof.
proc; inline Direct.sample; sp; if=> //.
sim.
by rnd; wp.
qed.
local equiv Game3'1_Direct:
Gen1(GAdv3,H3'1,G1).main ~ Gen1(GAdv3,GenH3(Direct),G1).main: ={glob A} ==> ={res}.
proof.
proc.
inline Gen1(GAdv3,H3'1,G1).GA.main Gen1(GAdv3,GenH3(Direct),G1).GA.main; sim.
call (_: ={glob Hmap, glob Gmap, glob Mem}).
proc; sp; if=> //; sp.
inline GAdv3(H3'1,G1).Hs.o GAdv3(GenH3(Direct),G1).Hs.o.
auto; call Game3'1_GenH3_H.
by auto.
by sim.
proc; sp; if=> //; sp.
auto; call Game3'1_GenH3_H.
by auto.
by inline *; auto.
qed.
local module Loop = {
proc sample(i:pkey * skey * bool * int, dflt:int): int = {
var u, z, pk, sk, b, x;
u = 0;
z = dflt;
(pk,sk,b,x) = i;
while (!0 <= z < 2^(k - 1))
{
u = $challenge pk;
z = simul pk sk b x u;
}
return u;
}
}.
local lemma Direct_Loop pk' sk' b' x' d a &1 &2:
valid_keys (pk',sk') =>
rsap_dom pk' x' =>
(b' => invertible pk' x') =>
!0 <= d < 2^(k - 1) =>
Pr[Direct.sample((pk',sk',b',x'),d) @ &1: res = a]
= Pr[Loop.sample((pk',sk',b',x'),d) @ &2: res = a].
proof.
progress.
case (exists r', 0 <= r' < 2^(k - 1) /\ a = simul_inv pk' sk' b' x' r').
move=> [r'] [valid_r'] ->.
cut ->: Pr[Direct.sample((pk',sk',b',x'),d) @ &1: res = simul_inv pk' sk' b' x' r']
= 1%r/(2^(k - 1))%r.
byphoare (_: i = (pk',sk',b',x') ==> res = simul_inv pk' sk' b' x' r')=> //.
proc; inline *; wp; rnd (fun r, simul pk' sk' b' x' r = r'); wp; skip; progress.
rewrite /sigd Dapply.mu_def /= mu_support.
cut ->: ((fun r, simul pk' sk' b' x' (simul_inv pk' sk' b' x' r) = r') /\ support [0..2^(k - 1) - 1])
= ((=) r').
rewrite /Pred.(/\) /= -fun_ext=> y /=.
rewrite eq_iff; split.
by progress; rewrite simul_invK //; first smt.
progress.
by rewrite simul_invK //; first smt.
smt.
rewrite -/(mu_x _ _) Dinter.mu_x_def.
cut ->: in_supp r' [0..2^(k - 1) - 1] by smt.
smt.
by rewrite simulK //; smt.
by rewrite simul_invK //; smt.
apply Logic.eq_sym.
pose bdt:= (2^(k - 1))%r.
cut bdt_pos: 0 < 2^(k - 1) by smt.
cut bdt_posr: 0%r < (2^(k - 1))%r by smt.
byphoare (_: i = (pk',sk',b',x') /\ dflt = d ==> res = simul_inv pk' sk' b' x' r')=> //; proc.
pose bd:= mu_x (challenge pk') r'.
cut bd_pos: 0%r < bd by smt.
cut d_uni: forall x, in_supp x (challenge pk') => mu_x (challenge pk') x = bd.
by move=> y Hy; rewrite /bd; apply challengeU=> //; smt.
cut Hdiff: bdt <> (Real.zero)%Real by smt.
sp.
conseq [-frame] (_: (pk,sk,b,x){hr} = (pk',sk',b',x') /\ !0 <= z < 2^(k - 1) ==>
u = simul_inv pk' sk' b' x' r': = (if 0 <= z < 2^(k - 1)
then charfun ((=) (simul_inv pk' sk' b' x' r')) u
else 1%r / bdt)) => //;
first smt.
while ((pk,sk,b,x){hr} = (pk',sk',b',x'))
(if 0 <= z < 2^(k - 1) then 0 else 1) 1 (bdt * bd) => //.
progress; cut ->: 0 <= z < 2^(k - 1) by smt.
rewrite /= /charfun; cut ->: (simul_inv pk sk b x r' = u){hr} = false by smt.
smt.
smt.
move=> Hw.
alias 3 z0 = z.
phoare split bd ((1%r - bdt*bd) * (1%r/bdt)): (r' = z0).
move=> &hr [H5 H6]; rewrite (_: 0 <= z{hr} < 2^(k - 1) = false) 1:neqF //=.
cut {1}->: bd = bd * bdt / bdt.
cut ->: bd * bdt / bdt = bd * (bdt / bdt) by smt.
cut ->: bdt / bdt = 1%r by smt.
smt.
smt.
seq 3: (r' = z0) bd 1%r _ 0%r (z0 = z /\
simul_inv pk' sk' b' x' z0 = u /\
(pk,sk,b,x) = (pk',sk',b',x'))=> //.
by auto; progress; rewrite simulK //; smt.
wp; rnd; skip; progress.
cut ->: mu (challenge pk{hr}) (fun y, r' = simul pk sk b x y){hr}
= mu (challenge pk{hr}) ((=) (simul_inv pk sk b x r')){hr}.
rewrite (mu_support (fun y, r' = simul pk sk b x y){hr})
(mu_support ((=) (simul_inv pk sk b x r'){hr})).
apply mu_eq=> y; rewrite /Pred.(/\) /= eq_iff; split.
by progress; rewrite simulK //; smt.
by progress; rewrite simul_invK //; smt.
by rewrite /bd /mu_x; apply challengeU; smt.
conseq Hw; progress=> //.
cut ->: 0 <= z{hr} < 2^(k - 1) by smt.
by rewrite /charfun.
hoare; conseq (_: _ ==> true) => //.
by progress;rewrite -nand;left.
seq 3: (0 <= z0 < 2^(k - 1)) _ 0%r (1%r - bdt * bd) (1%r/bdt)
((pk,sk,b,x) = (pk',sk',b',x') /\ 0 <= r' < 2^(k - 1) /\ z0 = z /\
simul_inv pk' sk' b' x' z = u)=> //.
by auto; progress; rewrite simulK //; smt.
case (r' = z0); first by conseq (_: _ ==> false).
conseq Hw; progress=> //.
cut ->: 0 <= z{hr} < 2^(k - 1) by smt.
rewrite /= /charfun.
cut simul_inj: (simul_inv pk sk b x r' = simul_inv pk sk b x z => r' = z){hr}.
cut {2}<-:= simul_invK pk{hr} sk{hr} b{hr} x{hr} r'=> //; first smt.
cut {2}<-:= simul_invK pk{hr} sk{hr} b{hr} x{hr} z{hr}=> //; first smt.
by move=> ->.
smt.
phoare split ! 1%r (bdt*bd); wp; rnd=> //.
by skip; smt.
skip; progress; rewrite /bdt /bd {2}/challenge Dinter.mu_x_def_in; first smt.
by rewrite mu_challenge_in_pim //; smt.
by conseq Hw => //; smt.
by conseq (_: _ ==> true)=> //; auto; smt.
progress; first smt.
wp; rnd; skip; progress.
cut ->: 0 <= z{hr} < 2^(k - 1) = false by smt.
rewrite /=; cut ->: (fun y, (if 0 <= simul pk sk b x y < 2^(k - 1) then 0 else 1) < 1){hr}
= (fun y, 0 <= simul pk sk b x y < 2^(k - 1)){hr}.
by apply fun_ext=> y /=; smt.
rewrite /bdt /bd {1}/challenge Dinter.mu_x_def_in; first smt.
by rewrite mu_challenge_in_pim //; smt.
cut ->: (!exists r', 0 <= r' < 2^(k - 1) /\ a = simul_inv pk' sk' b' x' r')
<=> (forall r', !0 <= r' < 2^(k - 1) \/ a <> simul_inv pk' sk' b' x' r').
by split; smt.
move=> r'_constraints.
cut ->: Pr[Direct.sample((pk',sk',b',x'),d) @ &1: res = a] = 0%r.
byphoare (_: i = (pk',sk',b',x') /\ dflt = d ==> res = a)=> //=.
hoare; proc; rnd; wp; skip=> //= &hr [i_def d_def] r; subst=> //=.
rewrite /sigd Dapply.supp_def.
smt.
apply Logic.eq_sym.
byphoare (_: i = (pk',sk',b',x') /\ dflt = d ==> res = a)=> //=.
hoare; proc.
while (valid_keys (pk,sk) /\ rsap_dom pk x /\ (b => invertible pk x) /\
(0 <= z < 2^(k - 1) => u = simul_inv pk sk b x z)).
by auto; progress; rewrite simulK //; smt.
wp; skip; progress.
smt.
cut:= H8 _; first smt.
smt.
qed.
local equiv Direct_Loop_equiv: Direct.sample ~ Loop.sample:
={i, dflt} /\ !0 <= dflt{1} < 2^(k - 1) /\
let (pk',sk',b',x') = i {1} in
valid_keys (pk',sk') /\
rsap_dom pk' x' /\
(b' => invertible pk' x') ==>
={res}.
proof.
bypr (res{1}) (res{2})=> //.
move=> &1 &2 a.
elim/tuple4_ind (i{2})=> i2 pk' sk' b' x' i2_def.
move: (dflt{2})=> d.
move=> [[->] ->] [d_invalid] //= [vkeys [vx' invx']].
cut:= Direct_Loop pk' sk' b' x' d a &1 &2 _ _ _ _=> //.
cut ->: Pr[Direct.sample((pk',sk',b',x'),d) @ &1: res = a]
= Pr[Direct.sample((pk',sk',b',x'),d) @ &1: a = res]
by rewrite Pr [mu_eq].
by move=> ->; rewrite Pr [mu_eq].
qed.
local equiv GenH3Direct_Loop: GenH3(Direct).o ~ GenH3(Loop).o:
={glob Hmap, glob Gmap, c, m, r} /\
valid_keys (Hmem.pk,Hmem.sk){2} /\ rsap_dom Hmem.pk{2} Hmem.xstar{2} ==>
={glob Hmap, glob Gmap, res}.
proof.
proc*; inline GenH3(Direct).o GenH3(Loop).o; sp; if=> //; first smt.
auto; call Direct_Loop_equiv.
by skip; progress; expect 27 smt.
by auto.
qed.
local lemma GameH3Direct_Loop &m:
Pr[Gen1(GAdv3,GenH3(Direct),G1).main() @ &m: res]
= Pr[Gen1(GAdv3,GenH3(Loop),G1).main() @ &m: res].
proof.
byequiv (_: ={glob A} ==> ={res})=> //.
proc.
inline Gen1(GAdv3,GenH3(Direct),G1).GA.main Gen1(GAdv3,GenH3(Loop),G1).GA.main
GenH3(Direct).v GenH3(Loop).v G1.o; auto.
call (_: ={glob Hmap, glob Gmap, glob Mem} /\
valid_keys (Hmem.pk,Hmem.sk){2} /\
rsap_dom Hmem.pk{2} Hmem.xstar{2}).
proc; inline GAdv3(GenH3(Direct),G1).Hs.o GAdv3(GenH3(Loop),G1).Hs.o; sp; if=> //; auto.
by call GenH3Direct_Loop; auto.
by proc; inline *; sp; if=> //; auto.
proc; sp; if=> //; auto.
by call GenH3Direct_Loop; auto.
by inline *; auto; smt.
qed.
local module H3'2: SplitOracle1 = {
proc init = Hmap.init
proc o(c:caller,m:message,r:salt): (htag * gtag) option = {
var w, st, u, z, ho, i, b;
u = 0;
z = 2^k - 1;
i = 0;
ho = None;
w = witness;
st = witness;
b = false;
if (invertible Hmem.pk Hmem.xstar \/ c <> Adv) {
while (!b) {
u = $challenge Hmem.pk;
z = if c = Adv
then (Hmem.ystar ** (rsap Hmem.pk u)) Hmem.pk
else rsap Hmem.pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
b = b \/ 0 <= z < 2^(k - 1);
i = i + 1;
}
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (c <> Adv \/ invertible Hmem.pk u) {
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,u);
Gmap.m.[w] = (st,c);
}
ho = Some (w,st);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
}
}
return ho;
}
proc v(m:message,r:salt):htag = {
var h;
h = $htag;
if (mem (m,r) (dom Hmap.m)) h = pi3_1 (oget Hmap.m.[(m,r)]);
return h;
}
}.
local module Game3'2 = Gen1(GAdv3,H3'2,G1).
local lemma H3'2_o_ll:
phoare [H3'2.o: support keypairs (Hmem.pk,Hmem.sk) /\
rsap_dom Hmem.pk Hmem.xstar /\
Hmem.ystar = rsap Hmem.pk Hmem.xstar ==>
true] = 1%r.
proof.
proc; sp; wp.
if=> //; wp.
while (valid_keys (Hmem.pk,Hmem.sk) /\
rsap_dom Hmem.pk Hmem.xstar /\
(c = Adv => invertible Hmem.pk Hmem.xstar) /\
Hmem.ystar = rsap Hmem.pk Hmem.xstar)
(if !b then 1 else 0) 1 ((2^(k-1))%r/(p_n Hmem.pk)%r)=> //.
smt.
progress; seq 6: (valid_keys (Hmem.pk,Hmem.sk) /\
rsap_dom Hmem.pk Hmem.xstar /\
(c = Adv => invertible Hmem.pk Hmem.xstar) /\
Hmem.ystar = rsap Hmem.pk Hmem.xstar)=> //.
by auto; smt.
by hoare; auto.
by auto; smt.
split.
progress.
cut lt_div: forall (x y z:real), 0%r < z => x < y => x / z < y / z by smt.
cut pos_inv: forall x, 0%r < x => 0%r < 1%r/x.
by move=> x lt0x; cut ->: 0%r = 0%r/x; smt.
cut ->: forall x y, x / y = x * 1%r/y by smt.
cut pos_mul: forall x y, 0%r < x => 0%r < y => 0%r < x * y by smt.
by apply (pos_mul ((2^(k-1))%r) (1%r/(p_n Hmem.pk{hr})%r)); smt.
move=> z; conseq (_: _: =((2^(k - 1))%r/(p_n Hmem.pk)%r)).
wp; rnd; skip; progress.
move: H2; rewrite -neqF=> -> //=.
cut ->: (fun x, (if !0 <= (if c{hr} = Adv
then ((rsap Hmem.pk Hmem.xstar) ** (rsap Hmem.pk x)) Hmem.pk
else rsap Hmem.pk x)
< 2^(k - 1)
then 1 else 0) < 1){hr} =
(fun x, (if (fun y, 0 <= simul Hmem.pk Hmem.sk (c = Adv) Hmem.xstar y < 2^(k - 1)){hr} x
then 0 else 1) < 1){hr}.
by rewrite /simul -fun_ext=> x //=; smt.
cut ->: forall (P:int -> bool), (fun x, (if P x then 0 else 1) < 1) = P.
by move=> P; apply fun_ext=> x /=; smt.
by apply mu_challenge_in_pim.
qed.
local equiv GenH3Loop_H3'2: GenH3(Loop).o ~ H3'2.o:
={glob Hmap, glob Gmap, c, m, r} /\
valid_keys (Hmem.pk,Hmem.sk){2} /\
Hmem.ystar{2} = (rsap Hmem.pk Hmem.xstar){2} ==>
={glob Hmap, glob Gmap, res}.
proof.
proc.
sp; if=> //.
seq 1 1: (={glob Hmap, glob Gmap, u, ho, c, m, r} /\
(c{1} = Adv => invertible Hmem.pk{2} Hmem.xstar{2}) /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
valid_keys (Hmem.pk,Hmem.sk){2} /\
z{2} = (simul Hmem.pk Hmem.sk (c = Adv) Hmem.xstar u){2} /\
w{2} = to_htag (sub (from_signature (i2osp z)) 1 kh){2} /\
st{2} = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg){2}).
inline Loop.sample; wp.
while (pk{1} = Hmem.pk{2} /\ sk{1} = Hmem.sk{2} /\ b{1} = (c{2} = Adv) /\
x{1} = Hmem.xstar{2} /\ u0{1} = u{2} /\ z0{1} = z{2} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
b{2} = 0 <= z{2} < 2^(k - 1) /\
(0 <= z{2} < 2^(k - 1) =>
z{2} = (simul Hmem.pk Hmem.sk (c = Adv) Hmem.xstar u){2} /\
w{2} = to_htag (sub (from_signature (i2osp z)) 1 kh){2} /\
st{2} = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg){2})).
auto; progress; first last; last 2 smt.
by cut:= H4; rewrite /simul; smt.
by wp; skip; progress; expect 8 smt.
seq 4 1: (={glob Hmap, glob Gmap, u, ho, c, z, w, st, m, r});
first by wp.
by sim.
qed.
local equiv Game3'1Loop_3'2: Gen1(GAdv3,GenH3(Loop),G1).main ~ Game3'2.main:
={glob A} ==> ={res}.
proof.
proc; seq 3 3: (={glob A, glob Hmap, glob Gmap, keys} /\
keys{2} = (Hmem.pk,Hmem.sk){2} /\
valid_keys (Hmem.pk,Hmem.sk){2} /\
rsap_dom Hmem.pk{2} Hmem.xstar{2} /\
Hmem.ystar{2} = (rsap Hmem.pk Hmem.xstar){2}).
by inline*; auto; smt.
inline*; auto.
call (_: ={glob Hmap, glob Gmap, glob Mem} /\
support keypairs (Hmem.pk,Hmem.sk){2} /\
rsap_dom Hmem.pk{2} Hmem.xstar{2} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
Mem.pk{2} = Hmem.pk{2}).
proc; inline GAdv3(GenH3(Loop),G1).Hs.o GAdv3(H3'2,G1).Hs.o; sp; if=> //.
wp; call GenH3Loop_H3'2.
by auto.
by proc; inline*; sp; if=> //; auto.
by proc; sp; if=> //; wp; call GenH3Loop_H3'2; auto.
by auto.
qed.
(** We stop the loop early to ensure that the simulator is p.p.t. *)
local module H3'3: SplitOracle1 = {
var bad:bool
proc init(ks:keypair): unit = {
Hmap.init(ks);
bad = false;
}
proc o(c:caller,m:message,r:salt): (htag * gtag) option = {
var w, st, u, z, ho, i, b;
u = 0;
z = 2^k - 1;
i = 0;
ho = None;
w = witness;
st = witness;
b = false;
if (invertible Hmem.pk Hmem.xstar \/ c <> Adv) {
while (!b /\ i < k0 + 1) {
u = $challenge Hmem.pk;
z = if c = Adv
then (Hmem.ystar ** (rsap Hmem.pk u)) Hmem.pk
else rsap Hmem.pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
b = b \/ 0 <= z < 2^(k - 1);
i = i + 1;
}
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (0 <= z < 2^(k - 1) /\ (c <> Adv \/ invertible Hmem.pk u)) {
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,u);
Gmap.m.[w] = (st,c);
}
ho = Some (w,st);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
} else bad = true;
}
return ho;
}
proc v(m:message,r:salt):htag = {
var h;
h = $htag;
if (mem (m,r) (dom Hmap.m)) h = pi3_1 (oget Hmap.m.[(m,r)]);
return h;
}
}.
local module Game3'3 = Gen1(GAdv3,H3'3,G1).
local equiv Game3'2_3'3_H: H3'2.o ~ H3'3.o:
!H3'3.bad{2} /\ ={glob Hmap, glob Gmap, c, m, r} /\
valid_keys (Hmem.pk,Hmem.sk){1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1} ==>
!H3'3.bad{2} => ={glob Hmap, glob Gmap, res}.
proof.
proc.
sp; if=> //.
splitwhile {1} 1 : (i < k0 + 1).
seq 1 1: (={glob Hmap, glob Gmap, u, z, i, ho, w, st, b, c, m, r} /\
valid_keys (Hmem.pk,Hmem.sk){1} /\
(c{1} = Adv => invertible Hmem.pk{1} Hmem.xstar{1}) /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1} /\
b{1} = 0 <= z{1} < 2^(k - 1)).
while (={Hmem.pk, Hmem.ystar, u, z, i, w, st, b, c} /\
b{1} = 0 <= z{1} < 2^(k - 1));
first by auto; progress; smt.
by auto; smt.
case (b{1}); first by rcondf{1} 1; auto; smt.
(** Reduce to proving termination of the remainder of the loop *)
wp; conseq (_: valid_keys (Hmem.pk,Hmem.sk){1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
(c{1} = Adv => invertible Hmem.pk{1} Hmem.xstar{1}) /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1} ==> true)
(_: valid_keys (Hmem.pk,Hmem.sk){1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
(c{1} = Adv => invertible Hmem.pk{1} Hmem.xstar{1}) /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1} ==>
true: =1%r)=> //; first smt.
while (valid_keys (Hmem.pk,Hmem.sk){1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
(c{1} = Adv => invertible Hmem.pk{1} Hmem.xstar{1}) /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1})
(if !b{1} then 1 else 0) 1 ((2^(k-1))%r/(p_n Hmem.pk)%r)=> //.
smt.
progress; seq 6: (valid_keys (Hmem.pk,Hmem.sk){1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
(c{1} = Adv => invertible Hmem.pk{1} Hmem.xstar{1}) /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1})=> //.
by auto; smt.
by hoare; auto.
by auto; smt.
split.
progress.
cut lt_div: forall (x y z:real), 0%r < z => x < y => x / z < y / z by smt.
cut pos_inv: forall x, 0%r < x => 0%r < 1%r/x.
by move=> x lt0x; cut ->: 0%r = 0%r/x; smt.
cut ->: forall x y, x / y = x * 1%r/y by smt.
cut pos_mul: forall x y, 0%r < x => 0%r < y => 0%r < x * y by smt.
apply (pos_mul ((2^(k-1))%r) (1%r/(p_n Hmem.pk{1})%r)); first smt.
smt.
move=> z; conseq (_: _: =((2^(k - 1))%r/(p_n Hmem.pk)%r)).
wp; rnd; skip; progress.
move: H2; rewrite -neqF=> -> //=.
cut ->: (fun x, (if !0 <= (if c{1} = Adv
then ((rsap Hmem.pk Hmem.xstar) ** (rsap Hmem.pk x)) Hmem.pk
else rsap Hmem.pk x)
< 2^(k - 1)
then 1 else 0) < 1){1} =
(fun x, (if (fun y, 0 <= simul Hmem.pk Hmem.sk (c = Adv) Hmem.xstar y < 2^(k - 1)){1} x
then 0 else 1) < 1){1}.
by rewrite /simul -fun_ext=> x //=; smt.
cut ->: forall (P:int -> bool), (fun x, (if P x then 0 else 1) < 1) = P.
by move=> P; apply fun_ext=> x /=; smt.
by apply mu_challenge_in_pim.
qed.
local equiv GenH3'2_Game3'3: Game3'2.main ~ Game3'3.main:
={glob A} ==> ={res} \/ H3'3.bad{2}.
proof.
proc.
seq 3 3: (={glob A, glob Hmap, glob Gmap, keys} /\
!H3'3.bad{2} /\
support keypairs keys{1} /\
support keypairs (Hmem.pk,Hmem.sk){1} /\
keys{1} = (Hmem.pk,Hmem.sk){1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1}).
by inline*; auto; smt.
inline*; auto.
call (_: H3'3.bad,
={glob Hmap, glob Gmap, glob Mem} /\
support keypairs (Hmem.pk,Hmem.sk){2} /\
rsap_dom Hmem.pk{2} Hmem.xstar{2} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
Mem.pk{2} = Hmem.pk{2},
={glob Hmem, Mem.pk} /\
support keypairs (Hmem.pk,Hmem.sk){2} /\
rsap_dom Hmem.pk{2} Hmem.xstar{2} /\
Hmem.ystar{2} = rsap Hmem.pk{2} Hmem.xstar{2} /\
Mem.pk{2} = Hmem.pk{2}).
by progress; apply (A_forge_ll H G O).
(* sign upto *)
proc; inline GAdv3(H3'2,G1).Hs.o GAdv3(H3'3,G1).Hs.o; sp; if=> //; auto.
call Game3'2_3'3_H.
by auto; smt.
(* Bad => sign{1} *)
progress; proc; inline GAdv3(H3'2,G1).Hs.o; sp; if=> //; auto.
call H3'2_o_ll.
by auto; smt.
(* Bad => sign{2} *)
progress; proc; inline*; sp; if=> //; rcondt 13; auto.
while (0 <= i <= k0 + 1 /\ valid_keys (Hmem.pk,Hmem.sk)) (k0 + 1 - i).
by progress; auto; smt.
by auto; smt.
(* Ga *)
by proc; inline *; sp; if=> //; auto.
by progress; proc; inline *; sp; if=> //; auto; smt.
by progress; proc; inline *; sp; if=> //; auto; smt.
(* Ha upto *)
proc; inline GAdv3(H3'2,G1).Ha.o GAdv3(H3'3,G1).Ha.o; sp; if=> //; auto.
call Game3'2_3'3_H.
by auto; smt.
(* Bad => Ha{1} *)
progress; proc; inline GAdv3(H3'2,G1).Ha.o; sp; if=> //; auto.
call H3'2_o_ll.
by auto; smt.
(* Bad => Ha{2} *)
progress; proc; inline*; sp; if=> //; sp; if=> //; auto.
while (0 <= i <= k0 + 1 /\ valid_keys (Hmem.pk,Hmem.sk)) (k0 + 1 - i).
by progress; auto; smt.
by auto; smt.
by auto; smt.
qed.
(* computing the probability of bad in Game3'3 (a call to H fails to sample a valid
signature in k0 + 1 attempts) *)
local module H3'3bad: SplitOracle1 = {
var cH:int
proc init(ks:keypair): unit = {
Hmap.init(ks);
H3'3.bad = false;
cH = 0;
}
proc o(c:caller,m:message,r:salt): (htag * gtag) option = {
var w, st, u, z, ho, i, b;
u = 0;
z = 2^k - 1;
i = 0;
ho = None;
w = witness;
st = witness;
b = false;
if (cH < qH + qS) {
if (Hmem.ystar = rsap Hmem.pk Hmem.xstar /\ support keypairs (Hmem.pk, Hmem.sk) /\
rsap_dom Hmem.pk Hmem.xstar /\
(invertible Hmem.pk Hmem.xstar \/ c <> Adv)) {
while (!b /\ i < k0 + 1) {
u = $challenge Hmem.pk;
z = if c = Adv
then (Hmem.ystar ** (rsap Hmem.pk u)) Hmem.pk
else rsap Hmem.pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
b = b \/ 0 <= z < 2^(k - 1);
i = i + 1;
}
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (0 <= z < 2^(k - 1) /\ (c <> Adv \/ invertible Hmem.pk u)) {
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,u);
Gmap.m.[w] = (st,c);
}
ho = Some (w,st);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
} else H3'3.bad = true;
}
cH = cH + 1;
}
return ho;
}
proc v = H3'3.v
}.
local module Game3'3bad = Gen1(GAdv3,H3'3bad,G1).
local equiv H3'3o : H3'3.o ~ H3'3bad.o :
={arg, glob Hmap, glob Gmap, H3'3.bad} /\
(Hmem.ystar = rsap Hmem.pk Hmem.xstar){2} /\ support keypairs (Hmem.pk, Hmem.sk){2} /\
(rsap_dom Hmem.pk Hmem.xstar){2} /\
(H3'3bad.cH = Mem.cH + Mem.cS){2} /\ (Mem.cH + Mem.cS){2} < qH + qS ==>
={res,glob Hmap, glob Gmap, H3'3.bad} /\ (H3'3bad.cH = Mem.cH + Mem.cS + 1){2}.
proof.
proc;inline *;sp;rcondt{2} 1; first by move=> _;skip;progress.
if => //;last by auto.
wp 3 3; conseq (_: _ ==> ={ho,glob Hmap, glob Gmap, H3'3.bad}) => //;sim.
qed.
local lemma Game3'3_3'3bad &m:
Pr[Game3'3.main() @ &m: H3'3.bad] =
Pr[Game3'3bad.main() @ &m: H3'3.bad /\ H3'3bad.cH <= qH + qS].
proof.
byequiv (_: ={glob A} ==> ={H3'3.bad} /\ H3'3bad.cH{2} <= qH + qS) => //;proc.
inline Gen1(GAdv3, H3'3, G1).GA.main Gen1(GAdv3, H3'3bad, G1).GA.main.
seq 6 6 : (={m,s,glob A, glob Hmap, glob Gmap, glob Mem, H3'3.bad} /\
(Hmem.ystar = rsap Hmem.pk Hmem.xstar){2} /\ support keypairs (Hmem.pk, Hmem.sk){2} /\
(rsap_dom Hmem.pk Hmem.xstar){2} /\ H3'3bad.cH{2} <= qH + qS);
last by sim (: ={glob Hmap, glob Gmap, glob Mem}) /(H3'3bad.cH{2} <= qH + qS) : (={H3'3.bad}).
call (_: ={glob Hmap, glob Gmap, glob Mem, H3'3.bad} /\
(Hmem.ystar = rsap Hmem.pk Hmem.xstar){2} /\ support keypairs (Hmem.pk, Hmem.sk){2} /\
(rsap_dom Hmem.pk Hmem.xstar){2} /\
(H3'3bad.cH = Mem.cH + Mem.cS){2} /\ Mem.cH{2} <= qH /\ Mem.cS{2} <= qS).
proc;sp;if => //;wp; inline GAdv3(H3'3, G1).Hs.o GAdv3(H3'3bad, G1).Hs.o;wp.
call H3'3o;wp;rnd;skip;progress;smt.
by sim (: ={glob Gmap}) / ((Hmem.ystar = rsap Hmem.pk Hmem.xstar){2} /\ support keypairs (Hmem.pk, Hmem.sk){2} /\
(rsap_dom Hmem.pk Hmem.xstar){2} /\
H3'3bad.cH{2} = Mem.cH{2} + Mem.cS{2} /\ Mem.cH{2} <= qH /\ Mem.cS{2} <= qS) :
(={res,glob Hmap, glob Gmap, glob Mem, H3'3.bad}).
by proc;sp;if => //;wp;call H3'3o;skip;progress;smt.
inline *;auto;progress. smt. smt. smt. smt. smt. smt.
qed.
(* computing the probability of bad in Game3'3 (a call to H fails to sample a valid
signature in k0 + 1 attempts) *)
local lemma Game3'3'bad &m:
Pr[Game3'3bad.main() @ &m: H3'3.bad /\ H3'3bad.cH <= qH + qS] <= (qH + qS)%r * 1%r/(2^(k0+1))%r.
proof.
fel 3 (H3'3bad.cH)
(fun x, 1%r/ (2^(k0+1))%r)
(qH + qS)
(H3'3.bad)
[H3'3bad.o: (H3'3bad.cH < qH + qS)] => //.
rewrite /int_sum (Monoid.Mrplus.NatMul.sum_const (1%r /(2^(k0 + 1))%r)) //.
rewrite /intval card_interval_max (_: qH + qS - 1 - 0 + 1 = qH + qS); first smt.
rewrite /max (_: qH + qS < 0 = false) /=; first smt.
by rewrite /Monoid.Mrplus.NatMul.( * ); smt.
by inline *;auto.
cut Hpos : (0%r <= 1%r / (2 ^ (k0+1))%r).
cut lt_div: forall (x y z:real), 0%r < z => x < y => x / z < y / z by smt.
cut pos_inv: forall x, 0%r < x => 0%r < 1%r/x.
by move=> x lt0x; cut ->: 0%r = 0%r/x; smt.
cut pos_mul: forall x y, 0%r < x => 0%r < y => 0%r < x * y by smt.
smt.
proc;sp;if;last by hoare.
if;last by hoare;auto.
wp => /=;simplify.
conseq (_: _ ==> !b : <= (1%r/(2^(k0+1-i))%r))
(_: _ ==> (0 <= z < 2 ^ (k - 1) /\ (c <> Adv \/ invertible Hmem.pk u)) <=> b)=> //.
by while (0 <= z < 2 ^ (k - 1) => b); auto;smt.
by progress; rewrite -not_def=> /H11.
while (0 <= i <= k0 + 1 /\ (c = Adv => invertible Hmem.pk Hmem.xstar) /\
rsap_dom Hmem.pk Hmem.xstar /\
Hmem.ystar = rsap Hmem.pk Hmem.xstar /\ support keypairs (Hmem.pk, Hmem.sk)) => //.
move=> Hrec;exists * i;elim * => i0.
seq 6 : (!b) (1%r/2%r) (1%r / (2 ^ (k0+1 - (i0 + 1)))%r) _ 0%r
(i = i0 + 1 /\ 0 <= i0 <= k0 /\ (c = Adv => invertible Hmem.pk Hmem.xstar) /\
rsap_dom Hmem.pk Hmem.xstar /\
Hmem.ystar = rsap Hmem.pk Hmem.xstar /\ support keypairs (Hmem.pk, Hmem.sk)) => //;first by auto;smt.
wp => /=;rnd;skip;progress.
rewrite (_:b{hr} = false)=> /=;first by smt.
cut -> : ((fun (x:int),
! 0 <= (if c{hr} = Adv then ( ** ) (rsap Hmem.pk{hr} Hmem.xstar{hr}) (rsap Hmem.pk{hr} x) Hmem.pk{hr}
else rsap Hmem.pk{hr} x) < 2 ^ (k - 1)) =
(!(fun (x:int), 0 <= simul Hmem.pk{hr} Hmem.sk{hr} (c{hr} = Adv) Hmem.xstar{hr} x < 2^(k-1)))).
by apply fun_ext => x;rewrite /Pred.([!]) /simul.
rewrite mu_not (_ : mu (challenge Hmem.pk{hr}) True = 1%r);first by smt.
cut -> := mu_challenge_in_pim Hmem.pk{hr} Hmem.sk{hr} (c{hr} = Adv) Hmem.xstar{hr} _ _ _ => //.
cut : (1%r/2%r <= (2 ^ (k - 1))%r / (p_n Hmem.pk{hr})%r); last smt.
apply (_:forall x1 x2 y1 y2, 0%r < y1 => 0%r < y2 => x1 * y2 <= x2 * y1 => x1/y1 <= x2/y2) => //=.
move=> x1 x2 y1 y2 Hy1 Hy2 Hm.
apply (_: forall (x y z:real), 0%r < z => x*z <= y => x <= y / z) => //; first by smt.
by cut -> : ((x1 / y1) * y2 = (x1*y2) / y1);smt.
by smt.
rewrite {2} (_:2 = 2^1); first by rewrite (_: 1 = 0 + 1) // powS // pow0.
rewrite (_:(2 ^ (k - 1))%r * (2 ^ 1)%r = (2 ^ (k - 1) * 2 ^ 1)%r); first smt.
by rewrite pow_add //;smt.
by conseq Hrec => //;smt.
rcondf 1 => //;first by auto;smt.
by hoare.
progress.
rewrite (_ : (2%r * (2 ^ (k0 + 1 - (i{hr} + 1)))%r) = (2 ^ (k0 + 1 - i{hr}))%r) //.
rewrite {1}(_: 2 = (2^1)); first by rewrite (_: 1 = 0 + 1) // powS // pow0.
cut ->: (2^1)%r * (2 ^ (k0 + 1 - (i{hr} + 1)))%r = (2^1 * 2^(k0 + 1 - (i{hr} + 1)))%r.
smt.
by rewrite pow_add //;smt.
by skip;smt.
by move=> c;proc;sp;rcondt 1 => //;wp;conseq (_ : _ ==> true)=> //;smt.
by move=> b c;proc;sp;rcondf 1.
qed.
(* end of computation *)
local lemma Game3'2_3'3 &m:
Pr[Game3'2.main() @ &m: res]
<= Pr[Game3'3.main() @ &m: res]
+ (qH + qS)%r * 1%r/(2^(k0+1))%r.
proof.
cut: Pr[Game3'2.main() @ &m: res] <= Pr[Game3'3.main() @ &m: res \/ H3'3.bad].
by byequiv GenH3'2_Game3'3=> //; smt.
rewrite Pr [mu_or].
rewrite (Game3'3_3'3bad &m).
cut := Game3'3'bad &m; smt.
qed.
(** Game4: Minor cleanup to facilitate the reduction *)
local module H4: SplitOracle1 = {
proc init = Hmap.init
proc o(c:caller,m:message,r:salt): (htag * gtag) option = {
var w, st, u, z, ho, i;
u = 0;
z = 2^k - 1;
i = 0;
ho = None;
w = witness;
st = witness;
if (invertible Hmem.pk Hmem.xstar \/ c <> Adv) {
while (!0 <= z < 2^(k - 1) /\ i < k0 + 1) {
u = $challenge Hmem.pk;
z = if c = Adv
then (Hmem.ystar ** (rsap Hmem.pk u)) Hmem.pk
else rsap Hmem.pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
i = i + 1;
}
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (0 <= z < 2^(k - 1) /\ (c <> Adv \/ invertible Hmem.pk u)) {
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,c,u);
Gmap.m.[w] = (st,c);
}
ho = Some (w,st);
} else {
w = oget (omap pi3_1 Hmap.m.[(m,r)]);
ho = if c = Adv then Some(w,witness) else None;
}
}
}
return ho;
}
proc v(m:message,r:salt):htag = {
var h;
h = $htag;
if (mem (m,r) (dom Hmap.m)) h = pi3_1 (oget Hmap.m.[(m,r)]);
return h;
}
}.
local module Game4 = Gen1(GAdv3,H4,G1).
local lemma Game3'3_4 &m: Pr[Game3'3.main() @ &m: res] = Pr[Game4.main() @ &m: res].
proof.
byequiv (_: ={glob A} ==> ={res})=> //.
proc; inline *; auto.
call (_: ={glob Mem, glob Hmap, glob Gmap}).
proc; inline *; sp; if=> //.
rcondt{1} 13; first by auto.
rcondt{2} 12; first by auto.
wp; while (={glob Hmap, z, i, u, w0, st, c} /\
0 <= i{1} <= k0 + 1 /\
b{1} = (0 <= z{2} < 2^(k - 1))).
by auto; progress; expect 5 smt.
by auto; progress; expect 4 smt.
by proc; inline *; sp; if=> //; auto; smt.
proc; inline *; sp; if=> //; case (!invertible Hmem.pk{1} Hmem.xstar{1}).
rcondf{1} 11; first by auto.
rcondf{2} 10; first by auto.
by auto.
rcondt{1} 11; first by auto.
rcondt{2} 10; first by auto.
wp; while (={glob Hmap, z, i, u, w, st, c} /\
0 <= i{1} <= k0 + 1 /\
b{1} = (0 <= z{2} < 2^(k - 1))).
by auto; progress; expect 5 smt.
by auto; progress; expect 4 smt.
by auto.
qed.
(**** Current status *)
local lemma Game3_4 &m:
Pr[Game3.main() @ &m: res]
<= Pr[Game4.main() @ &m: res]
+ qH%r * 1%r/(2^(k /% 2 - 1))%r
+ (qH + qS)%r * 1%r/(2^(k0+1))%r.
proof.
rewrite -(Game3'3_4 &m).
cut: Pr[Game3.main() @ &m: res]
<= Pr[Game3'1.main() @ &m: res]
+ qH%r * 1%r/(2^(k /% 2 - 1))%r.
cut: Pr[Game3.main() @ &m: res]
<= Pr[Game3'1.main() @ &m: res \/ H3'1.bad].
by byequiv Game3_3'1=> //; smt.
rewrite Pr [mu_or].
cut ->: Pr[Game3'1.main() @ &m: H3'1.bad]
= Pr[Game3'1'bad.main() @ &m: H3'1.bad /\ Mem.cH <= qH]
by byequiv Game3'1_3'1'bad.
by cut:= Pr_Game3'1'bad &m; smt.
cut ->: Pr[Game3'1.main() @ &m: res]
= Pr[Gen1(GAdv3,GenH3(Direct),G1).main() @ &m: res].
by byequiv Game3'1_Direct.
rewrite (GameH3Direct_Loop &m).
cut ->: Pr[Gen1(GAdv3,GenH3(Loop),G1).main() @ &m: res]
= Pr[Game3'2.main() @ &m: res].
by byequiv Game3'1Loop_3'2.
cut:= Game3'2_3'3 &m.
smt.
qed.
local lemma PSS96_Game4 &m:
Pr[UF_CMA(Wrap(PSS96(H,G)),Bounded_PSS_Adv(A,H,G)).main() @ &m: res]
<= Pr[Game4.main() @ &m: res]
+ (qS + qH)%r * (qS + qH + qG - 1)%r / (2^kh)%r
+ qS%r * (qS + qH)%r / (2^k0)%r
+ 1%r / (2^(k /% 2 - 2))%r
+ qH%r * 1%r/(2^(k /% 2 - 1))%r
+ (qH + qS)%r * 1%r/(2^(k0+1))%r.
proof.
cut:= PSS96_Game2 &m.
rewrite (Game2_3 &m).
smt.
qed.
(** We now build the inverter. Note that we now check whether ystar is
invertible (not xstar) before doing computations in H *)
local module LocalInverter(A:PSS_AdvCMA): RSA.Inverter = {
module G = {
proc o(w:htag): gtag = {
var r;
r = $gtag;
if (!mem w (dom Gmap.m)) Gmap.m.[w] = (r,Adv);
return fst (oget Gmap.m.[w]);
}
}
module Ga = {
proc o(w:htag): gtag = {
var r;
if (Mem.cG < qG) {
r = G.o(w);
Mem.cG = Mem.cG + 1;
}
else r = witness;
return r;
}
}
module Ha = {
proc o(mr:message * salt): htag = {
var m, r, w, st, u, z, i;
(m,r) = mr;
u = 0;
w = witness;
st = witness;
i = 0;
z = 2^k - 1;
if (Mem.cH < qH) {
if (invertible Hmem.pk Hmem.ystar) {
while (!0 <= z < 2^(k - 1) /\ i < k0 + 1) {
u = $challenge Hmem.pk;
z = (Hmem.ystar ** (rsap Hmem.pk u)) Hmem.pk;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
i = i + 1;
}
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (0 <= z < 2^(k - 1) /\ invertible Hmem.pk u) {
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,Adv,u);
Gmap.m.[w] = (st,Adv);
}
} else
w = pi3_1 (oget Hmap.m.[(m,r)]);
} else
w = witness;
}
Mem.cH = Mem.cH + 1;
}
return w;
}
}
module S = {
proc sign(m:message): signature = {
var r, w, st, u, z, i, s;
s = witness;
i = 0;
z = 2^k - 1;
r = $salt;
u = 0;
w = witness;
st = witness;
if (Mem.cS < qS) {
while (!0 <= z < 2^(k - 1) /\ i < k0 + 1) {
u = $challenge Hmem.pk;
z = rsap Hmem.pk u;
w = to_htag (sub (from_signature (i2osp z)) 1 kh);
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg);
i = i + 1;
}
st = st ^ (to_gtag (from_salt r || zeros (kg - k0)));
if (0 <= z < 2^(k - 1)) {
if (!mem (m,r) (dom Hmap.m)) {
if (!mem w (dom Gmap.m)) {
Hmap.m.[(m,r)] = (w,Sig,u);
Gmap.m.[w] = (st,Sig);
}
s = i2osp u;
}
}
Mem.cS = Mem.cS + 1;
}
return s;
}
}
module A = A(Ha,Ga,S)
proc invert(pk:pkey, c:int): int = {
var m, s, y, w, st, w', st', r, c', u, x;
Hmap.m = FMap.empty;
Hmem.pk = pk;
Hmem.ystar = c;
Gmap.m = FMap.empty;
Mem.cS = 0;
Mem.cG = 0;
Mem.cH = 0;
Mem.qs = FSet.empty;
u = 1;
(m,s) = A.forge(pk);
y = from_signature (i2osp (rsap pk (os2ip s)));
w = to_htag (sub y 1 kh);
st = to_gtag (sub y (1 + kh) kg);
st' = G.o(w);
r = to_salt (sub (from_gtag (st ^ st')) 0 k0);
w' = $htag;
if (mem (m,r) (dom Hmap.m))
(w',c',u) = oget Hmap.m.[(m,r)];
x = ((os2ip s) ** (inv pk u)) pk;
return x;
}
}.
local equiv SignEq: GAdv3(H4,G1).S.sign ~ LocalInverter(A).S.sign:
={glob Gmap, Hmap.m, Mem.cS, Hmem.pk, Hmem.ystar, m} /\
valid_keys (Hmem.pk,Mem.sk){1} /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1} ==>
={glob Gmap, Hmap.m, Mem.cS, res}.
proof.
proc.
case (Mem.cS{1} < qS).
rcondt{1} 2; first by auto.
rcondt{2} 8; first by auto.
inline GAdv3(H4,G1).Hs.o H4.o.
rcondt{1} 13; first by auto.
wp; while (={Hmem.pk, s, r, u, m, st, z, i} /\
w0{1} = w{2} /\
c{1} = Sig /\
rsap_dom Hmem.pk{2} u{2} /\
valid_keys (Hmem.pk,Mem.sk){1} /\
(0 <= z{1} < 2^(k - 1) =>
z{2} = rsap Hmem.pk{2} u{2} /\
w{2} = to_htag (sub (from_signature (i2osp z)) 1 kh){2} /\
st{2} = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg)){2}).
by auto; progress; expect 2 smt.
auto; progress; first 4 smt.
rewrite /oget /snd /= -xorwA xorwK xorw0.
cut:= H7 _=> // [[->]] [->] ->; rewrite /from_signature /to_signature.
rewrite /from_htag /to_htag HTag.pcan_to_from; first smt.
rewrite /from_gtag /to_gtag GTag.pcan_to_from; first smt.
cut ->: (sub (to_bits (i2osp (rsap Hmem.pk u_R))){2} 1 kh ||
sub (to_bits (i2osp (rsap Hmem.pk u_R))){2} (1 + kh) kg) =
sub (to_bits (i2osp (rsap Hmem.pk u_R))){2} 1 (kh + kg)
by smt.
cut:= msb0_bnd (i2osp (rsap Hmem.pk{2} u_R)); rewrite /from_signature; elim=> _ <-.
by rewrite pcan_os2ip_i2osp; smt.
cut ->: (sub (to_bits (i2osp (rsap Hmem.pk u_R))){2} 0 1 ||
sub (to_bits (i2osp (rsap Hmem.pk u_R))){2} 1 (kh + kg)) =
to_bits (i2osp (rsap Hmem.pk u_R)){2}
by smt.
rewrite Signature.can_from_to pcan_os2ip_i2osp; first smt.
by rewrite rsas_rsap; first 2 smt.
smt.
smt.
smt.
rewrite /oget /snd /= -xorwA xorwK xorw0.
cut:= H7 _=> // [[->]] [->] ->; rewrite /from_signature /to_signature.
rewrite /from_htag /to_htag HTag.pcan_to_from; first smt.
rewrite /from_gtag /to_gtag GTag.pcan_to_from; first smt.
cut ->: (sub (to_bits (i2osp (rsap Hmem.pk u_R))){2} 1 kh ||
sub (to_bits (i2osp (rsap Hmem.pk u_R))){2} (1 + kh) kg) =
sub (to_bits (i2osp (rsap Hmem.pk u_R))){2} 1 (kh + kg)
by smt.
cut:= msb0_bnd (i2osp (rsap Hmem.pk{2} u_R)); rewrite /from_signature; elim=> _ <-.
by rewrite pcan_os2ip_i2osp; smt.
cut ->: (sub (to_bits (i2osp (rsap Hmem.pk u_R))){2} 0 1 ||
sub (to_bits (i2osp (rsap Hmem.pk u_R))){2} 1 (kh + kg)) =
to_bits (i2osp (rsap Hmem.pk u_R)){2}
by smt.
rewrite Signature.can_from_to pcan_os2ip_i2osp; first smt.
by rewrite rsas_rsap; first 2 smt.
smt.
smt.
smt.
smt.
smt.
by rcondf{1} 2; [auto | rcondf{2} 8; auto]; progress; smt.
qed.
local hoare SignInv: GAdv3(H4,G1).S.sign:
valid_keys (Hmem.pk,Hmem.sk) /\
Hmem.ystar = rsap Hmem.pk Hmem.xstar /\
Hmem.pk = Mem.pk /\
Hmem.sk = Mem.sk /\
rsap_dom Hmem.pk Hmem.xstar /\
(forall m r,
mem (m,r) (dom Hmap.m) =>
let (w,c,u) = oget Hmap.m.[(m,r)] in
mem w (dom Gmap.m) /\
rsap_dom Hmem.pk u /\
let (st,c') = oget Gmap.m.[w] in
c = c' /\
(c = Adv =>
invertible Hmem.pk u /\
let y = (Hmem.ystar ** rsap Hmem.pk u) Hmem.pk in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs)) ==>
(forall m r,
mem (m,r) (dom Hmap.m) =>
let (w,c,u) = oget Hmap.m.[(m,r)] in
mem w (dom Gmap.m) /\
rsap_dom Hmem.pk u /\
let (st,c') = oget Gmap.m.[w] in
c = c' /\
(c = Adv =>
invertible Hmem.pk u /\
let y = (Hmem.ystar ** rsap Hmem.pk u) Hmem.pk in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs)).
proof.
proc; sp; if=> //.
inline GAdv3(H4,G1).Hs.o H4.o.
rcondt 12; first by auto.
seq 12: (c = Sig /\ m = m1 /\ r = r1 /\
s = witness /\ ho = None /\
valid_keys (Hmem.pk,Hmem.sk) /\
Hmem.ystar = rsap Hmem.pk Hmem.xstar /\
Hmem.pk = Mem.pk /\
Hmem.sk = Mem.sk /\
rsap_dom Hmem.pk Hmem.xstar /\
(0 <= z < 2^(k - 1) => rsap_dom Hmem.pk u) /\
(forall m r,
mem (m,r) (dom Hmap.m) =>
let (w,c,u) = oget Hmap.m.[(m,r)] in
mem w (dom Gmap.m) /\
rsap_dom Hmem.pk u /\
let (st,c') = oget Gmap.m.[w] in
c = c' /\
(c = Adv =>
invertible Hmem.pk u /\
let y = (Hmem.ystar ** rsap Hmem.pk u) Hmem.pk in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs)) /\
(0 <= z < 2^(k - 1) =>
z = rsap Hmem.pk u /\
zeros 1 = sub (from_signature (i2osp z)) 0 1 /\
w0 = to_htag (sub (from_signature (i2osp z)) 1 kh) /\
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg))).
while (c = Sig /\
valid_pkey Hmem.pk /\
(0 <= z < 2^(k - 1) =>
rsap_dom Hmem.pk u /\
z = rsap Hmem.pk u /\
zeros 1 = sub (from_signature (i2osp z)) 0 1 /\
w0 = to_htag (sub (from_signature (i2osp z)) 1 kh) /\
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg))).
by auto; progress; expect 3 smt.
by auto; progress; expect 12 smt.
sp 1; elim* => st0; if=> //; last by rcondt 3; auto.
if=> //; last by rcondt 5; auto.
if=> //; last first.
rcondf 4; first by auto.
wp; skip; progress [-split].
cut:= H2 m2 r2 _ => //; rewrite H9 /= => -[x1_in_G].
cut:= x1_in_G; rewrite mem_dom /oget; case (Gmap.m.[x1]{hr})=> //= [[w st]].
by progress; cut:= H12 _=> //; progress; rewrite mem_add; left.
rcondf 6; first by auto.
wp; skip; progress.
case ((m1,r1){hr} = (m2,r2)).
elim=> m_eq r_eq; subst; move: H9; rewrite get_set_eq /oget /= => -[->].
by rewrite mem_dom get_set_eq.
move=> neq; move: H9; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m2 r2 _=> //; rewrite hmr /=; progress.
by rewrite mem_dom get_set_neq 2:-mem_dom; first smt.
case ((m1,r1){hr} = (m2,r2)).
by elim=> m_eq r_eq; subst; move: H9; rewrite get_set_eq /oget /=; smt.
move=> neq; move: H9; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
by cut:= H2 m2 r2 _=> //; rewrite hmr /=; smt.
case ((m1,r1){hr} = (m2,r2)).
by elim=> m_eq r_eq; subst; move: H9; rewrite get_set_eq /oget /=; smt.
move=> neq; move: H9; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
by cut:= H2 m2 r2 _=> //; rewrite hmr /=; smt.
case ((m1,r1){hr} = (m2,r2)).
elim=> m_eq r_eq; subst; move: H9; rewrite get_set_eq /oget /= => -[w_eq] [c_eq u_eq]; subst.
by move: H10; rewrite get_set_eq /oget.
move=> neq; move: H9; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m2 r2 _=> //; rewrite hmr /=; progress.
move: H10 H11; rewrite get_set_neq; first smt.
by move=> -> /=.
move: H9; case ((m1,r1){hr} = (m2,r2)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget.
move=> neq; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m2 r2 _=> //; rewrite hmr /=; progress.
move: H10 H11; rewrite get_set_neq; first smt.
by move=> -> /=; smt.
move: H9; case ((m1,r1){hr} = (m2,r2)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget.
move=> neq; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m2 r2 _=> //; rewrite hmr /=; progress.
move: H10 H11; rewrite get_set_neq; first smt.
by move=> -> /=; smt.
move: H9; case ((m1,r1){hr} = (m2,r2)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget.
move=> neq; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m2 r2 _=> //; rewrite hmr /=; progress.
move: H10 H11; rewrite get_set_neq; first smt.
by move=> -> /=; smt.
move: H9; case ((m1,r1){hr} = (m2,r2)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget.
move=> neq; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m2 r2 _=> //; rewrite hmr /=; progress.
move: H10 H11; rewrite get_set_neq; first smt.
by move=> ->.
move: H9; case ((m1,r1){hr} = (m2,r2)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget /= => -[w_eq u_eq]; subst; smt.
move=> neq; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m2 r2 _=> //; rewrite hmr /=; progress.
move: H10 H11; rewrite get_set_neq; first smt.
by move=> ->.
move: H9; case ((m1,r1){hr} = (m2,r2)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget /= => -[w_eq u_eq]; subst; smt.
move=> neq; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m2 r2 _=> //; rewrite hmr /=; progress.
move: H10 H11; rewrite get_set_neq; first smt.
by move=> ->.
move: H9; case ((m1,r1){hr} = (m2,r2)).
elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget /= => -[w_eq u_eq]; subst.
move: H10; rewrite get_set_eq /oget /= => -[st_eq c'_eq]; subst.
by rewrite -xorwA xorwK xorw0; smt.
move=> neq; rewrite get_set_neq // => hmr.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m2 r2 _=> //; rewrite hmr /=; progress.
move: H10 H11; rewrite get_set_neq; first smt.
by move=> ->.
rewrite /oget /= -xorwA xorwK xorw0.
case ((m1,r1){hr} = (m2,r2)).
elim=> [m_eq r_eq]; subst; move: H9; rewrite get_set_eq /oget /= => -[w_eq u_eq]; subst.
move: H10; rewrite get_set_eq /oget /= => -[st_eq c'_eq]; subst.
cut:= H3 _; first by split.
move=> [z_def [-> [-> ->]]].
rewrite /to_htag /from_htag HTag.pcan_to_from; first smt.
rewrite /to_gtag /from_gtag GTag.pcan_to_from; first smt.
cut ->: (sub (from_signature (i2osp z)) 0 1 ||
sub (from_signature (i2osp z)) 1 kh ||
sub (from_signature (i2osp z)) (1 + kh) kg){hr} =
from_signature (i2osp z){hr}.
cut ->: (sub (from_signature (i2osp z)) 1 kh ||
sub (from_signature (i2osp z)) (1 + kh) kg){hr} =
sub (from_signature (i2osp z)){hr} 1 (kh + kg)
by smt.
smt.
rewrite /to_signature /from_signature Signature.can_from_to.
rewrite pcan_os2ip_i2osp; first smt.
by rewrite z_def rsas_rsap; smt.
move=> neq.
move: H8; rewrite mem_dom get_set_neq // -mem_dom=> dmrh.
move: H9; rewrite get_set_neq // => hmr.
cut:= H2 m2 r2 _ => //; rewrite hmr /=; progress.
move: H10 H11; rewrite get_set_neq; first smt.
move=> -> //=.
by rewrite mem_add; progress; left.
qed.
local equiv HaEq: GAdv3(H4,G1).Ha.o ~ LocalInverter(A).Ha.o:
={glob Gmap, Hmap.m, Mem.cH, Hmem.pk, Hmem.ystar} /\ m{1} = mr{2} /\
valid_keys (Hmem.pk,Mem.sk){1} /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1} ==>
={glob Gmap, Hmap.m, Mem.cH, res}.
proof.
proc; sp; if=> //.
inline H4.o.
case (!invertible Hmem.pk{1} Hmem.xstar{1}).
rcondf{1} 10; first by auto.
rcondf{2} 1; first by auto; progress; smt.
by auto.
rcondt{1} 10; first by auto.
rcondt{2} 1; first by auto; smt.
seq 10 1: (={glob Gmap, Hmap.m, Mem.cH, Hmem.pk, Hmem.ystar, u, w, st, z} /\
m{1} = (m0,r0){1} /\ m{1} = (m,r){2} /\
ho{1} = None /\
c{1} = Adv /\
valid_keys (Hmem.pk,Mem.sk){1} /\
(0 <= z{1} < 2^(k - 1) =>
rsap_dom Hmem.pk{2} u{2} /\
z{2} = (Hmem.ystar ** (rsap Hmem.pk u)){2} Hmem.pk{2} /\
w{2} = to_htag (sub (from_signature (i2osp z)) 1 kh){2} /\
st{2} = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg)){2}).
while (={Hmem.pk, Hmem.ystar, u, w, st, z, i} /\
c{1} = Adv /\
rsap_dom Hmem.pk{2} u{2} /\
valid_keys (Hmem.pk,Mem.sk){1} /\
(0 <= z{1} < 2^(k - 1) =>
z{2} = (Hmem.ystar ** (rsap Hmem.pk u)){2} Hmem.pk{2} /\
w{2} = to_htag (sub (from_signature (i2osp z)) 1 kh){2} /\
st{2} = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg)){2}).
by auto; progress; expect 2 smt.
by auto; progress; expect 7 smt.
sp 1 1; elim* => st0 st1.
if=> //; last by auto.
if=> //; last by auto; progress; smt.
if=> //; last by auto.
by wp.
qed.
local hoare HaInv: GAdv3(H4,G1).Ha.o:
valid_keys (Hmem.pk,Hmem.sk) /\
Hmem.ystar = rsap Hmem.pk Hmem.xstar /\
Hmem.pk = Mem.pk /\
Hmem.sk = Mem.sk /\
rsap_dom Hmem.pk Hmem.xstar /\
(forall m r,
mem (m,r) (dom Hmap.m) =>
let (w,c,u) = oget Hmap.m.[(m,r)] in
mem w (dom Gmap.m) /\
rsap_dom Hmem.pk u /\
let (st,c') = oget Gmap.m.[w] in
c = c' /\
(c = Adv =>
invertible Hmem.pk u /\
let y = (Hmem.ystar ** rsap Hmem.pk u) Hmem.pk in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs)) ==>
(forall m r,
mem (m,r) (dom Hmap.m) =>
let (w,c,u) = oget Hmap.m.[(m,r)] in
mem w (dom Gmap.m) /\
rsap_dom Hmem.pk u /\
let (st,c') = oget Gmap.m.[w] in
c = c' /\
(c = Adv =>
invertible Hmem.pk u /\
let y = (Hmem.ystar ** rsap Hmem.pk u) Hmem.pk in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs)).
proof.
proc; sp; if=> //.
inline GAdv3(H4,G1).Hs.o H4.o.
case (!invertible Hmem.pk Hmem.xstar); first by rcondf 10; auto.
rcondt 10; first by auto.
seq 10: (c = Adv /\
ho = None /\
valid_keys (Hmem.pk,Hmem.sk) /\
Hmem.ystar = rsap Hmem.pk Hmem.xstar /\
Hmem.pk = Mem.pk /\
Hmem.sk = Mem.sk /\
rsap_dom Hmem.pk Hmem.xstar /\
(0 <= z < 2^(k - 1) => rsap_dom Hmem.pk u) /\
(forall m r,
mem (m,r) (dom Hmap.m) =>
let (w,c,u) = oget Hmap.m.[(m,r)] in
mem w (dom Gmap.m) /\
rsap_dom Hmem.pk u /\
let (st,c') = oget Gmap.m.[w] in
c = c' /\
(c = Adv =>
invertible Hmem.pk u /\
let y = (Hmem.ystar ** rsap Hmem.pk u) Hmem.pk in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs)) /\
(0 <= z < 2^(k - 1) =>
z = (Hmem.ystar ** rsap Hmem.pk u) Hmem.pk /\
zeros 1 = sub (from_signature (i2osp z)) 0 1 /\
w = to_htag (sub (from_signature (i2osp z)) 1 kh) /\
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg))).
while (c = Adv /\
(0 <= z < 2^(k - 1) =>
rsap_dom Hmem.pk u /\
z = (Hmem.ystar ** rsap Hmem.pk u) Hmem.pk /\
zeros 1 = sub (from_signature (i2osp z)) 0 1 /\
w = to_htag (sub (from_signature (i2osp z)) 1 kh) /\
st = to_gtag (sub (from_signature (i2osp z)) (1 + kh) kg))).
by auto; progress; expect 3 smt.
by auto; progress; expect 11 smt.
sp 1; elim* => st0; if=> //; last by auto.
if=> //; last by auto.
if=> //; last by auto.
wp; skip; progress.
case ((m0,r0){hr} = (m1,r1)).
elim=> m_eq r_eq; subst; move: H10; rewrite get_set_eq /oget /= => -[->].
by rewrite mem_dom get_set_eq.
move=> neq; move: H10; rewrite get_set_neq // => hmr.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress.
by rewrite mem_dom get_set_neq 2:-mem_dom; first smt.
case ((m0,r0){hr} = (m1,r1)).
by elim=> m_eq r_eq; subst; move: H10; rewrite get_set_eq /oget; smt.
move=> neq; move: H10; rewrite get_set_neq //.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> H9 hmr.
by cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress; smt.
case ((m0,r0){hr} = (m1,r1)).
by elim=> m_eq r_eq; subst; move: H10; rewrite get_set_eq /oget; smt.
move=> neq; move: H10; rewrite get_set_neq //.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> H9 hmr.
by cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress; smt.
case ((m0,r0){hr} = (m1,r1)).
elim=> m_eq r_eq; subst; move: H10; rewrite get_set_eq /oget /= => -[w_eq [c_eq u_eq]]; subst.
by move: H11; rewrite get_set_eq /oget.
move=> neq; move: H10; rewrite get_set_neq // => hmr.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress.
move: H11 H12; rewrite get_set_neq; first smt.
by move=> ->.
move: H10; case ((m0,r0){hr} = (m1,r1)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget; cut:= H3 _.
move=> neq; rewrite get_set_neq // => hmr.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress.
move: H11 H12; rewrite get_set_neq; first smt.
by move=> ->.
move: H10; case ((m0,r0){hr} = (m1,r1)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget /= => -[w_eq u_eq]; subst; smt.
move=> neq; rewrite get_set_neq // => hmr.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress.
move: H11 H12; rewrite get_set_neq; first smt.
by move=> ->; rewrite /rsap_dom.
move: H10; case ((m0,r0){hr} = (m1,r1)).
elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget /= => -[w_eq u_eq]; subst.
move: H11; rewrite get_set_eq /oget /= => -[st_eq c'_eq]; subst.
by cut:= H3 _.
move=> neq; rewrite get_set_neq // => hmr.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress.
move: H11 H12; rewrite get_set_neq; first smt.
by move=> ->.
move: H10; case ((m0,r0){hr} = (m1,r1)).
elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget /= => -[w_eq u_eq]; subst.
move: H11; rewrite get_set_eq /oget /= => -[st_eq c'_eq]; subst.
by rewrite -xorwA xorwK xorw0; cut:= H3 _.
move=> neq; rewrite get_set_neq // => hmr.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress.
move: H11 H12; rewrite get_set_neq; first smt.
by move=> ->.
move: H10; case ((m0,r0){hr} = (m1,r1)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget.
move=> neq; rewrite get_set_neq // => hmr.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress.
move: H11 H12; rewrite get_set_neq; first smt.
by move=> ->.
move: H10; case ((m0,r0){hr} = (m1,r1)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget.
move=> neq; rewrite get_set_neq // => hmr.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress.
move: H11 H12; rewrite get_set_neq; first smt.
by move=> ->.
move: H10; case ((m0,r0){hr} = (m1,r1)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget.
move=> neq; rewrite get_set_neq // => hmr.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress.
move: H11 H12; rewrite get_set_neq; first smt.
by move=> ->.
move: H10; case ((m0,r0){hr} = (m1,r1)).
by elim=> [m_eq r_eq]; subst; rewrite get_set_eq /oget.
move=> neq; rewrite get_set_neq // => hmr.
move: H9; rewrite mem_dom get_set_neq // -mem_dom=> dom_hmr.
cut:= H2 m1 r1 _=> //; rewrite hmr /=; progress.
move: H11 H12; rewrite get_set_neq; first smt.
by move=> ->.
qed.
(** The adversary wins if he is lucky, or if he knows the result of H
for the (m,r) used in the signature he returns *)
local lemma Game4_split &m:
Pr[Game4.main() @ &m: res] = Pr[Game4.main() @ &m: res /\ GAdv3.lucky]
+ Pr[Game4.main() @ &m: res /\ !GAdv3.lucky].
proof.
cut ->: Pr[Game4.main() @ &m: res] = Pr[Game4.main() @ &m: (res /\ GAdv3.lucky) \/ (res /\ !GAdv3.lucky)].
by rewrite Pr [mu_eq]; first smt.
rewrite Pr [mu_or].
cut ->: Pr[Game4.main() @ &m: (res /\ GAdv3.lucky) /\ (res /\ !GAdv3.lucky)] = Pr[Game4.main() @ &m: false].
by rewrite Pr [mu_eq]; first smt.
by rewrite Pr [mu_false].
qed.
(** Bounding the adversary's luck *)
local lemma Pr_Game4_lucky &m:
Pr[Game4.main() @ &m: res /\ GAdv3.lucky] <= 1%r/(2^kh)%r.
proof.
byphoare (_: true ==> res /\ GAdv3.lucky)=> //; proc.
inline Gen1(GAdv3,H4,G1).GA.main.
seq 12: (mem (m,r) (dom Hmap.m)) 1%r 0%r 1%r (1%r/(2^kh)%r)=> //.
by hoare; inline H4.v; rcondt 5; auto; smt.
inline H4.v; rcondf 5; first by auto.
by wp; rnd ((=) w); wp; skip; progress; smt.
qed.
local hoare GInv w0: G1.o:
w = w0 /\
(forall m r,
mem (m,r) (dom Hmap.m) =>
let (w,c,u) = oget Hmap.m.[(m,r)] in
mem w (dom Gmap.m) /\
rsap_dom Hmem.pk u /\
let (st,c') = oget Gmap.m.[w] in
c = c' /\
(c = Adv =>
invertible Hmem.pk u /\
let y = (Hmem.ystar ** rsap Hmem.pk u) Hmem.pk in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs)) ==>
omap fst Gmap.m.[w0] = Some res /\
(forall m r,
mem (m,r) (dom Hmap.m) =>
let (w,c,u) = oget Hmap.m.[(m,r)] in
mem w (dom Gmap.m) /\
rsap_dom Hmem.pk u /\
let (st,c') = oget Gmap.m.[w] in
c = c' /\
(c = Adv =>
invertible Hmem.pk u /\
let y = (Hmem.ystar ** rsap Hmem.pk u) Hmem.pk in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs)).
proof.
proc; case (mem w (dom Gmap.m)).
by rcondf 2; auto; progress; cut:= H0; rewrite mem_dom /fst /oget; case (Gmap.m.[w]{hr}).
rcondt 2; first by auto.
auto; progress; (* Good opportunity for progress* *)
last 9 by (cut:= H m r _=> //; rewrite H3 => -[x2_sig] [x_in_G];
(cut neq_w_x: w{hr} <> x1 by smt);
cut:= H4; rewrite get_set_neq /rsap_dom // => ->).
by rewrite /fst /oget get_set_eq.
cut:= H m r _=> //; rewrite H3 => -[x2_sig] [x_in_G].
cut neq_w_x: w{hr} <> x1 by smt.
by rewrite mem_dom get_set_neq // -mem_dom.
cut:= H m r _=> //; rewrite H3 => -[x2_sig] [x_in_G].
cut neq_w_x: w{hr} <> x1 by smt.
smt.
cut:= H m r _=> //; rewrite H3 => -[x2_sig] [x_in_G].
cut neq_w_x: w{hr} <> x1 by smt.
smt.
qed.
local equiv G_LocalG w0: G1.o ~ LocalInverter(A).G.o:
={Hmem.pk, Gmap.m, w} /\
w{1} = w0 /\
(forall m r,
mem (m,r) (dom Hmap.m){1} =>
let (w,c,u) = oget Hmap.m.[(m,r)]{1} in
mem w (dom Gmap.m){1} /\
rsap_dom Hmem.pk{1} u /\
let (st,c') = oget Gmap.m.[w]{1} in
c = c' /\
(c = Adv =>
invertible Hmem.pk{1} u /\
let y = (Hmem.ystar ** rsap Hmem.pk u){1} Hmem.pk{1} in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk{1} u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs{1})) ==>
={Gmap.m, res} /\
omap fst Gmap.m.[w0]{1} = Some res{1} /\
(forall m r,
mem (m,r) (dom Hmap.m){1} =>
let (w,c,u) = oget Hmap.m.[(m,r)]{1} in
mem w (dom Gmap.m){1} /\
rsap_dom Hmem.pk{1} u /\
let (st,c') = oget Gmap.m.[w]{1} in
c = c' /\
(c = Adv =>
invertible Hmem.pk{1} u /\
let y = (Hmem.ystar ** rsap Hmem.pk u){1} Hmem.pk{1} in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk{1} u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs{1})).
proof.
conseq (_: ={Hmem.pk, Gmap.m, w} ==> ={Gmap.m, res}) (GInv w0)=> //.
by sim.
qed.
lemma equal_components s1 s2:
sub (from_signature s1) 0 1 = sub (from_signature s2) 0 1 =>
to_htag (sub (from_signature s1) 1 kh) = to_htag (sub (from_signature s2) 1 kh) =>
to_gtag (sub (from_signature s1) (1 + kh) kg) = to_gtag (sub (from_signature s2) (1 + kh) kg) =>
s1 = s2.
proof.
rewrite /from_signature=> b0_eq h_eq g_eq.
apply ((_: forall (x y:message), `|x| = kh => `|y| = kh => to_htag x = to_htag y => x = y) _ _ _ _) in h_eq;
first 3 by try apply length_sub; smt.
apply ((_: forall (x y:message), `|x| = kg => `|y| = kg => to_gtag x = to_gtag y => x = y) _ _ _ _) in g_eq;
first 3 by try apply length_sub; smt.
cut decomp1: forall (s:signature), s = to_signature (sub (to_bits s) 0 1 || sub (to_bits s) 1 (kh + kg))
by smt.
cut decomp2: forall (s:signature), sub (to_bits s) 1 (kh + kg) =
(sub (to_bits s) 1 kh || sub (to_bits s) (1 + kh) kg)
by smt.
by rewrite decomp1 decomp2 b0_eq h_eq g_eq -decomp2 -decomp1.
qed.
lemma i2osp_inj x y pk:
valid_pkey pk =>
rsap_dom pk x => rsap_dom pk y =>
i2osp x = i2osp y => x = y.
proof.
move=> vpk x_dom y_dom.
rewrite -{2}(pcan_os2ip_i2osp x); first smt.
rewrite -{2}(pcan_os2ip_i2osp y); first smt.
by move=> ->.
qed.
lemma rsap_inj x y pk sk:
valid_keys (pk,sk) =>
rsap_dom pk x => rsap_dom pk y =>
rsap pk x = rsap pk y => x = y.
proof.
move=> vpk x_dom y_dom.
rewrite -{2}(rsas_rsap pk sk x) //.
rewrite -{2}(rsas_rsap pk sk y) //.
by move=> ->.
qed.
lemma fcongr (f:'a -> 'b) x y:
x = y => f x = f y
by move=> ->.
(** Reduction: if the adversary wins in a clever way, then he can invert the one-way challenge *)
local equiv reduction:
Game4.main ~ OW(LocalInverter(A)).main:
={glob A} ==> res{1} /\ !GAdv3.lucky{1} => res{2}.
proof.
proc; inline Gen1(GAdv3,H4,G1).GA.main LocalInverter(A).invert.
seq 6 14: (={Mem.cH, Mem.cG, Mem.cS, Gmap.m, Hmap.m, Hmem.pk, Hmem.ystar, m, s} /\
valid_keys (Hmem.pk,Hmem.sk){1} /\
x{2} = Hmem.xstar{1} /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1} /\
pk0{2} = Mem.pk{1} /\
Hmem.pk{1} = Mem.pk{1} /\
Hmem.sk{1} = Mem.sk{1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
(forall m r,
mem (m,r) (dom Hmap.m){1} =>
let (w,c,u) = oget Hmap.m.[(m,r)]{1} in
mem w (dom Gmap.m){1} /\
rsap_dom Hmem.pk{1} u /\
let (st,c') = oget Gmap.m.[w]{1} in
c = c' /\
(c = Adv =>
invertible Hmem.pk{1} u /\
let y = (Hmem.ystar{1} ** rsap Hmem.pk{1} u) Hmem.pk{1} in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk{1} u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs{1}))).
wp; call (_: ={Mem.cH, Mem.cG, Mem.cS, Gmap.m, Hmap.m, Hmem.pk, Hmem.ystar} /\
valid_keys (Hmem.pk,Hmem.sk){1} /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1} /\
Hmem.pk{1} = Mem.pk{1} /\
Hmem.sk{1} = Mem.sk{1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
(forall m r,
mem (m,r) (dom Hmap.m){1} =>
let (w,c,u) = oget Hmap.m.[(m,r)]{1} in
mem w (dom Gmap.m){1} /\
rsap_dom Hmem.pk{1} u /\
let (st,c') = oget Gmap.m.[w]{1} in
c = c' /\
(c = Adv =>
invertible Hmem.pk{1} u /\
let y = (Hmem.ystar{1} ** rsap Hmem.pk{1} u) Hmem.pk{1} in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk{1} u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs{1}))).
(* Sign... we combine hoare invariant and a "simple" relational equivalence *)
by conseq SignEq SignInv=> //.
(* Ga *)
proc; sp; if=> //; last by wp.
by exists* w{1}; elim* => w0; wp; call (G_LocalG w0).
(* Ha *)
by conseq HaEq HaInv=> //.
by inline*; auto; progress; smt.
(* After the adversary call...
We know the invariant, and we know that (m,s){1} and (m,s){2} are equal *)
seq 3 3: (={Mem.cH, Mem.cG, Mem.cS, Gmap.m, Hmap.m, Hmem.pk, Hmem.ystar, m, s, y, w, st} /\
y{1} = from_signature (i2osp (rsap Mem.pk (os2ip s))){1} /\
w{1} = to_htag (sub y 1 kh){1} /\
st{1} = to_gtag (sub y (1 + kh) kg){1} /\
x{2} = Hmem.xstar{1} /\
valid_keys (Hmem.pk,Hmem.sk){1} /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1} /\
pk0{2} = Mem.pk{1} /\
Hmem.pk{1} = Mem.pk{1} /\
Hmem.sk{1} = Mem.sk{1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
(forall m r,
mem (m,r) (dom Hmap.m){1} =>
let (w,c,u) = oget Hmap.m.[(m,r)]{1} in
mem w (dom Gmap.m){1} /\
rsap_dom Hmem.pk{1} u /\
let (st,c') = oget Gmap.m.[w]{1} in
c = c' /\
(c = Adv =>
invertible Hmem.pk{1} u /\
let y = (Hmem.ystar{1} ** rsap Hmem.pk{1} u) Hmem.pk{1} in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk{1} u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs{1})));
first by wp.
seq 1 1: (={Mem.cH, Mem.cG, Mem.cS, Gmap.m, Hmap.m, Hmem.pk, Hmem.ystar, m, s, y, w, st} /\
y{1} = from_signature (i2osp (rsap Mem.pk (os2ip s))){1} /\
w{1} = to_htag (sub y 1 kh){1} /\
st{1} = to_gtag (sub y (1 + kh) kg){1} /\
g{1} = st'{2} /\
omap fst Gmap.m.[w]{1} = Some g{1} /\
x{2} = Hmem.xstar{1} /\
valid_keys (Hmem.pk,Hmem.sk){1} /\
Hmem.ystar{1} = rsap Hmem.pk{1} Hmem.xstar{1} /\
pk0{2} = Mem.pk{1} /\
Hmem.pk{1} = Mem.pk{1} /\
Hmem.sk{1} = Mem.sk{1} /\
rsap_dom Hmem.pk{1} Hmem.xstar{1} /\
(forall m r,
mem (m,r) (dom Hmap.m){1} =>
let (w,c,u) = oget Hmap.m.[(m,r)]{1} in
mem w (dom Gmap.m){1} /\
rsap_dom Hmem.pk{1} u /\
let (st,c') = oget Gmap.m.[w]{1} in
c = c' /\
(c = Adv =>
invertible Hmem.pk{1} u /\
let y = (Hmem.ystar{1} ** rsap Hmem.pk{1} u) Hmem.pk{1} in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg)) /\
(c = Sig =>
let y = rsap Hmem.pk{1} u in
zeros 1 = sub (from_signature (i2osp y)) 0 1 /\
w = to_htag (sub (from_signature (i2osp y)) 1 kh) /\
st ^ (to_gtag (from_salt r || zeros (kg - k0))) =
to_gtag (sub (from_signature (i2osp y)) (1 + kh) kg) /\
mem (m,i2osp u) Mem.qs{1}))).
by exists* w{1}; elim* => w0; call (G_LocalG w0).
inline H4.v; wp; rnd; wp; skip; progress.
move: H5 H7; pose r:= to_salt (sub (from_gtag (to_gtag (sub (from_signature (i2osp (rsap Mem.pk{1} (os2ip s{2})))) (1 + kh) kg) ^ st'{2})) 0 k0); move=> H5 H7.
cut:= H2 m{2} r _=> //; move: H5 H7.
rewrite mem_dom /oget /pi3_1; case (Hmap.m.[(m,r)]{2})=> //= hmr.
elim/tuple3_ind hmr=> hmr w c u //=.
case c=> //= hmr_def.
(* c = Adv *)
move=> w_def []; cut:= H; rewrite w_def mem_dom /oget /fst; case (Gmap.m.[w]{2})=> //= stc'.
elim/tuple2_ind stc'=> stc' st c' stc'_def //= st'_def [c'_def] [u_inv].
apply someI in st'_def.
rewrite -H6 -w_def -H8 /r.
rewrite /from_salt /to_salt Salt.pcan_to_from.
by rewrite length_sub /from_gtag /to_gtag /from_signature=> //; smt.
rewrite app_sub=> //; first 3 smt.
rewrite /to_gtag /from_gtag GTag.can_from_to -/(to_gtag _) st'_def xorwC -xorwA xorwK xorw0.
move=> [u_in_ZN] [b0_eq] [w_eq st_eq].
cut: i2osp (rsap Mem.pk (os2ip s{2})){1} =
i2osp (((rsap Mem.pk Hmem.xstar) ** (rsap Mem.pk u)) Mem.pk){1}
by apply equal_components.
rewrite -rsap_morphism_mulzp; first 2 smt.
move=> sig_bits_eq.
apply (i2osp_inj _ _ Mem.pk{1} _ _ _) in sig_bits_eq; first 3 smt.
apply (rsap_inj _ _ Mem.pk{1} Mem.sk{1} _ _ _) in sig_bits_eq; first 3 smt.
apply (fcongr (fun x, (x ** (inv Mem.pk{1} u)) Mem.pk{1})) in sig_bits_eq; move: sig_bits_eq=> /=.
rewrite mulzpA; first 3 smt.
rewrite mulzpV; first 2 smt.
rewrite (mulzpC _ 1); first 2 smt.
rewrite mulzp1; first smt.
smt.
(* c = Sig: ignore the goal and prove s{2} = i2osp u *)
move=> w_def []; cut:= H; rewrite w_def mem_dom /oget /fst; case (Gmap.m.[w]{2})=> //= stc'.
elim/tuple2_ind stc'=> stc' st c' stc'_def //= st'_def [c'_def].
apply someI in st'_def.
rewrite -H6 -w_def -H8 /r.
rewrite /from_salt /to_salt Salt.pcan_to_from.
by rewrite length_sub /from_gtag /to_gtag/ from_signature=> //; smt.
rewrite app_sub=> //; first 3 smt.
rewrite /to_gtag /from_gtag GTag.can_from_to -/(to_gtag _) st'_def xorwC -xorwA xorwK xorw0.
move=> [_] [b0_eq] [w_eq] [st_eq unfresh].
cut: i2osp (rsap Mem.pk (os2ip s{2})){1} =
i2osp (rsap Mem.pk u){1}
by apply equal_components.
move=> sig_bits_eq.
apply (i2osp_inj _ _ Mem.pk{1} _ _ _) in sig_bits_eq; first 3 smt.
apply (rsap_inj _ _ Mem.pk{1} Mem.sk{1} _ _ _) in sig_bits_eq; first 3 smt.
apply (fcongr i2osp) in sig_bits_eq.
by move: sig_bits_eq unfresh H11; rewrite can_i2osp_os2ip=> -> ->.
qed.
local lemma OW_Local_Global &m:
Pr[OW(LocalInverter(A)).main() @ &m: res] = Pr[OW(Inverter(A)).main() @ &m: res].
proof. by byequiv (_: ={glob A} ==> ={res})=> //; sim. qed.
lemma conclusion &m:
Pr[UF_CMA(Wrap(PSS96(H,G)),Bounded_PSS_Adv(A,H,G)).main() @ &m: res]
<= Pr[OW(Inverter(A)).main() @ &m: res]
+ (qS + qH)%r * (qS + qH + qG - 1)%r / (2^kh)%r
+ qS%r * (qS + qH)%r / (2^k0)%r
+ 1%r / (2^(k /% 2 - 2))%r
+ qH%r * 1%r/(2^(k /% 2 - 1))%r
+ (qH + qS)%r * 1%r/(2^(k0+1))%r
+ 1%r/(2^kh)%r.
proof.
cut:= PSS96_Game4 &m.
rewrite (Game4_split &m).
cut: Pr[Game4.main() @ &m: res /\ !GAdv3.lucky] <= Pr[OW(Inverter(A)).main() @ &m: res].
by rewrite -(OW_Local_Global &m); byequiv reduction.
cut:= Pr_Game4_lucky &m.
smt.
qed.
end section.
Computing file changes ...
