Formalizing Sphinx in Lean
A Lean formalization of the Sphinx packet format, generic over its cryptographic primitives, and what it does and doesn’t prove.
A Lean formalization of the Sphinx packet format, generic over its cryptographic primitives, and what it does and doesn’t prove.