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)