Helper

ConstUS_n_discloses_V1

Section malicious_n

Type Lemma

Proof Lines 6

Lemma ConstUS_n_discloses_V1 (US VS : {RV P -> {ffun 'I_n_relay.+1 -> msg}}) : US = (fun _ => ConstUS_n) -> Dotp_n_rv US VS = (fun t => VS t ord0).

If Alice sets US = e_1, she can extract V_1

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...