Helper

dsdp_ok

File dumas2017dual/dsdp/dsdp_correctness.v

Section dsdp_computational

Type Lemma

Proof Lines 1

Signature

Lemma dsdp_ok : dsdp 15 = ([:: Finish; Finish; Finish], [:: [:: d (v3 * u3 + r3 + (v2 * u2 + r2) - r2 - r3 + u1 * v1); e (v3 * u3 + r3 + (v2 * u2 + r2)); e v3; e v2; d r3; d r2; d u3; d u2; d u1; d v1; k dk_a]; [:: e (v3 * u3 + r3); e (v2 * u2 + r2); d v2; k dk_b]; [:: e (v3 * u3 + r3 + (v2 * u2 + r2)); d v3; k dk_c] ]).

Description

Protocol execution result: running dsdp for 15 steps produces the expected final state with all parties finished and their respective traces. In the idealized scheme, enc(pk, m, r) = m, so ciphertexts are just messages.

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