Helper

dsdp_var_entropy

File dumas2017dual/dsdp/dsdp_entropy.v

Section dsdp_var_entropy

Type Lemma

Proof Lines 5

Signature

Lemma dsdp_var_entropy : `p_VarRV = fdist_uniform card_msg_pair -> `H `p_VarRV = log (m%:R * m%:R : R).

Description

Unconditional entropy of private inputs (V2, V3) when uniformly distributed. Since V2, V3 are private inputs from Bob and Charlie respectively, assuming uniform distribution gives H(V2,V3) = log(m²) = 2*log(m). Combined with the conditional entropy result H(V2,V3 | view) = log(m), this shows DSDP leaks log(m) bits but preserves log(m) bits of entropy. The security argument (joint_centropy_reduction at end of file) shows that H(V2,V3 | AliceView) = H(V2 | AliceView), i.e., knowing V3 given the constraint adds no information beyond knowing V2.

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