Formalization for SMC protocols

smc/smc_interpreter.v

@@ -454,8 +454,10 @@ Let x1x2s2x1'r2_y2_indepP :=
   x1x2s2x1'r2_y2_indep (x2s2x1s1r2_y2_indep (x2s2x1s1r1_y2_indep inputs)).
 
 Let x2s2x1s1_r2_indep :
+  P |= [% s1, s2] _|_ [% x1, x2, r1] ->
   P |= [% x2, s2, x1, s1] _|_ [%s1, s2, r1].
 Proof.
+About RV2_indeC.
 Abort.
 
 Let x2s2x1'_r2_indep :

smc/smc_proba.v

@@ -37,6 +37,25 @@ Local Notation "f × g" :=
   (fun xy => (f xy.1, g xy.2)) (at level 10).
 
 
+Lemma RV2_indeC :
+  P |= [% X, X] _|_ [% Y, Z] ->
+  P |= [% X, Y] _|_ [% X, Z].
+Proof.
+rewrite /inde_rv => H [x1 y] [x2 z].
+rewrite pr_eq_pairA.
+transitivity (`Pr[ [% X, X, Y, Z] = (x1, x2, y, z) ]).
+  admit.
+(* TODO: spliting events and changing order of RVs are kinda difficult *)
+Admitted.
+
+Lemma RV2_inde_reduce :
+  P |= X _|_ Y ->
+  P |= [% X, X] _|_ Y.
+Proof.
+(* TODO: [% X, X] = (x1, x2) but x1 could be different from x2 for all x1, x2? *)
+Admitted.
+
+
 (* Information-Theoretically Secure Number Protocol*)
 (* Lemma 3.1 *)
 Lemma inde_rv_comp (UB' TB' : finType) (g' : TB' -> UB')(Y' : {RV P -> TB'}): P|= X _|_ Y' -> P|= (f `o X) _|_ (g' `o Y').