Crypto and leftover hash lemma

Stream: general

[Ashley Blacquiere]

I'm working on a potential crypto-related project with @Hart Montgomery and others and we're just in the process of doing a little due diligence to see if anyone else has any in-progress contributions that might be in line with our goals. In particular, we're interested in formalizing the leftover hash lemma and definitions for entropy.

I've seen a few crypto-related threads pop up in ZulipChat searches, and it looks like there has been some progress made for some crypto applications (@Joe Hendrix and @Joey Lupo ?) , but we wanted to try to cast the net wide to see what else might be happening. We'd like to ensure that our work is beneficial to the community as well, and so would be happy to connect with anyone else who has a related interest. If this sounds like you, feel free to reply to this thread, or to get in touch directly with @Hart Montgomery or myself.

[Joe Hendrix]

@Ashley Blacquiere That sounds interesting. I have a small side project where I am formalizing one of the post-quantum algorithms (Classic McEliece) as an experiment. It currently uses Lake to build a bunch of code from OpenSSL and the reference implementation. McEliece needs random numbers for key generation and encryption, but I don't need to reason about distributions.
I'd definitely be interested in learning more about your project as you make progress.

[Frédéric Dupuis]

I'm very interested in this as well! My long term goal here is to formalize the basic mathematical tools of quantum information theory and cryptography, which include various information measures like the min-entropy and things like the leftover hash lemma. I say "long term" here because the main challenge is to do this at the right level of generality: we would want definitions that cover both classical probability distributions (possibly continuous) and quantum states, and this requires a lot of background in C*-algebras to even be able to define the entropy in that general setting.

However, the min-entropy should be a lot easier to define, and the classical leftover hash lemma definitely looks doable right now -- keep me posted!

[Ashley Blacquiere]

Thanks, @Joe Hendrix and @Frédéric Dupuis! That's good to hear on both counts. TBH the mathematics of it is not my area of expertise - @Hart Montgomery will have a better understanding of our cryptographic goals. We'll definitely keep in touch though - thanks for reaching out!

[Hart Montgomery]

@Joe Hendrix That sounds really interesting. I'm curious: how are you handling McEliece without reasoning about distributions? I haven't thought about this much (so maybe I'm missing something obvious), but it seems like you'd need some way to formalize the fact that the noise distribution is appropriate (which would necessitate reasoning about distributions). Thanks!

[Joe Hendrix]

@Hart Montgomery I think it will be relevant to reason about distributions eventually -- I'm kind of learning as I go. At the moment, I'm working on some basic definitions and arithmetic solving.
I think I can prove decryption succeeds if encryption does without reasoning about distributions, but showing the noise distribution has good entropy given a uniform random number generator would likely require more formalization effort.

[Hart Montgomery]

@Joe Hendrix @Ashley Blacquiere Thanks a lot for your response Joe! I guess I should be more precise: at some point, you will need to show that a McEliece ciphertext looks indistinguishable from random in your security proof. At this point, you need to apply some lemma/theorem based on the McEliece assumption itself, which says that, very informally, code words plus some noise are indistinguishable from random. This lemma/theorem needs to implicitly "check" in Lean that the noise distribution is appropriate in the formal proof.

This kind of reasoning seems pretty tricky to do in Lean (or even something like Coq), which is why, to my knowledge, there don't seem to be a lot of formal proofs of lattice-based cryptosystems. We are currently trying to figure out the cleanest way to write such kinds of statements in lean--if you have any ideas, we'd love to hear them!

Thanks for your time and for reading this!