search

easyuc / EasyUC

Experiments with Universal Composability in EasyCrypt
30 stars 1 forks source link

Admitted high-end cryptographic primitives for applied cryptographers? #1

Closed weikengchen closed 5 years ago

weikengchen commented 5 years ago

There are possibly two lines of security/cryptography works:

EasyCrypt and many of its descendants, usually game-based proofs, are suitable for the first sort of works.

EasyUC, allowing the use of ideal functionalities, is useful for the second sort of works.

For example, in the second line, for one who wants to do Yao's Millionaires' Problem today, this person can simply invoke the general-purpose secure multiparty computation protocol (like AG-MPC, SPDZ). The security proof should, therefore, be trivial; an ideal case is like:

Require Import EasyUC_SecureMultiPartyComputation.

lemma ymp_security .....
proof.
    crush.
qed.

(should be more complicated in practice)

However, this is very hard today in EasyUC, because most of the high-end primitives like general-purpose MPC have not yet been implemented/proved. Proving these primitives likely requires a lot of works -- SPDZ builds on LWE, FHE. AG-MPC builds on specialized protocols from garbled circuits and OT. There is a huge gap from the currently written proofs to the state-of-the-art big systems.

So, what if, EasyUC first has/admits a bunch of ideal functionalities for these high-end primitives, like secure multi-party computation, like general-purpose zero-knowledge proofs, such that one who is building a big protocol using standard crypto can verify that their construction is secure in EasyUC, assuming there are EasyUC-secure realizations for these primitives.

How likely would EasyUC be equipped with these high-end primitives first, likely without proofs temporarily, but just the ideal functionalities?

alleystoughton commented 5 years ago

We definitely have in mind defining a variety of ideal functionalities, in advance of possibly defining real functionalities and proving UC security for them. First up, though, is finishing the design and implementation of a DSL for expressing functionalities and simulators. We are also working towards changes in EasyCrypt that will make our proof approach scale up.

weikengchen commented 5 years ago

Thanks for the information. Will wait for the EasyUC DSL; I think many people are waiting for that DSL.

It would be promising if one in the future can program their prototype in this DSL so their implementation's code immediately carries the proof. Otherwise, even if a protocol is UC-secure, it is usually unknown where the code is also UC-secure.

For the scaling-up problem, I don't know how long it takes at this moment for EasyUC to prove SMC, but I see that there are two separate performance demands:

(1) Fast for the first cryptographer who writes the proof to see that the proof goes through. (Probably an ec file with a bunch of time-consuming crush)

(2) Fast for other cryptographers to verify that the proof does go through. (Probably a special file without crush; instead, a few hints are included to help the verifier check the proof efficiently, like "Verifier, use #15-#21-#47-#36." instead of "Verifier, simplify; verifier, omega.").

Even if the first one is hard, probably the second one is more hopeful.

alleystoughton commented 5 years ago

I think you have a model of EasyCrypt being more automated than it is; the search tree is just too big, in general. Once one has an EasyCrypt proof, though, running the tool to check it is generally quick. We're working toward dramatically decreasing the effort needed to construct a new proof using our UC framework.

We are also interested in connecting high-level proofs of protocol security, with verified implementations of those protocols.

weikengchen commented 5 years ago

Excited to hear about that!