Skip to content

Commit

Permalink
Move temporary stuff, and update PKE with NM changes.
Browse files Browse the repository at this point in the history
  • Loading branch information
@MM45
MM45 committed Nov 15, 2024
1 parent 725a076 commit 3145cd9
Show file tree
Hide file tree
Showing 3 changed files with 162 additions and 229 deletions.
106 changes: 3 additions & 103 deletions proofs/KeyEncapsulationMechanisms.eca
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ module O_CCA1_Default (S : Scheme) : Oracles_CCA1i = {
}.

(**
A duplication of the default implementation for the oracles employed in CCA1 security games
A duplicate of the default implementation for the oracles employed in CCA1 security games
(as well as the first stage of CCA2 games). May be useful for security notions considering two
such (sets of) oracles.
**)
Expand Down Expand Up @@ -183,7 +183,7 @@ module O_CCA2_Default (S : Scheme) : Oracles_CCA2i = {
}.

(**
A duplication of the default implementation for the oracles employed in
A duplicate of the default implementation for the oracles employed in
(the second stage of) CCA2 (CCA) security games. May be useful for security notions
considering two such (sets of) oracles.
**)
Expand Down Expand Up @@ -622,7 +622,7 @@ end IND.
is (uniformly) random).

Note that these notions only have a sensible definition with a provided bit, so
no "sampled bit" variants are defined
no "sampled bit" variants are defined.
**)
abstract theory NM.
(* Distributions *)
Expand Down Expand Up @@ -3951,105 +3951,5 @@ if => //.
wp; call (: true); call (: true).
by wp; call(: true); skip => /> /#.
qed.



