Cryptography proofs

Stream: general

[Wrenna Robson]

Anyone familiar with the SSProve framework/similar efforts to formalise game-based and simulation-based cryptographic proof? If you are, do you know much about whether porting it to Lean would be possible, or even useful? A lot of this work only exists in Coq currently.

[Frédéric Dupuis]

I don't know much about these frameworks (yet!) but I definitely think it would be interesting to have something like that in Lean.

[Wrenna Robson]

I agree! https://github.com/SSProve/ssprove is the theory in question.

[Devon Tuma]

I've been working on implementing a framework similar to https://dash.harvard.edu/bitstream/handle/1/17463136/PETCHER-DISSERTATION-2015.pdf in lean, although I've only been opening PRs to mathlib for the more clearly mathematical portions of it

[Devon Tuma]

It's in a state that you could write proofs of things, but a lot of API's still need to be fleshed out with lemmas to make large proofs workable

[Wrenna Robson]

iiiiinteresting

[Devon Tuma]

This is the computational model I'm using if you're interested (it seems related to the pmf and finite sum stuff you mentioned in another thread): https://github.com/dtumad/crypto_formalization/tree/master/src/computational_monads

[Wrenna Robson]

Thank you.

[Wrenna Robson]

OOI why was it FCF you chose? Have you looked much at the SSP-style stuff (which I think post-dates this)?

[Wrenna Robson]

https://github.com/linesthatinterlace/lean_pdists/blob/main/src/distributions.lean

[Wrenna Robson]

This is the probability stuff I was doing (I wanted to avoid the measure approach that's already there, as it's perfectly great but finitely it's a bit of a sledgehammer, as it were.)

[Devon Tuma]

I haven't looked at SSP much, the main reason for FCF style was it seemed to make rewinding algorithms by simulation easier, which was relevant in trying to prove zero knowledge proofs and signatures are secure.

[Devon Tuma]

SSP style does seem like it might clean up a lot of the stuff about tracking oracle access and simulating oracles that I've been working around

[Bolton Bailey]

I'm also interested in formalization of cryptography, and it's partially why I have been working on a complexity theory PR (#11046). If you're not already aware, there are frameworks like EasyCrypt which allow one to carry out cryptographic proofs, but it seems like none of these really connect their frameworks to formalizations to this, and I was little disappointed by that. Do you know if FCF does this?

[Devon Tuma]

I'm not sure I understand the question. Connecting the framework/formalization to what?

[Devon Tuma]

To complexity theory?

[Bolton Bailey]

Yes. Generally theorems in cryptography are stated in terms of existence or nonexistence of polynomial time algorithms for doing certain tasks, and polynomial time algorithms are usually defined in terms of the number of Turing machine steps it takes to solve a problem. But I don't think any of these frameworks prove, for example, that a composition of two polynomial-time functions is polynomial time.

[Wrenna Robson]

You should check out SSProve above.

[Wrenna Robson]

It's -- as far as I am aware -- the most up-to-date approach to this sort of formalisation. Better than EC in that regard imo.

[Wrenna Robson]

Eric Wieser said:

(wrong thread Wrenna Robson ? You can edit the title of your message to move it)

Hmm, I thought I'd correctly edited the title now, but it hasn't appeared.

[Wrenna Robson]

The thing that SSProve does is that it implements a recent framework for properly compositional proofs - using some kinda cool monadic stuff. A port of SSProve into Lean would be highly desirable IMO... currently it only exists in Coq. But I think we probably have all the tools you'd need - it's just a matter of doing it in a Lean/mathlib ideomatic way.

[Wrenna Robson]

Bolton Bailey said:

Yes. Generally theorems in cryptography are stated in terms of existence or nonexistence of polynomial time algorithms for doing certain tasks, and polynomial time algorithms are usually defined in terms of the number of Turing machine steps it takes to solve a problem. But I don't think any of these frameworks prove, for example, that a composition of two polynomial-time functions is polynomial time.

This is sort-of true, but the simulation-based proofs framework is a little trickier in a sense. I guess it's not quite at the same level of abstraction.

[Bolton Bailey]

Thanks for the SSprove link. This seems like another good example - I search "polynomial" in the repository and get no hits.
My advisor is getting me into Universal Composability, so I'm actually drafting a plan to prove some UC theorems in Lean.

[Wrenna Robson]

Yeah I'm currently working out what my next course of research in my PhD is going to involve, I work in similar lines (though I'm interested in different forms of verification also) in general.

[Wrenna Robson]

I'd be interested to keep updated in what you're up to.

[Wrenna Robson]

I'm not sure SSProve necessarily needs polynomial-time stuff for what it does.

[Wrenna Robson]

I believe SSProve is based off some of the UC stuff, maybe some of Maurer's Abstract Cryptography things.

[Wrenna Robson]

I'm mainly interested in Lean for this because I'm interested in PQC, and for some of that it seems like you'd need quite a developed maths library - which Lean has, of course.

[Bolton Bailey]

Cool! You might be interested to know that a bit of the math behind quantum info theory has been formalized in mathlib here (though I think this is all there is).

[Devon Tuma]

The FCF approach defines polynomial complexity but not necessarily in terms of Turing machines. Algorithms are implemented by extending the lean base language with monads for sampling distributions and oracle access (Although these monads are a lot simpler than the monads in SSProve).

Since algorithms are essentially Lean functions (modulo the binding of the monads), polynomial complexity is just some predicate polynomial_complexity : (A -> B) -> Prop on Lean functions (which then naturally extends to the monad functions). Because of function extensionality, this predicate essentially means "some implementation of this function is polynomial time".

The approach to defining this is to just assume some primitive functions (e.g. id or prod.fst) are polynomial time, and have axioms to for things like "a composition of polynomial time things is polynomial time". Ideally it would be better to have something like "this function is realized by a polynomial time Turing machine", but I'm not sure if that is something the complexity theory in Lean can prove.

[Devon Tuma]

This is also my current research project in my PhD so I'd also be interested in staying updated on other cryptography work people are doing in Lean

[Bolton Bailey]

Devon Tuma said:

The FCF approach defines polynomial complexity but not necessarily in terms of Turing machines. Algorithms are implemented by extending the lean base language with monads for sampling distributions and oracle access (Although these monads are a lot simpler than the monads in SSProve).

Since algorithms are essentially Lean functions (modulo the binding of the monads), polynomial complexity is just some predicate polynomial_complexity : (A -> B) -> Prop on Lean functions (which then naturally extends to the monad functions). Because of function extensionality, this predicate essentially means "some implementation of this function is polynomial time".

The approach to defining this is to just assume some primitive functions (e.g. id or prod.fst) are polynomial time, and have axioms to for things like "a composition of polynomial time things is polynomial time". Ideally it would be better to have something like "this function is realized by a polynomial time Turing machine", but I'm not sure if that is something the complexity theory in Lean can prove.

Right, that's what I thought. The "a composition of polynomial time things is polynomial time" proof is what the bulk of the #11046 PR is about (using the basis of partially recursive functions, though one could do it with TM's too to be complete). I guess it's not too big a novelty just to carry out the composition proof and attach it to the bottom of a framework like this, but I like the idea of being able to say that we haven't written any code that isn't checked itself by another theorem prover.

