Zulip Chat Archive

Stream: new members

Topic: Lean for Cryptography


view this post on Zulip Cibo (Oct 18 2019 at 10:44):

Hello,
Can you please give any references on using lean for proving security of ciphers or cryptographic protocols?
Or at least give opinion on possibility of development tools that would help with cryptography?

Im intrigued by possibility of having tool for rapid prototyping crypto primitives construction, but im curious if it be possible to express some probabilistic boundary or computation boundary?

view this post on Zulip Johan Commelin (Oct 18 2019 at 12:00):

@Cibo I'm not aware of any crypto written in Lean so far

view this post on Zulip Johan Commelin (Oct 18 2019 at 12:01):

We certainly have all the ingredients in place to implement RSA.

view this post on Zulip Cibo (Oct 18 2019 at 12:07):

We certainly have all the ingredients in place to implement RSA.

Thanks! Sounds like a nice challenge for a weekend

view this post on Zulip Johan Commelin (Oct 18 2019 at 12:22):

@Cibo You'll probably want to use mathlib. Also, I make no promises about whether the resulting code will run fast enough to work with key sizes >10.

view this post on Zulip Cibo (Oct 18 2019 at 12:28):

@Johan Commelin I am more interested in proving that no adversary would be able to get private key out of public key with probability grater then $\varepsilon$ within time boundary of time $t$. Rather then calculate actual ciphertexts

view this post on Zulip Kevin Buzzard (Oct 18 2019 at 17:45):

But there could in theory be an O(n) algorithm for factoring / breaking your favourite protocol, no?

view this post on Zulip Cibo (Oct 18 2019 at 18:30):

@Kevin Buzzard yes.
That is why I will have to define some assumption(like hardness of factorisation and best known attack on it). I know that there is a shores algorithm, but lets do some basics first.

I would like to end up with set of assumption and proofs s.t. any new cryptographic protocol that would be build can be easily analyzed by hardness of its assumptions(if proof holds).

My question here is: should I start learning lean or my goal is not reachable at all? and I should go back to coq, proverif and tamarin

view this post on Zulip Simon Hudon (Oct 18 2019 at 19:45):

@Cibo you may want to talk to @Joe Hendrix

view this post on Zulip Joe Hendrix (Oct 18 2019 at 20:27):

@Cibo I was involved in a project at Galois where we worked on a protocol specification, and verified some correctness properties (specified in LTL) in Lean 3. We were starting on infrastructure for cryptographic hardness proofs (I was probably going to borrow heavily from FCF), but the project needed to shift directions.
I don't see any theoretical problems in using Lean for this, and I found Lean's metaprogramming and tactic approach quite useful. However, there is relatively little in the way of existing libraries for doing this.

view this post on Zulip Joe Hendrix (Oct 18 2019 at 20:28):

We made all the code we can share available here: https://github.com/GaloisInc/lean-protocol-support. The use case was for a third party block chain system that I was not allowed to share, but the infrastructure is there.

view this post on Zulip Joe Hendrix (Oct 18 2019 at 20:30):

On the crypto side, the repo has SHA2, HMAC, and some basic Merkle tree work. It'd be neat to see more, perhaps a block cipher and public key method.

view this post on Zulip Cibo (Oct 18 2019 at 21:32):

Many thanks @Simon Hudon, @Joe Hendrix ! :big_smile:


Last updated: May 09 2021 at 18:17 UTC