Helper

DParty_intermediate_erase

File dumas2017dual/dsdp/dsdp_pismc.v

Section dsdp_n_rsteps

Type Lemma

Proof Lines 10

Signature

Lemma DParty_intermediate_erase self alice_src upstream downstream dk' v' r1' r2' : erase (@DParty_intermediate AHE ek self alice_src upstream downstream dk' v' r1' r2') = pInit (priv_key dk') (pInit (d v') (pSend alice_src (e (enc (ek self) v' r1')) (pRecv alice_src (fun d0 : data => match std_from_enc (AHE:=AHE) d0 with | Some enc0 => pRecv upstream (fun d1 : data => match std_from_enc (AHE:=AHE) d1 with | Some enc1 => match dec dk' enc1 with | Some m0 => pSend downstream (e (Emul enc0 (enc (ek downstream) m0 r2'))) Finish | None => Fail end | None => Fail end) | None => Fail

Description

Intermediate relay: Init dk; Init v; Send E(v) to Alice; Recv enc from Alice; Recv dec from upstream; Send product to downstream

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