[Devon Tuma]

I agree that it's not ideal since it is just sort of tacked on. I'm not super familiar with complexity theory in Lean, is there a way to connect it to Lean functions themselves? Or is it fixed to some internal representation of functions?

[Wrenna Robson]

Devon Tuma said:

This is also my current research project in my PhD so I'd also be interested in staying updated on other cryptography work people are doing in Lean

Great. I am - sort of at a crossroads and I'm not sure what I do next will involve Lean (I might not be good enough at it...) but I'm SUPER interested in hearing about the work people do.

[Wrenna Robson]

I've thought a bit about trying to formalise some of the homomorphic encryption constructions in Lean, actually.

[Bolton Bailey]

Devon Tuma said:

I agree that it's not ideal since it is just sort of tacked on. I'm not super familiar with complexity theory in Lean, is there a way to connect it to Lean functions themselves? Or is it fixed to some internal representation of functions?

You could look at tm2_computable_in_poly_time, this is a structure for wrapping a statement about computability with a function.

[Frédéric Dupuis]

You might also want to check out some of the work done in Isabelle, for example this formalization of the Constructive Cryptography framework.

[Wrenna Robson]

Frédéric Dupuis said:

You might also want to check out some of the work done in Isabelle, for example this formalization of the Constructive Cryptography framework.

aye, I'm familiar with this paper - it's nice

[Devon Tuma]

Wrenna Robson said:

The thing that SSProve does is that it implements a recent framework for properly compositional proofs - using some kinda cool monadic stuff. A port of SSProve into Lean would be highly desirable IMO... currently it only exists in Coq. But I think we probably have all the tools you'd need - it's just a matter of doing it in a Lean/mathlib ideomatic way.

