Theorem

US_compromised_leaks_V2

File dumas2017dual/dsdp/dsdp_security.v

Section malicious_adversary_case_analysis

Type Theorem

Proof Lines 37

Signature

Theorem US_compromised_leaks_V2 : US = ConstUS -> ~ `H(V2 | AliceView ) = `H `p_V2.

Description

This theorem shows that if an active adversary controls Alice, it can set U1 and U2 as a special combination (1, 0), which allows revealing `V2` from the result that Alice receives. \cite[\S5.2]{dumas2017dual}.

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