Lean for Cryptography

Stream: new members

[Cibo]

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?

[Johan Commelin]

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

[Johan Commelin]

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

[Cibo]

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

Thanks! Sounds like a nice challenge for a weekend

[Johan Commelin]

@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.

[Cibo]

@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

[Kevin Buzzard]

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

[Cibo]

@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

[Simon Hudon]

@Cibo you may want to talk to @Joe Hendrix

[Joe Hendrix]

@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.

[Joe Hendrix]

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.

[Joe Hendrix]

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.

[Cibo]

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