Theorem

dsdp_constraint_centropy_eqlogm

File dumas2017dual/dsdp/dsdp_security.v

Section dsdp_security

Type Theorem

Proof Lines 13

Signature

Theorem dsdp_constraint_centropy_eqlogm : `H(VarRV | CondRV) = log (m%:R : R).

Description

Core entropy bound: H((V2,V3) | constraint view) = log(m). Instantiates the general DSDP entropy analysis with security hypotheses. Shows Alice learns exactly log(m) bits about Bob/Charlie's joint input, not the full log(m^2) bits - proving entropic security.

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