adjusting lossness assumptions

Author: dfirsov

case_studies/FiatShamir/FS_Completeness.ec

@@ -1,3 +1,4 @@
+
 pragma Goals:printall.
 require import AllCore DBool Bool List Distr.
 require import FS_Basics.

case_studies/FiatShamir/FS_ZeroKnowledge.ec

@@ -8,11 +8,6 @@ proof*.
 
 import Statistical.
 
-(* (* importing statistical zero knowledge  *) *)
-(* clone import Statistical with op epsilon <- 0%r,   (* conditional probability of indistinguishability *) *)
-(*                               op sigma <- 1%r/2%r (* success-event *) *)
-(* proof*. *)
-(* realize epsilon_pos. auto. qed. *)
 
 (* importing the rewinding framework *)
 require  RewBasics.
@@ -29,8 +24,7 @@ section. (* modules and their losslessness assumptions  *)
 declare module V <: RewMaliciousVerifier{-ZK.Hyb.HybOrcl,-ZK.Hyb.Count,-HP}.
 declare module D <: ZKDistinguisher{-ZK.Hyb.HybOrcl,-ZK.Hyb.Count, -HP}.
 
-declare axiom Sim1_run_ll : forall (V0 <: RewMaliciousVerifier), islossless V0.challenge 
-  => islossless V0.summitup => islossless Sim1(V0).run.
+declare axiom Sim1_run_ll : islossless Sim1(V).run.
 declare axiom V_summitup_ll : islossless V.summitup. 
 declare axiom V_challenge_ll : islossless V.challenge.
 declare axiom D_guess_ll : islossless D.guess.

case_studies/HamiltonBlum/Blum_ZeroKnowledge.ec

@@ -27,7 +27,7 @@ declare axiom stat_wit : zk_relation stat wit.
 declare module V <: RewMaliciousVerifier{-HP, -ZK.Hyb.HybOrcl,-ZK.Hyb.Count}.
 declare module D <: ZKDistinguisher{-HP,-ZK.Hyb.HybOrcl,-ZK.Hyb.Count}.
 
-declare axiom Sim1_run_ll : forall (V0 <: RewMaliciousVerifier), islossless V0.challenge => islossless V0.summitup => islossless Sim1(V0).run.
+declare axiom Sim1_run_ll : islossless Sim1(V).run.
 declare axiom V_summitup_ll : islossless V.summitup. 
 declare axiom V_challenge_ll : islossless V.challenge.
 declare axiom D_guess_ll : islossless D.guess.

case_studies/HamiltonBlum/PrArg.ec

@@ -5,6 +5,8 @@ require import StdRing StdOrder StdBigop.
 import BRM.
 
 
+prover ["Alt-Ergo" "Z3" "CVC4"].
+
 (*
 
 The section below contains the derivation of the zero-knowledge upper-bound for a Blum-protocol

case_studies/Schnorr/Schnorr_Basics.ec

@@ -1,6 +1,8 @@
 require import AllCore DBool Bool List Distr AuxResults Finite.
 
 require import CyclicGroup.
+
+
 import FDistr.
 
 

generic/GenericZeroKnowledge.eca

@@ -795,8 +795,7 @@ proof *.
   }.
 
 
-   declare axiom sim1_run_ll : forall (V0 <: RewMaliciousVerifier),
-        islossless V0.challenge => islossless V0.summitup => islossless Sim1(V0).run.
+   declare axiom sim1_run_ll :  islossless Sim1(V).run.
    declare axiom V_summitup_ll  : islossless V.summitup.
    declare axiom V_challenge_ll : islossless V.challenge.
    declare axiom D_guess_ll     : islossless D.guess.
@@ -876,7 +875,7 @@ sim.  skip. progress. auto. auto.
      apply (one_to_many_zk  Sim1' D _  _ _ _ _ &m  stat wit sigma epsilon N
         Pr[ZKD(HonestProver, V, D).main(stat, wit) @ &m : res]  _ _ _).
      conseq D_guess_prop. auto.
-     apply (sim1_run_ll V). apply V_challenge_ll. apply V_summitup_ll. 
+     apply sim1_run_ll. 
      move => x. 
      proc*. 
      call (sim1_rew_ph (x.`4, x.`5)).
@@ -910,8 +909,7 @@ sim.  skip. progress. auto. auto.
   declare module V <: RewMaliciousVerifier {-Sim1, -HonestProver,-Hyb.Count, -Hyb.HybOrcl}.
   declare module D <: ZKDistinguisher{-HonestProver}.
 
-  declare axiom sim1_run_ll : forall (V0 <: RewMaliciousVerifier), islossless V0.challenge
-    => islossless V0.summitup => islossless Sim1(V0).run.
+  declare axiom sim1_run_ll : islossless Sim1(V).run.
   declare axiom V_summitup_ll  : islossless V.summitup.
   declare axiom V_challenge_ll : islossless V.challenge.
   declare axiom D_guess_ll     : islossless D.guess.