Code

Formalization for SMC protocols#136

Code

Draft

weng-chenghui wants to merge 142 commits intoaffeldt-aist:masteraffeldt-aist/infotheo:masterfrom weng-chenghui:smc_useful_toolsweng-chenghui/infotheo:smc_useful_toolsCopy head branch name to clipboard

+2,992-1

Commits

Commits on Jul 17, 2024

• lemma 3.1

  

  t6s

  authored and

  gregweng

  committed
  3275147

  Copy full SHA for 3275147

• cleaning

  

  t6s

  authored and

  gregweng

  committed
  4713b10

  Copy full SHA for 4713b10

• Lemma 3.2

  

  t6s

  authored and

  gregweng

  committed
  91cef06

  Copy full SHA for 91cef06

• Lemma 3.3 in a new file probability/smc.v

  gregweng

  committed
  22e2c29

  Copy full SHA for 22e2c29

• WIP: try to prove Lemma 3.4

  gregweng

  committed
  79fee7c

  Copy full SHA for 79fee7c

• WIP: lemma 3.4

  gregweng

  committed
  ae6146a

  Copy full SHA for ae6146a

• WIP: try prob + uniform dist

  gregweng

  committed
  4d2a5da

  Copy full SHA for 4d2a5da

• pXY_unif

  

  t6s

  authored and

  gregweng

  committed
  0438fad

  Copy full SHA for 0438fad

• comments

  

  t6s

  authored and

  gregweng

  committed
  7405564

  Copy full SHA for 7405564

