Feasibility of proving a result in TOC and cryptography?

Stream: new members

[João Diogo Duarte]

Hi all, as an effort to learn another proof assistant rather than just EasyCrypt, I want to try out a little project in Lean. I have this result that applies theory of computation to cryptography:

A reduction from cryptographic primitive X to Y means that if X is secure, then Y is secure. In cryptography, we normally use Turing reductions, which means that we can take the X to Y reduction and say that if X is secure relative to oracle O, then so is Y. We then say that X reduces to Y, relative to O. I would like to prove that fully black box reductions allow us to relativise reductions as I just described.

As an example of what I would need from Lean, I'll just quickly recap what a cryptographic primitive is according to https://lucatrevisan.github.io/pubs/rtv04.pdf, which is the starting point for the pen-and-paper proof.

A primitive is a tuple F and R, whereby F = set of all functions (aka implementations) f_i : A_i -> B_i that conform to some behaviour (e.g., hash will compress your input), and R is a list of all Turing machines M and implementations f \in F such that M breaks f per some definition (e.g., finding a collision is difficult). An implementation g is secure if all Turing machines M < g, M> \in R are not probabilistic polynomial time. We say that g is efficient if it is computable by a probabilistic polynomial time turing machine.

Just there, we already need to define Turing machines, infinite list of functions, define interaction between Turing machines, complexity classes, a computational model, what a reduction is etc...

Can anyone help me understand if Lean is a good candidate for this kind of task? I really appreciate it!

[Bolton Bailey]

You might be interested in https://github.com/Verified-zkEVM/ArkLib and https://github.com/dtumad/VCV-io

[Bolton Bailey]

To elaborate a bit more, mathlib has a few definitions of Turing machines (Turing.TM2ComputableInPolyTime), but not much in terms of interaction between them or reductions.

[João Diogo Duarte]

Thanks for the pointers :), I will have a look at the repos you sent, they look promising