# Zulip Chat Archive

## Stream: general

### Topic: Cryptography proofs

#### Wrenna Robson (Feb 18 2022 at 09:45):

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 (Feb 18 2022 at 17:04):

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 (Feb 24 2022 at 13:27):

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

#### Devon Tuma (Feb 24 2022 at 19:50):

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 (Feb 24 2022 at 19:54):

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 (Feb 24 2022 at 20:43):

iiiiinteresting

#### Devon Tuma (Feb 24 2022 at 21:23):

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 (Feb 24 2022 at 21:24):

Thank you.

#### Wrenna Robson (Feb 24 2022 at 21:29):

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

#### Wrenna Robson (Feb 24 2022 at 21:33):

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

#### Wrenna Robson (Feb 24 2022 at 21:34):

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 (Feb 24 2022 at 21:47):

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 (Feb 24 2022 at 21:50):

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 (Feb 24 2022 at 22:27):

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 (Feb 24 2022 at 22:36):

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

#### Devon Tuma (Feb 24 2022 at 22:37):

To complexity theory?

#### Bolton Bailey (Feb 24 2022 at 23:15):

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 (Feb 24 2022 at 23:20):

You should check out SSProve above.

#### Wrenna Robson (Feb 24 2022 at 23:21):

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 (Feb 24 2022 at 23:21):

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 (Feb 24 2022 at 23:24):

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 (Feb 24 2022 at 23:25):

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 (Feb 24 2022 at 23:28):

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 (Feb 24 2022 at 23:35):

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 (Feb 24 2022 at 23:35):

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

#### Wrenna Robson (Feb 24 2022 at 23:36):

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

#### Wrenna Robson (Feb 24 2022 at 23:37):

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

#### Wrenna Robson (Feb 24 2022 at 23:38):

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 (Feb 24 2022 at 23:40):

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 (Feb 24 2022 at 23:40):

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 (Feb 24 2022 at 23:45):

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 (Feb 24 2022 at 23:47):

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 (Feb 24 2022 at 23:53):

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 (Feb 24 2022 at 23:59):

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 (Feb 25 2022 at 00:00):

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

#### Bolton Bailey (Feb 25 2022 at 00:01):

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 (Feb 25 2022 at 00:02):

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 (Feb 25 2022 at 00:02):

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 (Feb 25 2022 at 00:02):

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 (Feb 25 2022 at 00:03):

yeah that seems very possible.

#### Wrenna Robson (Feb 25 2022 at 00:04):

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

#### Devon Tuma (Feb 25 2022 at 00:04):

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

#### Wrenna Robson (Feb 25 2022 at 00:04):

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 (Feb 25 2022 at 00:05):

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 (Feb 25 2022 at 00:06):

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 (Feb 25 2022 at 00:06):

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 (Feb 25 2022 at 00:09):

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 (Feb 25 2022 at 00:10):

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 (Feb 25 2022 at 00:11):

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 (Feb 25 2022 at 00:12):

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

#### Wrenna Robson (Feb 25 2022 at 00:13):

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 (Feb 25 2022 at 00:13):

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

#### Wrenna Robson (Feb 25 2022 at 00:14):

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

#### Devon Tuma (Feb 25 2022 at 00:14):

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 (Feb 25 2022 at 00:15):

right exactly

#### Wrenna Robson (Feb 25 2022 at 00:15):

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 (Feb 25 2022 at 00:17):

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 (Feb 25 2022 at 00:22):

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

#### Wrenna Robson (Feb 25 2022 at 00:22):

but yes sounds sensible

#### Wrenna Robson (Feb 25 2022 at 00:22):

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

#### Ashvni Narayanan (Jun 04 2022 at 10:11):

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

#### Mario Carneiro (Jun 04 2022 at 12:57):

@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 (Jun 04 2022 at 18:52):

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 (Jun 04 2022 at 19:09):

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 (Jun 06 2022 at 09:39):

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

#### Jeremy Avigad (Jun 09 2022 at 00:22):

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 (Jun 09 2022 at 11:34):

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 (Jun 09 2022 at 11:34):

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

Last updated: Aug 03 2023 at 10:10 UTC