• adapt smc_useful_tools to mc2 (#1)

  Show description for 86a9d01
  

  5 peoplecommitted
  86a9d01

  Copy full SHA for 86a9d01

• WIP: cpr_eqE_mul

  gregweng

  committed
  1ae2f57

  Copy full SHA for 1ae2f57

• WIP: progress but not yet finished lemma 3.5

  gregweng

  committed
  d11ba90

  Copy full SHA for d11ba90

• WIP: lemma 3.5 with a new approach

  Show description for 5979d82
  gregweng

  committed
  5979d82

  Copy full SHA for 5979d82

• WIP: checking how to prove fdist_cond Y0 |= X' _|_ Z'

  gregweng

  committed
  654ba1c

  Copy full SHA for 654ba1c

• By a lemma with graphoid lemmas, prove lemma 3.5

  gregweng

  committed
  9571191

  Copy full SHA for 9571191

• clean up lemma_3_5 (#2)

  Show description for 2dc2086
  

  garrigue

  authored and

  gregweng

  committed
  2dc2086

  Copy full SHA for 2dc2086

• simplify proof of lemma_3_5 (#3)

  

  garrigue

  authored and

  gregweng

  committed
  d39e077

  Copy full SHA for d39e077

• Lemma 3.6 and Theorem 3.7, before the entropy part

  gregweng

  committed
  3e13173

  Copy full SHA for 3e13173

• Proved Theorem 3.7 (masked condition removal) entropy version

  gregweng

  committed
  66b7a15

  Copy full SHA for 66b7a15

• Rebase: unto infotheo master

  gregweng

  committed
  3c9709d

  Copy full SHA for 3c9709d

Commits on Jul 24, 2024

• WIP: how to handle forall and one instance of it?

  gregweng

  committed
  26691ff

  Copy full SHA for 26691ff

• WIP: cannot swap two assumption in one implication?

  gregweng

  committed
  144f02e

  Copy full SHA for 144f02e

Commits on Jul 26, 2024

• WIP: discussed about how to continue proofs

  gregweng

  committed
  d7371ba

  Copy full SHA for d7371ba

Commits on Jul 29, 2024

• WIP: fun_cond_entropy_eq0

  gregweng

  committed
  fd67582

  Copy full SHA for fd67582

Commits on Jul 30, 2024

• WIP: try to continue fun_cond_entropy_eq0

  gregweng

  committed
  3186927

  Copy full SHA for 3186927

• add some comments

  gregweng

  committed
  9bb3a81

  Copy full SHA for 9bb3a81

Commits on Aug 2, 2024

• WIP: stuck because associativity in distribution expressions

  gregweng

  committed
  eb1a3cc

  Copy full SHA for eb1a3cc

Commits on Aug 7, 2024

• WIP: fun cond removal entropy

  gregweng

  committed
  9bc2aa9

  Copy full SHA for 9bc2aa9

• fun_cond_removal_entropy

  gregweng

  committed
  ddef3cf

  Copy full SHA for ddef3cf

Commits on Aug 21, 2024

• WIP: want to prove pi2 but need joint_entropy_indeRV first

  gregweng

  committed
  5a67d2e

  Copy full SHA for 5a67d2e

• protocol pi2 eq2 is done

  gregweng

  committed
  1c178b6

  Copy full SHA for 1c178b6

Commits on Aug 29, 2024

• WIP: try to prove eq_fin

  gregweng

  committed
  0dc4e99

  Copy full SHA for 0dc4e99

• WIP: Found that the type of TX in eq3 may need to be 'I_p

  gregweng

  committed
  dd11e5c

  Copy full SHA for dd11e5c

Commits on Aug 30, 2024

• WIP: try to prove eq3 with TX is I_m.+2

  gregweng

  committed
  081e0f2

  Copy full SHA for 081e0f2

Commits on Aug 31, 2024

• Proved eq3

  gregweng

  committed
  f801c63

  Copy full SHA for f801c63

Commits on Sep 2, 2024

• Successfully prove two hypothese for eq3 can be provided by lemmas and proofs

  gregweng

  committed
  564237b

  Copy full SHA for 564237b

Commits on Sep 3, 2024

• WIP: Try to prove eqn4 but vector brings some difficulties

  gregweng

  committed
  865c3ad

  Copy full SHA for 865c3ad

Commits on Sep 5, 2024

• Generalize lemma_3_5

  gregweng

  committed
  703002d

  Copy full SHA for 703002d

• Proved eqn4

  gregweng

  committed
  98a99d6

  Copy full SHA for 98a99d6

Commits on Sep 6, 2024

• Proved eqn6

  gregweng

  committed
  ce34562

  Copy full SHA for ce34562

• WIP: need cond_entropy1 and cond_entropy conversion

  gregweng

  committed
  4e0542f

  Copy full SHA for 4e0542f

Commits on Sep 7, 2024

• WIP: trying to convert cond_entropy and cond_entropy1_RV

  gregweng

  committed
  60464d3

  Copy full SHA for 60464d3

Commits on Sep 10, 2024

• WIP: make the eqn2 proof works again

  gregweng

  committed
  c20588a

  Copy full SHA for c20588a

Commits on Sep 18, 2024

• Commit before the meeting

  gregweng

  committed
  8e7b326

  Copy full SHA for 8e7b326

• WIP: cpr_cond_entropy

  gregweng

  committed
  96db7ff

  Copy full SHA for 96db7ff

• cpr_cond_entropy

  garrigue

  committed
  579303b

  Copy full SHA for 579303b

Commits on Sep 19, 2024

• shorten proof of cpr_cond_entropy

  garrigue

  committed
  da27598

  Copy full SHA for da27598

• small cleanup

  garrigue

  committed
  12eb3ea

  Copy full SHA for 12eb3ea

Commits on Sep 25, 2024

• cleanup

  t6s

  committed
  a28d0fe

  Copy full SHA for a28d0fe

Commits on Sep 26, 2024

• remove surjective_pairing

  garrigue

  committed
  c53ff3c

  Copy full SHA for c53ff3c

• eqn3 proved after a new version of cpr_cond_entropy with a new hypothesis

  gregweng

  committed
  7cb3296

  Copy full SHA for 7cb3296

Commits on Oct 1, 2024

• WIP: Stuck at:

  Show description for c6b352b
  gregweng

  committed
  c6b352b

  Copy full SHA for c6b352b

• WIP: show function composition results equal to random variables

  gregweng

  committed
  14abca8

  Copy full SHA for 14abca8

• WIP: eqn3 proven with random variables instead of function compositions

  gregweng

  committed
  bb2ef59

  Copy full SHA for bb2ef59

• WIP: for eqn4, the problem is if P|= s2 _|_ [%...s2...]

  gregweng

  committed
  c86a45d

  Copy full SHA for c86a45d

Commits on Oct 2, 2024

• Completed the pi2_alice_view_is_leakage_free_proof; inde_RV2_comp still remains

  gregweng

  committed
  a50e5e7

  Copy full SHA for a50e5e7

Commits on Oct 3, 2024

• Fix

  gregweng

  committed
  14d08cc

  Copy full SHA for 14d08cc

Commits on Oct 4, 2024

• For showing premises clearly, Move cpr_cond_entropy to another section

  gregweng

  committed
  562e600

  Copy full SHA for 562e600

Commits on Oct 5, 2024

• Change the order in mc_removal_pr,

  Show description for 9f94801
  gregweng

  committed
  9f94801

  Copy full SHA for 9f94801

Commits on Oct 17, 2024

• Completed eqn6_proof

  gregweng

  committed
  aacf39e

  Copy full SHA for aacf39e

Commits on Oct 23, 2024

• extra_pr section

  t6s

  committed
  0f2b44f

  Copy full SHA for 0f2b44f

Commits on Oct 24, 2024

• Proved eqn8 again

  gregweng

  committed
  79b5086

  Copy full SHA for 79b5086

Commits on Oct 25, 2024

• Proved that from Bob's view pi2 is secure

  gregweng

  committed
  4870723

  Copy full SHA for 4870723

• try to use pairwise-like inde generator

  gregweng

  committed
  bfaf0b2

  Copy full SHA for bfaf0b2

Commits on Oct 30, 2024

• Rename indep hypothese

  gregweng

  committed
  9515b44

  Copy full SHA for 9515b44

Commits on Oct 31, 2024

• WIP: try to unify correct and information leakage but need a better way to do it instead of re-proving things

  gregweng

  committed
  b6fead2

  Copy full SHA for b6fead2

Commits on Nov 5, 2024

• SMC scalar product proved again with rV and TX

  gregweng

  committed
  1bc5513

  Copy full SHA for 1bc5513

Commits on Nov 6, 2024

• Try to connect the algorithm correctness and information leakage free

  Show description for ac6d667
  gregweng

  committed
  ac6d667

  Copy full SHA for ac6d667

Commits on Nov 7, 2024

• Connect algorithm and leakage analysis by proving relations between random variables satisify scalar-product; code clean up

  gregweng

  committed
  d3f312e

  Copy full SHA for d3f312e

• A comment to summarize the work

  gregweng

  committed
  4c6caa1

  Copy full SHA for 4c6caa1

Commits on Nov 22, 2024

• Try to introduce module for encapsulating information-leakage-free proofs

  gregweng

  committed
  977f95c

  Copy full SHA for 977f95c

• Commit Jacques' SMC interpreter

  gregweng

  committed
  e4368a3

  Copy full SHA for e4368a3

Commits on Nov 23, 2024

• WIP: try to figure out howto prove pr2_unif (line 747)

  gregweng

  committed
  d727199

  Copy full SHA for d727199

• Add hypothesis that r1 is uniformly distributed

  gregweng

  committed
  931b845

  Copy full SHA for 931b845

• WIP: admitted the working-in-progress fdist_uniformD because it is necessary for pr2_unif

  gregweng

  committed
  4662dfe

  Copy full SHA for 4662dfe

Commits on Nov 27, 2024

• Admitted pr2_unif before we can prove it; completed bob_view_is_leakage_free_proof

  gregweng

  committed
  4d6c274

  Copy full SHA for 4d6c274

Commits on Nov 28, 2024

• Commit the smc_interpreter_v1 as a reference

  gregweng

  committed
  6746862

  Copy full SHA for 6746862

Commits on Dec 2, 2024

• WIP: try to understand where to put log

  gregweng

  committed
  cb9af4b

  Copy full SHA for cb9af4b

Commits on Dec 4, 2024

• Add logs

  gregweng

  committed
  a63161f

  Copy full SHA for a63161f

• Change types in proc scalar_product to RV

  gregweng

  committed
  9edcacc

  Copy full SHA for 9edcacc

• Format log lines

  gregweng

  committed
  7bd6aac

  Copy full SHA for 7bd6aac

• WIP: from logs to alice_view

  gregweng

  committed
  4cfb4bb

  Copy full SHA for 4cfb4bb

• WIP: bug in log -- first Send wont appear ; build_alice_view

  gregweng

  committed
  948ea62

  Copy full SHA for 948ea62

Commits on Dec 5, 2024

• Add two debug proc

  gregweng

  committed
  d7be3e1

  Copy full SHA for d7be3e1

• Fixed the logging problem

  gregweng

  committed
  c8a1896

  Copy full SHA for c8a1896

• Remove debugging procs

  gregweng

  committed
  6c0c7bc

  Copy full SHA for 6c0c7bc

• Proved general binop of RVs preserves independence in pr_eqM and pr_eqM2 (smc_entropy.v) -- prepartion for dotproduct in RV preserves uniform distribution

  gregweng

  committed
  cb51583

  Copy full SHA for cb51583

Commits on Dec 7, 2024

• Debug logs

  gregweng

  committed
  4b40d3b

  Copy full SHA for 4b40d3b

• WIP: try to simulate a generator by init but fallback

  gregweng

  committed
  b3f9d21

  Copy full SHA for b3f9d21

Commits on Dec 8, 2024

• WIP: try to instantiate scalar product but failed

  gregweng

  committed
  a1843d4

  Copy full SHA for a1843d4

Commits on Dec 11, 2024

• WIP: suddeny cannot compare two RV (eq)

  gregweng

  committed
  6eda9a7

  Copy full SHA for 6eda9a7

• WIP: smc_interpreter.v - Cannot infer an internal placeholder of type

  gregweng

  committed
  2f492ae

  Copy full SHA for 2f492ae

Commits on Dec 13, 2024

• WIP: change smc_interpreter log structure

  gregweng

  committed
  24c9f68

  Copy full SHA for 24c9f68

Commits on Dec 14, 2024

• WIP: Try to build the big record

  gregweng

  committed
  9b9a5b7

  Copy full SHA for 9b9a5b7

Commits on Dec 15, 2024

• Can get RV of TX and VX from scalar_product logs

  gregweng

  committed
  aa5bca3

  Copy full SHA for aa5bca3

• get intermediate results from rv inputs

  gregweng

  committed
  28b4caa

  Copy full SHA for 28b4caa

Commits on Dec 17, 2024

• WIP: try to prove r2 unif (problem: dotproduct_rv is not binop for s1Ms2_r1_indep)

  gregweng

  committed
  3677f24

  Copy full SHA for 3677f24

• pr2_unif proved

  gregweng

  committed
  051d634

  Copy full SHA for 051d634

• WIP: try to integrate proofs to smc_interpreter

  gregweng

  committed
  9fbc692

  Copy full SHA for 9fbc692

Commits on Dec 18, 2024

• Move neg_RV lemmas to a new section

  gregweng

  committed
  27ec108

  Copy full SHA for 27ec108

• WIP: seperate sections

  gregweng

  committed
  b06246a

  Copy full SHA for b06246a

• WIP: Put variables back to sections

  gregweng

  committed
  9cdb4b5

  Copy full SHA for 9cdb4b5

Commits on Dec 19, 2024

• Prepare to migrate RVInputs to smc_interpreter

  gregweng

  committed
  4d7286d

  Copy full SHA for 4d7286d

• Prepare for information leakage proof

  gregweng

  committed
  160d42b

  Copy full SHA for 160d42b

• Can embed alice_information_leakage_free into scalar_product_information_leakage_free

  gregweng

  committed
  e129d1b

  Copy full SHA for e129d1b

• WIP: bug when proving x1s2_x1'_indep in smc_interpreter

  gregweng

  committed
  0dcd7d5

  Copy full SHA for 0dcd7d5

Commits on Dec 20, 2024

• Debugging x2s2_x1'_indep in smc_interpreter.v

  gregweng

  committed
  e6826db

  Copy full SHA for e6826db

Commits on Dec 23, 2024

• Commit the list-to-tuple change for the information leakage free proof

  gregweng

  committed
  8ce2d4e

  Copy full SHA for 8ce2d4e

• simplify interpreter + wip proving equivalence of traces

  garrigue

  committed
  601a2bf

  Copy full SHA for 601a2bf

• prove cond_entropyC and finish proof for Alice view

  garrigue

  committed
  c7d8c8d

  Copy full SHA for c7d8c8d

• remove unneeded funext

  garrigue

  committed
  e2ff392

  Copy full SHA for e2ff392

Commits on Dec 30, 2024

• Added is_scalar_product to the interpreter file

  gregweng

  committed
  2515e1d

  Copy full SHA for 2515e1d

• Remove the trace definition before we really need it

  gregweng

  committed
  c7d7e7b

  Copy full SHA for c7d7e7b

• Proved is_scalar_product in smc_interpreter.v

  gregweng

  committed
  33c2cb6

  Copy full SHA for 33c2cb6

• Simplify the Lemma smc_scalar_productP

  gregweng

  committed
  d115195

  Copy full SHA for d115195

Commits on Jan 2, 2025

• WIP: fail at the ps2_unif in smc_interpreter.v

  gregweng

  committed
  151ef25

  Copy full SHA for 151ef25

• Rename in traces_ok

  gregweng

  committed
  d0e7660

  Copy full SHA for d0e7660

Commits on Jan 3, 2025

• Fix the card of 'rV[TX]_n

  gregweng

  committed
  392195b

  Copy full SHA for 392195b

Commits on Jan 5, 2025

• WIP: Encountered type issue between add_RV_unif (finZmodType) and VX (finType)

  gregweng

  committed
  a2054fd

  Copy full SHA for a2054fd

• Renaming some eqn proofs

  gregweng

  committed
  dd5cf2f

  Copy full SHA for dd5cf2f

• Renaming

  gregweng

  committed
  fa397f0

  Copy full SHA for fa397f0

Commits on Jan 6, 2025

• WIP: add_RV_unif type issue

  gregweng

  committed
  b7c2583

  Copy full SHA for b7c2583

Commits on Jan 7, 2025

• Fix interpreter, adding Fail for safety

  garrigue

  committed
  f50c440

  Copy full SHA for f50c440

• x2s2_x1'_indepP

  t6s

  committed
  cde2fc8

  Copy full SHA for cde2fc8

Commits on Jan 9, 2025

• Move proba/smc.v to smc/smc_proba.v

  gregweng

  committed
  f6db9b5

  Copy full SHA for f6db9b5

Commits on Jan 10, 2025

• WIP: about how to express mutual independence for arbitrary lengthed + mixed types RV2

  gregweng

  committed
  4d53176

  Copy full SHA for 4d53176

Commits on Jan 11, 2025

• WIP: proving bob is leakage free

  gregweng

  committed
  b80d33e

  Copy full SHA for b80d33e

• Ltac1

  t6s

  committed
  970b544

  Copy full SHA for 970b544

Commits on Jan 12, 2025

• WIP: r2 inde of x2 s2 x1 s1

  gregweng

  committed
  5327b2c

  Copy full SHA for 5327b2c

• Add SMC party experiments

  gregweng

  committed
  badbf9f

  Copy full SHA for badbf9f

• Experiment: inde_between_parties

  gregweng

  committed
  ae6b710

  Copy full SHA for ae6b710

• rename

  t6s

  committed
  f9cbf79

  Copy full SHA for f9cbf79

• fix

  t6s

  committed
  0e27315

  Copy full SHA for 0e27315

Commits on Jan 13, 2025

• WIP: two lemmas in smc_proba.v: RV2_indeC should be provable; not sure about RV2_inde_reduce

  gregweng

  committed
  f87f021

  Copy full SHA for f87f021

• Remove old comments

  gregweng

  committed
  ca00aa9

  Copy full SHA for ca00aa9

Commits on Jan 15, 2025

• WIP: Try x2s2x1s1_r2_indep

  gregweng

  committed
  eff3a62

  Copy full SHA for eff3a62

Commits on Jan 17, 2025

• Add some comments

  gregweng

  committed
  baf98fc

  Copy full SHA for baf98fc

Commits on Jan 18, 2025

• Finished Alice and Bob information leakage proofs in smc_interpreter.v

  gregweng

  committed
  aecda0e

  Copy full SHA for aecda0e

Commits on Jan 31, 2025

• use bseq for traces

  garrigue

  committed
  bfe90fc

  Copy full SHA for bfe90fc

• clarify alice and bob trace proofs

  garrigue

  committed
  1791a73

  Copy full SHA for 1791a73

• Add scalar_product_is_leakage_freeP to complete the information leakage freedom theorem

  gregweng

  committed
  0d899d4

  Copy full SHA for 0d899d4

Commits on Feb 1, 2025

• small cleanup

  garrigue

  committed
  b8003d9

  Copy full SHA for b8003d9