Helper

DParty_last_erase

File dumas2017dual/dsdp/dsdp_pismc.v

Section dsdp_n_rsteps

Type Lemma

Proof Lines 7

Signature

Lemma DParty_last_erase self upstream dk' v' r1' r2' : erase (@DParty_last AHE ek self upstream dk' v' r1' r2') = pInit (priv_key dk') (pInit (d v') (pSend alice_idx (e (enc (ek self) v' r1')) (pRecv upstream (fun d0 : data => match std_from_enc (AHE:=AHE) d0 with | Some enc0 => match dec dk' enc0 with | Some m0 => pSend alice_idx (e (enc (ek alice_idx) m0 r2')) Finish | None => Fail end | None => Fail end)))).

Description

Last relay: Init dk; Init v; Send E(v) to Alice; Recv dec from upstream; Send re-encrypted to Alice

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