Looking at the eprint for SSProve (https://eprint.iacr.org/eprint-bin/getfile.pl?entry=2021/397&version=20210526:113037&file=397.pdf), I think that it seems fairly possible to implement some form of SSProve on top of the foundations given in FCF, which is something the authors mention in the related work section

[Wrenna Robson]

yeah that seems very possible.

[Wrenna Robson]

Oh - I actually re-implemented and extended the proofs in this paper in Lean last year. https://eprint.iacr.org/2020/1493

[Devon Tuma]

Essentially swapping out their free monads for the monads in FCF, and building packages in the same way on top of that

[Wrenna Robson]

It's not written up anywhere, and it's more maths-y. But maybe I should put that somewhere public, it's quite interesting.

[Wrenna Robson]

Devon Tuma said:

Essentially swapping out their free monads for the monads in FCF, and building packages in the same way on top of that

I think a key aim of any such things - which a lot of stuff fails at, incidentally - is making it accessible to cryptographers who are not formal verification people.

[Devon Tuma]

Bolton Bailey said:

Devon Tuma said:

I agree that it's not ideal since it is just sort of tacked on. I'm not super familiar with complexity theory in Lean, is there a way to connect it to Lean functions themselves? Or is it fixed to some internal representation of functions?

You could look at tm2_computable_in_poly_time, this is a structure for wrapping a statement about computability with a function.

This does seem like it would integrate fairly well, I'll try experimenting with using that when I have some time to dig into it

[Wrenna Robson]

It's desirable to create a setting where people can "just do proofs" without having to think too much about what's going on underneath.

[Wrenna Robson]

It's not as bleeding-edge, but this is a nice undergraduate approach to simulation-style proofs that they mention in the SSProve paper; I mention it because in a sense just as it's nice to be able to do "undergraduate maths" in Lean it would be nice to be able to do things to this level of formality. https://joyofcryptography.com/

[Devon Tuma]

So far I've found Lean to be fairly good at hiding a lot of the complexity of the implementation details of the system, so that it's mostly possible to "just do proofs" (mainly through use of tactics and lots of @[simp] lemmas). Although I may be biased as someone who has worked a lot on doing math in Lean

[Wrenna Robson]

Oh I 100% agree - that's a large part of my interest in it. To be honest when I read some Coq code my eyes glaze over...

[Wrenna Robson]

There's just a lot of quality-of-life stuff in Lean.

[Wrenna Robson]

Reading the FCF comparison in the SSProve paper and that does sound promising. The FCF approach seems more, I don't know - I like it better than the deep embedding of EasyCrypt (honestly while some people really like EC I'm colder on it, but maybe I just need more experience).

[Wrenna Robson]

If you would be at all interested in collaboration on your work at all, do let me know :)

[Wrenna Robson]

If we got a bunch done maybe there's a paper in it, but I'm just keen to help out really.

[Devon Tuma]

I also really like the shallow-embedding approach because it makes the semantics of the system much easier to work with since all of the theory about Lean programs applies directly to these programs, which something like EC doesn't have

[Wrenna Robson]

right exactly

[Wrenna Robson]

it feels like with SSProve they built it on EC because EC exists and implementing it in things is just a matter of porting...

[Devon Tuma]

Wrenna Robson said:

If you would be at all interested in collaboration on your work at all, do let me know :)

I'd definitely be open to that (although I'd probably want to take some time to clean up and document a lot of the code before asking someone else to try and understand it :sweat_smile: )

[Wrenna Robson]

"Clean up and document the code" - why do this, nobody else who releases formal crypto tools ever does ;)

[Wrenna Robson]

but yes sounds sensible

[Wrenna Robson]

wrenna.robson.2019@live.rhul.ac.uk <- this is my work address

[Ashvni Narayanan]

Hi all, just out of curiosity, has there been any work done on formalizing what a proof /zero knowledge proof is?

[Mario Carneiro]

@Jeremy Avigad did some work on verifying computations over finite fields for a blockchain application, not sure if zero knowledge proofs were defined explicitly but I think they feature in the formalization

[Jeremy Avigad]

The formalization is here: https://dl.acm.org/doi/abs/10.1145/3497775.3503675. The technology is built on top of the STARK proof protocol, but the protocol does not play a direct role in the formalization. The protocol provides efficient ways of verifying that that proof has/knows solutions to a parameterized family of polynomials, which you can use to encode information, computation, etc. Our formalization starts with a certain family of polynomials, and shows that they encode computation in a particular machine model. (Subsequent work verifies code wrt that machine model.)

[Bolton Bailey]

You may also be interested in my project formalizing SNARKs, which formalizes the soundness proof of Groth '16 and a few other pairing-based SNARKs.

[Wrenna Robson]

@Jeremy Avigad has any of your code for this found its way into mathlib?

[Jeremy Avigad]

Sorry to be slow to respond -- I am on a bike trip now -- but no, it hasn't. The original formalization is in a public repository. There is a file, util.lean or something like that, that has a few things that can perhaps go into mathlib.

[Wrenna Robson]

I was trying to do some work with bitvectors the other day and it's oddly tricky... even using nat.bits has issues. And it's weird that bitvectors don't seem to work nicely with nat.bits...

[Wrenna Robson]

(I noticed you had done some work on this.)