Skip to content

Commit

Permalink
Add some comments
Browse files Browse the repository at this point in the history
  • Loading branch information
gregweng committed Jan 17, 2025
1 parent eff3a62 commit baf98fc
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 10 deletions.
38 changes: 33 additions & 5 deletions smc/smc_entropy.v
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,39 @@ Require Import proba jfdist_cond entropy graphoid smc_proba.
Import GRing.Theory.
Import Num.Theory.

(******************************************************************************)
(* SMC Proofs in entroy *)
(* From: Information-theoretically Secure Number-product Protocol *)
(* *)
(******************************************************************************)
(************************************************************************************)
(* SMC Proofs in entroy *)
(* *)
(* From: Information-theoretically Secure Number-product Protocol *)
(* SHEN, Chih-Hao, et al. In: 2007 International Conference on Machine *)
(* Learning and Cybernetics. IEEE, 2007. p. 3006-3011. *)
(* *)
(* *)
(* | Definitions | | Meaning |*)
(* |-------------------|----|------------------------------------------------------|*)
(* | x \*d y | == | dot product of two random vectors. |*)
(* | scalar_product | == | The deterministic version of |*)
(* | | | SMC scalar product protocol as a function. |*)
(* | is_scalar_product | == | The correctness of the SMC scalar product results |*)
(* |-------------------------------------------------------------------------------|*)
(* *)
(* *)
(* Lemmas: *)
(* pi2_bob_is_leakage_free_proof == the proof shows that Bob's knowledge of *)
(* Alice's secret input x1 does not increase *)
(* by accessing random variables received *)
(* during the protocols execution *)
(* pi2_alice_is_leakage_free_proof == the proof shows that Alice's knowledge of *)
(* Bob's secret input x2 does not increase *)
(* by accessing random variables received *)
(* during the protocols execution *)
(* cpr_cond_entropy == given a conditional probability removal *)
(* lemma P( X | (Y, Z))->P( X | Y ), shows that*)
(* with some conditions met, there exists a *)
(* conditional entropy removal lemma *)
(* H( X | (Y, Z))->H( X | Y ) *)
(* *)
(************************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Expand Down
2 changes: 2 additions & 0 deletions smc/smc_interpreter.v
Original file line number Diff line number Diff line change
Expand Up @@ -453,9 +453,11 @@ Qed.
Let x1x2s2x1'r2_y2_indepP :=
x1x2s2x1'r2_y2_indep (x2s2x1s1r2_y2_indep (x2s2x1s1r1_y2_indep inputs)).


Let x2s2x1s1_r2_indep :
P |= [% x2, s2, x1, s1] _|_ [%s1, s2, r1].
Proof.

rewrite inde_rv_events'.
rewrite /inde_rv_ev => E F.
rewrite (reasoning_by_cases [%s1, s2, r1] [% x2, s2, x1, s1]).
Expand Down
14 changes: 9 additions & 5 deletions smc/smc_proba.v
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,15 @@ Require Import proba jfdist_cond graphoid.
Import GRing.Theory.
Import Num.Theory.

(******************************************************************************)
(* SMC Useful Tools *)
(* From: Information-theoretically Secure Number-product Protocol *)
(* *)
(******************************************************************************)
(************************************************************************************)
(* SMC "Useful Tools" probability lemmas *)
(* *)
(* From: Information-theoretically Secure Number-product Protocol, *)
(* Sec. III.B "Useful Tools" *)
(* SHEN, Chih-Hao, et al. In: 2007 International Conference on Machine *)
(* Learning and Cybernetics. IEEE, 2007. p. 3006-3011. *)
(* *)
(************************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Expand Down

0 comments on commit baf98fc

Please sign in to comment.