Helper

DParty_first_erase

File dumas2017dual/dsdp/dsdp_pismc.v

Section dsdp_n_rsteps

Type Lemma

Proof Lines 10

Signature

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

Description

First relay: Init dk; Init v; Send E(v) to Alice; Recv dec from Alice; Recv enc from Alice; 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