Helper

joint_centropy_reduction

File dumas2017dual/dsdp/dsdp_entropy.v

Section semi_honest_case_analysis

Type Lemma

Proof Lines 5

Signature

Lemma joint_centropy_reduction : `H([% V2, V3] | AliceView ) = `H(V2 | AliceView).

Description

Joint conditional entropy reduction: H(V2,V3 | AliceView) = H(V2 | AliceView). V3 adds no additional entropy because it is functionally determined by V2 and the constraint. Used in the entropic security proof (dsdp_security.v).

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