Universal Composability in Lean

A formalization of the UC Cryptographic framework in Lean 3.

I started this repo as a class project. I have been thinking it might be nice at some point to port it to Lean 4 and develop it more, maybe integrating some of my other work.

Some potentially relevant papers/links:

• David Heath's Course on MPC
• "A Simpler Variant of Universally Composable Security for Standard Multiparty Computation"
• "Algebraic Adversaries in the Universal Composability Framework"
• "Categorical composable cryptography" (Note mathlib defines Symmetric Monoidal Categories)