cryptolib

Stream: computer science

[Wrenna Robson]

I know that there have been various projects to do various cryptography related things in Lean in the past - e.g. some of my own work, Joey Lupo's Cryptolib (https://github.com/JoeyLupo/cryptolib/tree/main) and more. I think there's also the work of ArkLib (https://github.com/Verified-zkEVM/ArkLib).

I would like to propose that a library in the vein of mathlib or cslib would be desirable, focused on cryptography - both implementing cryptography and proving things about it. Perhaps this project already exists and I'm not aware of it - but I am not aware of it!

I would like to be involved in such a project but I cannot do it alone - so I would like to ask who IS interested. I think having one repo for cryptography in Lean is desirable compared to many small repos each implementing various things, and having an explictly cryptographic focus is also desirable.

I think any such repo will probably be downstream of mathlib, cslib but I suppose I am willing to hear arguments to the contrary.

[Fabrizio Montesi]

A mathlib dependency would be natural, since I expect you'll have good use for groups and related types, right?
Cslib as well, because we're developing languages/frameworks to write and verify sequential and concurrent software. Combining those with crypto primitives would enable, for example, writing and verifying security protocols. Some of the theory in cslib might help with proving crypto primitives correct, too.
Have you considered getting this _into_ cslib?

[Quang Dao]

As the main developer of ArkLib, I definitely agree on having a central cryptolib repo. There are a ton of cryptography to be formalized and much work to set things up - our effort on VCVio is meant to be the base layer for formalization.

Happy to talk more over a call or DM

[Wrenna Robson]

It might be that it fits better into CSLib, but my feelings is that the concerns of cryptographers are adjacent to but not the same as those of theoretical computer scientists.

[Wrenna Robson]

Possibly it might be the case that CSLib makes use of it as a dependency.

[Quang Dao]

My sense is that cryptographers are a distinct enough group (separate conferences, separate preprint website) that we should have a separate cryptolib repo as well

[Fabrizio Montesi]

I think it'd make good sense, but it'd also be good to keep an eye on what goes where as things develop. For example, some proofs involve defining an operational semantics, which makes cslib or something downstream of it a natural place to carry them out.

[Fabrizio Montesi]

I wanna avoid ending up in a circular dependency problem. :-)

[Wrenna Robson]

Yes definitely.

[Wrenna Robson]

@Quang Dao who are you aware of who is also doing active work in this area currently?

[Mukesh Tiwari]

@Wrenna Robson I use Rocq to formalise my crypto implementation related to electronic voting. (My main goal is to always extract a computer program from my formalisation).

[Wrenna Robson]

Yeah I'm aware of a lot more work in Rocq in these areas (and in custom tools like EasyCrypt).

[Quang Dao]

The people involved in ArkLib are all I know. There are also some work from the Aeneas team.

[Kajetan Granops]

Hi, this seems like the best place to ask about my project! Our first idea for my project was to somehow expand on Joey Lupo's library that @Wrenna Robson mentioned, but from looking at VCVio I get the impression that VCVio already is an expansion of the idea of Joey's cryptolib, so I think it makes more sense to use VCVio instead of porting cryptolib to Lean4.

[Quang Dao]

Tagging @Devon Tuma who is the main developer of VCVio. We would love to hear what application you have in mind for the library

[Wrenna Robson]

I am personally strongly of the view that it would be desirable to both have good, correct, performant, secure implementations of common cryptographic primitives and protocols in Lean, but also link these to both security proofs and proofs of correctness.

[Wrenna Robson]

There's quite a lot of prior work in this area in Rocq and in more specialised tools like EasyCrypt and many others.

[Wrenna Robson]

This is why I think performant implementations are particularly of interest to me.

[Wrenna Robson]

I don't personally work much with the EasyCrypt/Jasmin stack but I work for François Dupressoir who very much does. Trying to get Cameron, who also works for/with him and has done some work with trying to implement EasyCrypt semantics in lean, to come here and share thoughts.

[Quang Dao]

Definitely, all of this is of interest to me & many others. The path toward such a goal is unclear to me however. On the implementation side, I think we should make use of recent tooling (like LeanMLIR) in addition to copying / adapting Jasmin

[Quang Dao]

This is for instance what we are aiming for at ArkLib. At the minimum, have executable spec of SNARK protocols, but moreover, have these spec either be verified to be equivalent to extracted Rust implementation, or, verifiably compile these spec directly to a lower level language (through toolchains like MLIR)