This is the repository of the EasyUC Project, whose aim is to mechanize proofs of Universally Composable (UC) Security using the EasyCrypt proof assistant.
The principal designers and implementors of EasyUC are
- Tomislav Petrovic (formerly Boston University, tomislav@bu.edu)
- Alley Stoughton (Boston University, stough@bu.edu)
and the initial development of EasyUC was done in collaboration with
- Mayank Varia (Boston University, varia@bu.edu)
- Ran Canetti (Boston University, canetti@bu.edu)
Contributions to EasyUC were also made by:
- Megan Chen (Aarhus University, megchen@bu.edu)
- Tarakaram Gollamudi (gollamudi.ram@gmail.com)
- Uğur Y. Yavuz (Boston University, uyyavuz@bu.edu)
In our architecture, functionalities (real protocols, or ideal functionalities) have hierarchical addresses, and we build abstractions that route messages to their destinations, modeling the coroutine-style communication of UC.
In our first full example, we formalized the proof of the UC security of secure message communication using a one-time pad that's agreed using Diffie-Hellman key exchange. Our goal in this example was to test our EasyCrypt UC architecture, illustrating how instances of UC's composition operation and theorem may be formalized in EasyCrypt.
This work is described in the extended version of the CSF 2019 paper, EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security.
We have designed and implemented a parser, typechecker and interpreter for a domain specific language (DSL) for expressing functionalities (protocols and ideal functionalities) and simulators. The DSL allows crypto theorists to easily write and understand functionalities and simulators. Its design was driven by the expression of functionalities and simulators in our EasyCrypt architecture for UC. But it allows expression at a much higher level, avoiding all the message-routing boilerplate. DSL type-checking prevents errors like badly formed messages (e.g., ones with bad source addresses), simulators that interfere with communication between environment and adversary, or violations of the coroutine model (trying to send two message in sequence, without control having first returned). We are working toward a translator from the DSL into EasyCrypt, where the sequence of games security proofs will be mechanized.
This work was supported by the National Science Foundation (NSF) under grant CNS-1801564 "Towards Mechanized Proofs of Composable Security Properties" and by the Defense Advanced Research Projects Agency (DARPA) under Contract No. N66001-22-C-4020. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of NSF or DARPA.