(* Test *)
module SNM_CCA_Split(S : Scheme, O : Oracles_CCA2i, A : Adv_SNMCCA) = {
proc rest(b : bool, o : bool) = {
var pk : pk_t;
var sk : sk_t;
var k : key_t;
var k' : key_t;
var c : ctxt_t;
var rel : key_t -> key_t option list -> bool;
var cl : ctxt_t list;
var ko : key_t option;
var kol : key_t option list;

(pk, sk) <@ S.keygen();
(k, c) <@ S.encaps(pk);
k' <$ (dkeym pk)%NM;
O.init(sk, c);

(rel, cl) <@ A(O).find(pk, c, if o then (k', k) else (k, k'));
kol <- [];
while (size kol < size cl){
ko <@ S.decaps(sk, nth witness cl (size kol));
kol <- rcons kol ko;
}

return ! (c \in cl) /\ rel (if b then k' else k) kol;
}

proc main(b : bool) : bool = {
var o, r : bool;


o <$ {0,1};
r <@ rest(b, o);

return r;
}
}.

module (R_SNMCCA_INDCCAP (A : Adv_INDCCA) : Adv_SNMCCA) (O : Oracles_CCA) = {
proc find(pk : pk_t, c : ctxt_t, kk : key_t * key_t) : (key_t -> key_t option list -> bool) * ctxt_t list = {
var b' : bool;

b' <@ A(O).distinguish(pk, kk.`1, c);

return (fun k kl, k = if b' then kk.`2 else kk.`1, []);
}
}.


lemma test (S <: Scheme) (O <: Oracles_CCA2i{-S}) (A <: Adv_INDCCA{-S, -O}) &m :
IND.dkeym = NM.dkeym =>
Pr[SNM_CCA_Split(S, O, R_SNMCCA_INDCCAP(A)).main(false) @ &m : res]
=
1%r / 2%r * Pr[IND_CCA_P(S, O, A).main(false) @ &m : !res]
+
1%r / 2%r * Pr[IND_CCA_P(S, O, A).main(true) @ &m : res].
proof. admit. qed.


lemma test2 (S <: Scheme) (O <: Oracles_CCA2i{-S}) (A <: Adv_INDCCA{-S, -O}) &m :
IND.dkeym = NM.dkeym =>
Pr[SNM_CCA_Split(S, O, R_SNMCCA_INDCCAP(A)).main(true) @ &m : res]
=
1%r / 2%r * Pr[IND_CCA_P(S, O, A).main(false) @ &m : res]
+
1%r / 2%r * Pr[IND_CCA_P(S, O, A).main(true) @ &m : !res].
proof. admit. qed.



lemma test3 (S <: Scheme) (O <: Oracles_CCA2i{-S}) (A <: Adv_INDCCA{-S, -O}) &m :
IND.dkeym = NM.dkeym =>
Pr[SNM_CCA_Split(S, O, R_SNMCCA_INDCCAP(A)).main(false) @ &m : res]
-
Pr[SNM_CCA_Split(S, O, R_SNMCCA_INDCCAP(A)).main(true) @ &m : res]
=
Pr[IND_CCA_P(S, O, A).main(true) @ &m : res]
-
Pr[IND_CCA_P(S, O, A).main(false) @ &m : res].
proof.
move=> t.
move: (test S O A &m t) (test2 S O A &m t).
rewrite Pr[mu_not] Pr[mu_not].
have ->:
Pr[IND_CCA_P(S, O, A).main(false) @ &m : true]
=
1%r.
+ admit.
have ->:
Pr[IND_CCA_P(S, O, A).main(true) @ &m : true]
=
1%r.
+ admit.
smt().
qed.


end Relations.
189 changes: 63 additions & 126 deletions proofs/PublicKeyEncryption.eca
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,32 @@ module O_CCA1_Default (S : Scheme) : Oracles_CCA1i = {
}
}.

(**
A duplicate of the default implementation for the oracles employed in CCA1 security games
(as well as the first stage of CCA2 games). May be useful for security notions considering two
such (sets of) oracles.
**)
module O_CCA1_DDefault (S : Scheme) : Oracles_CCA1i = {
var sk : sk_t
var qs : (ctxt_t * ptxt_t option) list

proc init(sk_init : sk_t) = {
sk <- sk_init;
qs <- [];
}

proc dec(c : ctxt_t) : ptxt_t option = {
var p : ptxt_t option;

p <@ S.dec(sk, c);

qs <- rcons qs (c, p);

return p;
}
}.


(*
adaptive Chosen-Ciphertext Attacks (CCA2)
The adversary is given the considered public key and access to a decryption oracle throughout.
Expand Down Expand Up @@ -140,6 +166,37 @@ module O_CCA2_Default (S : Scheme) : Oracles_CCA2i = {
}
}.

(**
A duplicate of the default implementation for the oracles employed in
(the second stage of) CCA2 security games. May be useful for security notions considering two
such (sets of) oracles.
**)
module O_CCA2_DDefault (S : Scheme) : Oracles_CCA2i = {
var sk : sk_t
var c' : ctxt_t
var qs : (ctxt_t * ptxt_t option) list

proc init(sk_init : sk_t, c'_init : ctxt_t) = {
sk <- sk_init;
c' <- c'_init;
qs <- [];
}

proc dec(c : ctxt_t) : ptxt_t option = {
var p : ptxt_t option;

if (c <> c') {
p <@ S.dec(sk, c);
} else {
p <- None;
}

qs <- rcons qs (c, p);

return p;
}
}.

(** Interface for oracles given to the adversary in CCA (both 1 and 2) security games **)
module type Oracles_CCA = {
proc dec(c : ctxt_t) : ptxt_t option
Expand Down Expand Up @@ -449,6 +506,9 @@ module IND_CCA2_P (S : Scheme, O1 : Oracles_CCA1i, O2 : Oracles_CCA2i, A : Adv_I
The adversary is asked to provide a relation (say R) and
a list of ciphertexts such that the plaintexts obtained from decrypting these
ciphertexts are related (under R) to the plaintext corresponding to a given ciphertext.

Note that these notions only have a sensible definition with a provided bit, so
no "sampled bit" variants are defined.
**)
abstract theory NM.
(* Operators *)
Expand Down Expand Up @@ -477,45 +537,8 @@ module type Adv_NMCPA = {
proc find(c : ctxt_t) : (ptxt_t -> ptxt_t option list -> bool) * ctxt_t list
}.

(** NM-CPA security game (sampled bit) **)
(** NM-CPA security game **)
module NM_CPA (S : Scheme, A : Adv_NMCPA) = {
proc main() : bool = {
var pk : pk_t;
var sk : sk_t;
var dp : ptxt_t distr;
var b : bool;
var p, p' : ptxt_t;
var c : ctxt_t;
var rel : ptxt_t -> ptxt_t option list -> bool;
var cl : ctxt_t list;
var po : ptxt_t option;
var pol : ptxt_t option list;

(pk, sk) <@ S.keygen();

dp <@ A.choose(pk);

p <$ dp;
p' <$ dp;

c <@ S.enc(pk, p);

(rel, cl) <@ A.find(c);

pol <- [];
while (size pol < size cl) {
po <@ S.dec(sk, nth witness cl (size pol));
pol <- rcons pol po;
}

b <$ {0,1};

return is_valid_dp dp /\ !(c \in cl) /\ rel (if b then p' else p) pol;
}
}.

(** NM-CPA security game (provided bit) **)
module NM_CPA_P (S : Scheme, A : Adv_NMCPA) = {
proc main(b : bool) : bool = {
var pk : pk_t;
var sk : sk_t;
Expand Down Expand Up @@ -561,46 +584,8 @@ module type Adv_NMCCA1 (O : Oracles_CCA) = {
proc find(c : ctxt_t) : (ptxt_t -> ptxt_t option list -> bool) * ctxt_t list { }
}.

(** NM-CCA1 security game (sampled bit) **)
(** NM-CCA1 security game **)
module NM_CCA1 (S : Scheme, O : Oracles_CCA1i, A : Adv_NMCCA1) = {
proc main() : bool = {
var pk : pk_t;
var sk : sk_t;
var dp : ptxt_t distr;
var b : bool;
var p, p' : ptxt_t;
var c : ctxt_t;
var rel : ptxt_t -> ptxt_t option list -> bool;
var cl : ctxt_t list;
var po : ptxt_t option;
var pol : ptxt_t option list;

(pk, sk) <@ S.keygen();
O.init(sk);

dp <@ A(O).choose(pk);

p <$ dp;
p' <$ dp;

c <@ S.enc(pk, p);

(rel, cl) <@ A(O).find(c);

pol <- [];
while (size pol < size cl) {
po <@ S.dec(sk, nth witness cl (size pol));
pol <- rcons pol po;
}

b <$ {0,1};

return is_valid_dp dp /\ !(c \in cl) /\ rel (if b then p' else p) pol;
}
}.

(** NM-CCA1 security game (provided bit) **)
module NM_CCA1_P (S : Scheme, O : Oracles_CCA1i, A : Adv_NMCCA1) = {
proc main(b : bool) : bool = {
var pk : pk_t;
var sk : sk_t;
Expand Down Expand Up @@ -648,46 +633,7 @@ module type Adv_NMCCA2 (O : Oracles_CCA) = {
proc find(c : ctxt_t) : (ptxt_t -> ptxt_t option list -> bool) * ctxt_t list
}.

(** NM-CCA2 security game (sampled bit) **)
module NM_CCA2 (S : Scheme, O1 : Oracles_CCA1i, O2 : Oracles_CCA2i, A : Adv_NMCCA2) = {
proc main() : bool = {
var pk : pk_t;
var sk : sk_t;
var dp : ptxt_t distr;
var b : bool;
var p, p' : ptxt_t;
var c : ctxt_t;
var rel : ptxt_t -> ptxt_t option list -> bool;
var cl : ctxt_t list;
var po : ptxt_t option;
var pol : ptxt_t option list;

(pk, sk) <@ S.keygen();
O1.init(sk);

dp <@ A(O1).choose(pk);

p <$ dp;
p' <$ dp;

c <@ S.enc(pk, p);
O2.init(sk, c);

(rel, cl) <@ A(O2).find(c);

pol <- [];
while (size pol < size cl) {
po <@ S.dec(sk, nth witness cl (size pol));
pol <- rcons pol po;
}

b <$ {0,1};

return is_valid_dp dp /\ !(c \in cl) /\ rel (if b then p' else p) pol;
}
}.

(** NM-CCA2 security game (provided bit) **)
(** NM-CCA2 security game **)
module NM_CCA2_P (S : Scheme, O1 : Oracles_CCA1i, O2 : Oracles_CCA2i, A : Adv_NMCCA2) = {
proc main(b : bool) : bool = {
var pk : pk_t;
Expand Down Expand Up @@ -1243,15 +1189,6 @@ module WCFR_CCA (S : Scheme, O0 : Oracles_CCA1i, O1 : Oracles_CCA1i, A : Adv_WCF
}.


(*
BINDing (BIND)



*)



(** Delta-correct (i.e., partially-correct) PKE schemes. **)
theory DeltaCorrect.
(* Correctness *)
Expand Down
Loading

0 comments on commit 3145cd9

Please sign in to comment.