Note: this EasyCrypt development no longer checks with the current version of EasyCrypt. Unfortunately, to go back to a version of EasyCrypt for which the proof checks, one would also have to go back to an earlier version of Why3. It seems changes in how introduction patterns are handled is at least part of the problem. At this point, it doesn't seem worthwhile to update the proof. Instead we are working toward a better UC in EasyCrypt methodology, as the original proof was too laborious to scale up anyway. This new methodology will involve translation from the UC DSL, and you can see work-in-progress in smc-next.
We formalized the proof of the UC security of secure message communication (SMC) using a one-time pad that's agreed using Diffie-Hellman key exchange.
-
We first proved the security of Diffie-Hellman key exchange, reducing it to the Decisional Diffie-Hellman assumption for a constructed DDH adversary. This proof makes use of EasyCrypt's eager/lazy random sampling facilities, because, in the real and ideal functionalities, the DDH exponents are chosen in the middle of the functionalities' execution.
-
We then use the security of Diffie-Hellman key exchange to prove the security of secure message communication using a one-time pad agreed by the parties using D-H key exchange. This involves proving an instance of the UC composition theorem, as well as making use of the transitivity of UC security.
Our goal in this case study was to test our EasyCrypt UC architecture, illustrating how instances of UC's composition operation and theorem may be formalized in EasyCrypt.
The proof is complete, giving us confidence that our EasyCrypt UC architecture is sound. But there is much work to be done before the method can scale-up to realistic protocols. Most importantly:
-
Proving relationships between structurally dissimilar programs involved heavy use of manual symbolic program evaluation, guided by case analysis - essentially running programs using repeated applications of the EasyCrypt tactics
sp(for pushing assignments into the precondition),inline(for inlining procedures) andrcondt/rcondf(for reducing conditionals/while loops for which the truth/falsity of their boolean expressions can be established). There is a pressing need for better EasyCrypt support for symbolic evaluation. -
In our case study, we proved an instance of the UC Composition Theorem, via the definition of the composed environment and bridging lemmas. We are now generalizing this work, producing a generic version of these definitions/proofs. To obtain needed instances of the composition theorem, we’ll then instantiate the generic definitions/proofs, and automatically generate some additional bridging definitions and proofs.
-
Writing functionalities, simulators, etc., directly in EasyCrypt is somewhat tedious and error prone. We plan to develop a domain specific language for expressing functionalities, etc., with the short term goal of automatically translating DSL programs to actual EasyCrypt code.
This work is described in the extended version of the CSF 2019 paper, EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security.
ListPO.ec- prefix ordering on listsRedundantHashing.eca- redundant hashing (eager/lazy random sampling)