Update along with new version of eprint

Inria-Prosecco · Sep 10, 2021 · 9511f08 · 9511f08
1 parent 09c2806
commit 9511f08
Show file tree

Hide file tree

Showing 17 changed files with 33,865 additions and 34,486 deletions.
diff --git a/common.dhkem.dh.ocv b/common.dhkem.dh.ocv
@@ -1,7 +1,7 @@
 type G_t [bounded].
 fun Serialize(G_t): bitstring [data].
-type Z_t [bounded,pcoll250,nonuniform].
-proba PCollKey [pest250].
+type Z_t [bounded,nonuniform].
+proba PCollKey.
 
 expand DH_proba_collision_minimal(
   G_t,

diff --git a/dhkem.auth.insider-cca-lr.m4.ocv b/dhkem.auth.insider-cca-lr.m4.ocv
@@ -1,5 +1,8 @@
 proof {
-  allowed_collisions pest150;
+  allowed_collisions default^4/large;
+   (* We allow eliminating collisions with probability in power 4 of 
+      N, Qeperuser, Qdperuser, Qcperuser times PCollKey, to allow q^2 * PCollKey,
+      where q = N * (Qeperuser + Qdperuser + Qcperuser) *)
   (* on the left side *)
   out_game "l0.out.cv";
   (* Let appear this case distinction in the Decap oracle,
@@ -122,7 +125,7 @@ expand GDH_RSR_minimal(
 
 include(`common.dhkem.ocv')
 
-param N, Qeperuser, Qcperuser, Qdperuser [size30].
+param N, Qeperuser, Qcperuser, Qdperuser.
 
 equivalence
   Ostart() :=

diff --git a/dhkem.auth.insider-cca-lr.ocv b/dhkem.auth.insider-cca-lr.ocv
@@ -1,5 +1,8 @@
 proof {
-  allowed_collisions pest150;
+  allowed_collisions default^4/large;
+   (* We allow eliminating collisions with probability in power 4 of 
+      N, Qeperuser, Qdperuser, Qcperuser times PCollKey, to allow q^2 * PCollKey,
+      where q = N * (Qeperuser + Qdperuser + Qcperuser) *)
   (* on the left side *)
   out_game "l0.out.cv";
   (* Let appear this case distinction in the Decap oracle,
@@ -104,8 +107,8 @@ proof {
 
 type G_t [bounded].
 fun Serialize(G_t): bitstring [data].
-type Z_t [bounded,pcoll250,nonuniform].
-proba PCollKey [pest250].
+type Z_t [bounded,nonuniform].
+proba PCollKey.
 
 expand DH_proba_collision_minimal(
   G_t,
@@ -288,7 +291,7 @@ letfun AuthDecap(key_extr: hash_key_t, enc: bitstring, skR: Z_t, pkS: G_t) =
 
 
 
-param N, Qeperuser, Qcperuser, Qdperuser [size30].
+param N, Qeperuser, Qcperuser, Qdperuser.
 
 equivalence
   Ostart() :=

diff --git a/dhkem.auth.insider-cca-lr.proof b/dhkem.auth.insider-cca-lr.proof
diff --git a/dhkem.auth.outsider-auth-lr.m4.ocv b/dhkem.auth.outsider-auth-lr.m4.ocv
@@ -1,5 +1,8 @@
 proof {
-  allowed_collisions pest150;
+  allowed_collisions default^4/large;
+   (* We allow eliminating collisions with probability in power 4 of 
+      N, Qeperuser, Qdperuser, Qcperuser times PCollKey, to allow q^2 * PCollKey,
+      where q = N * (Qeperuser + Qdperuser + Qcperuser) *)
   (* start on the left side *)
   out_game "l.out.cv";
 
@@ -149,7 +152,7 @@ include(`common.dhkem.ocv')
 
 event AuthEncap_does_not_fail.
 
-param N, Qeperuser, Qdperuser [size30].
+param N, Qeperuser, Qdperuser.
 
 equivalence
   Ostart() :=

diff --git a/dhkem.auth.outsider-auth-lr.ocv b/dhkem.auth.outsider-auth-lr.ocv
@@ -1,5 +1,8 @@
 proof {
-  allowed_collisions pest150;
+  allowed_collisions default^4/large;
+   (* We allow eliminating collisions with probability in power 4 of 
+      N, Qeperuser, Qdperuser, Qcperuser times PCollKey, to allow q^2 * PCollKey,
+      where q = N * (Qeperuser + Qdperuser + Qcperuser) *)
   (* start on the left side *)
   out_game "l.out.cv";
 
@@ -129,8 +132,8 @@ proof {
 
 type G_t [bounded].
 fun Serialize(G_t): bitstring [data].
-type Z_t [bounded,pcoll250,nonuniform].
-proba PCollKey [pest250].
+type Z_t [bounded,nonuniform].
+proba PCollKey.
 
 expand DH_proba_collision_minimal(
   G_t,
@@ -315,7 +318,7 @@ letfun AuthDecap(key_extr: hash_key_t, enc: bitstring, skR: Z_t, pkS: G_t) =
 
 event AuthEncap_does_not_fail.
 
-param N, Qeperuser, Qdperuser [size30].
+param N, Qeperuser, Qdperuser.
 
 equivalence
   Ostart() :=