Helper

alice_view_to_cond

File dumas2017dual/dsdp/dsdp_entropy.v

Section semi_honest_case_analysis

Type Lemma

Proof Lines 74

Signature

Lemma alice_view_to_cond (A : finType) (Xvar : {RV P -> A}) : (P |= [% Dk_a, R2, R3] _|_ Xvar | [% V1, U1, U2, U3, S]) -> `H(Xvar | AliceView) = `H(Xvar | [% V1, U1, U2, U3, S]).

Description

Generic helper: Strip encryptions from AliceView and apply conditional independence. Given: X is conditionally independent of [Dk_a, R2, R3] given CondRV Proves: H(X | AliceView) = H(X | CondRV) This is reused in dsdp_security.v for the entropic security proof.

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