Helper

V3_determined_centropy_v2

File dumas2017dual/dsdp/dsdp_entropy.v

Section functional_determination

Type Lemma

Proof Lines 14

Signature

Lemma V3_determined_centropy_v2 : `H([% V2, V3] | [% V1, U1, U2, U3, S]) = `H(V2 | [% V1, U1, U2, U3, S]).

Description

* * Fundamental Principle of Constraint-Based Security When an auxiliary variable is functionally determined by a secret and a constraint, the joint entropy equals the secret's entropy alone. This formalizes the principle that "knowing possible solution pairs gives exactly the same information as knowing the constraint on the secret." This principle underlies many MPC protocols where: - [V2] is the secret to protect - [V3] is an auxiliary/helper variable - [S, U2, U3] form a constraint linking them - Given constraint, [v3] is determined by [V2] (or vice versa)

Uses (0)

This lemma does not use any other lemmas from the stats.

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats