Theorem

dsdp_entropic_security

File dumas2017dual/dsdp/dsdp_security.v

Section dsdp_security

Type Theorem

Proof Lines 17

Signature

Theorem dsdp_entropic_security : `H(V2 | AliceView) = log (m%:R : R) /\ `H(V2 | AliceView) > 0.

Description

DSDP entropic security: H(V2 | AliceView) = log(m) = H(V2) > 0. Since log(m) is the maximum entropy for V2 over Z/pqZ, this means Alice's view is statistically independent of V2: individual secrets enjoy perfect privacy in the sense of Dodis-Smith 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