Helper

bob_combined_value

File dumas2017dual/dsdp/dsdp_program.v
Section dsdp
Type Lemma
Proof Lines 7

Signature

Lemma bob_combined_value : exists rr, bob_combined alice_a3 = E charlie (v3 * u3 + r3 + d2_value) rr.

Description

Lemma: Bob's combined ciphertext encrypts the sum

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