leanXMSS/leanSPHINCS in Lean 4

Transcript

Okay, so this talk will be about security proof of signature schemes like Lean Sphinx, Lean XMSS in Lean. And before I start I want to say two things. The first is I did not do that that formalization. So all credits go to Emil and the AI. Um, so I guess if you see something here that you like a lot, that's please credits to Emil. If you see something that you don't like, the AI. Um, okay, and yeah, so the second thing I want to say is I'm not a Lean expert. So when I confuse terminology, please forgive me and please the Lean experts correct me

if needed. Uh, I will just walk through the statement from a sort of high-level perspective and try to convince you that morally they show the right thing. Okay. So what I want to focus on is what do we prove? Because usually when we do this sort of AI plus Lean workflow, we don't care so much about the proof itself. Lean will check that for us, but we care about what is proven. Is it really the thing we care about? So we focus on the statement that we prove. Now what in this context what is the statement? What does it consist of? So the first component is of course we need to define what is a signature scheme, what are the algorithms, what is the object that we study here, and yeah,

what is the API. Uh, then we need to define what it means that this thing is secure. So we need to use security definition. In cryptography we do that via security games. And we want to say something about the bits of security. I think we have talked already a lot about bits of security here and there in this workshop. I will talk even more about it. Um, and what is also part of the statement is of course what is the scheme that we that we look at? I will not look at that in the talk. So, we will look at Sphincs and XMSS. I assume you have some idea how they look like, but everything that I say will essentially apply to all signature schemes constructed in the

random oracle model, and that's why it's also useful preparation for sig.gov. Okay. So, we will the the schemes we care about are Lean Sphincs and Lean XMSS, and I think here the capitalization is is correct. And just to remind you, we have we have heard about it. These are two signature schemes, hash-based. One is stateful, one is stateless, and we very roughly think about one of them as being used in the Ethereum consensus layer to sign attestations. This is when validators vote for blocks, and the other one is for signing transactions. So, if Alice sends coins to to Bob, she would use a Sphincs.

Okay. As I said, I will not talk about how do these schemes work, but nonetheless, implicitly I have in my head that we talk about this family of schemes, stateless schemes. If you consider XMSS and stateful schemes, the definitions change a little bit because you know, the API is different, the security notion is a little bit different, but I will focus on this one. So, standard signature schemes. Okay. So, our goal is to formalize that these schemes are secure in Lean 4. And now, the first thing I want to point out is this is not the only thing that should be our goal because if this is the only goal that I have and we make this the only restriction for for example auto

research, then there's a very simple scheme that is 128-bit secure, and that does not that essentially has a signature size of zero, which is the scheme where the verifier always rejects. Okay. So, it's very important that we also prove correctness. So, when you look at cryptography papers, usually this is sort of ignored or there's like one sentence that says correctness follows by inspection, but if we are now in a world where the AI writes schemes and submits it to auto research challenges, then we really need to have that as an explicit requirement.

Okay, nonetheless I want to talk about the security uh in this talk. I just wanted to remind you. Okay, so let's start with the first part of the statement, which is what is a signature scheme. Uh of course we all know that, but let's look at some actual lean code for that. Okay, so the first part that a signature scheme needs is a key generation algorithm. Uh this is this algorithm. It takes as input uh let's say a seed. This is just some random coins that it will use, and it outputs a public key and a secret key. That's what we all already know, I guess.

Um the interesting part is we are now working in the random oracle model using this framework called VCIO, and for that we need to say that this algorithm is actually not a standard algorithm. It's an oracle algorithm. It can make queries to a specific oracle. We don't need to say what this oracle is or how it is implemented, but we need to say what is the interface. And this is what this hash spec thing is doing. It's essentially saying uh yeah, it's a specification of what is the interface. It takes some input, and then it's an oracle that uh results in some output. And this thing just says if I have a seed as input, then my computation is an oracle computation that has access to such an oracle with that particular interface.

Okay, and what I also want to say here is this also means that given the seed, this thing is deterministic, and all algorithms that we will see are deterministic. The only randomness that we have is actually the seed, which is the random input. Okay? Then we need a signing algorithm. Signing is uh very clear. We need a secret key. We need a message, and then we output a signature. So, here you see we output option signature. That means that signing can fail, and can output bottom. Um this is when you do grinding, this can always happen with some very small probability. And again, it's an Oracle computation.

And verification is also an Oracle computation. It takes the public key, the message, and the signature, and it outputs yes or no. Okay, accept or reject. Okay, that's uh pretty easy. So, now let's define security. I want to quickly remind what we what we aim for. Uh it's strong unforgeability. So, uh this is sort of the standard notion that that we care about. Of course, some people care about standard unforgeability, but let's aim for the strongest we can support. So, strong unforgeability. Uh in a non-lean uh picture, it looks like this. You generate a public key and a secret key. You give the public key to the adversary. The adversary makes a bunch of queries. In our case, queries to the random Oracle and signature queries.

And then it outputs a forgery, which is a message signature pair. And it wins if this is a valid message signature pair, and it is fresh. So, fresh in the sense of strong unforgeability means that the signing Oracle has never uh output this pair. In a sense that either you have a signature on a message that you have never submitted, that's fresh, or you have a signature that is different from the signature that the signing Oracle has returned. That's also fresh in this strong unforgeability sense. Okay, so far so good. I expect that uh po- most people know that definition.

Now, when we go to Lean, we need to formalize all of that. Um we need to formalize what are these Oracles. Again, what is their their API or the the interface, and what is the implementation of them. We need to formalize what is an adversary. Uh what is a forgery, what is a valid forgery. All of that we need to formalize that in Lean. And of course, what is the entire flow of the experiment? Okay, so let's start with that. Let's start with the adversary and forgery. So, forgery pretty simple, it's a message signature pair.

The adversary is again an oracle computation, right? So, let's think about it. So, our algorithms, the signing, verification, they have access to the random oracle, but our adversary has even more oracles. So, it will have the signing hash oracle, so the random oracle. It will have a signing oracle. What is a signing oracle? It takes a message and it returns a signature. That's all we need to know for now. And what we also give the adversary is this thing. This essentially says it gets some oracle with which it can flip random coins.

Because remember I said that all algorithms are by default deterministic, but we want that our statement also holds for randomized algorithms. So, one way to do that is to say it has an oracle that doesn't cost anything, but it sort of can give random coins to the adversary on demand. And again, this is just This is not saying how these oracles are implemented. This is just saying what is the interface of these oracles. And if I know that, I can define what an adversary is. It takes a public key and then based on that, it does some oracle computation with these three oracles and it outputs a forgery.

That's just syntactically what an adversary is. Okay. So, Nico, there was a question. >> Yeah, I was going to ask is the forgery you don't check that the message is valid or that the signature is valid for the message? >> No, I mean right now I'm just defining sort of the syntax of what is an adversary, okay? Not yet what is a valid forgery and all of that. We will define that. >> So, the adversary takes public key >> Yes. >> as an input. So, um >> It's not capturing cases where um you [snorts] have many public keys and you want to know the probability of it finding a forgery over all keys.

>> Yes, so this is single user security as specified on the previous slide. If you go to multi-user security, there's a trivial uh sort of union bound hybrid argument kind of thing. And this formalization that I'm talking about is just for single user security. So, maybe you can and show something for multi-user security that is tighter than the standard you know hybrid argument thing, but this is not considered here. >> Real protocols want want to use a security.

>> Yeah, I mean you get it asymptotically just with a log n bits loss essentially, but this this is about bit security of strong unforgeability for single user security. Okay, so now we know what an adversary is, what kind of object is that. Now we need to specify the security game that we have seen on the slide. And this is the lean code for it, slightly simplified. So, the first thing we do is we generate a public key. As I said, the only randomness that we will have is sampling the seed. Okay, so we generate a public key and the secret key and we then give this public key to the adversary.

And again, this adversary is an oracle computation. So far, we only said what is the interface of the oracles that it calls. Now we will actually implement these oracles. This is what this with oracles function is doing and it takes the secret key as input because for implementing the signing oracle, you need to know the secret key, right? So, think of this as being the adversary with a signing oracle that is implemented and the random oracle and the uniform sampling oracle, they actually come from the outside. So, the whole game is in in itself also an oracle computation. Okay, the only thing we implement here is the signing oracle and what we get back

Sorry, is the forgery and a log of all signing queries that the adversary have has made and their results and we check that the forgery is valid and we check that the forgery is fresh. Okay, and inside this with oracles there's a ton of ugly lean code, but believe me this is this with oracles is essentially just saying take the oracles that the game itself has and now add a signing oracle to it for which we keep track of the queries.

Okay, so now we know what the game is. We still don't know what it means that things are secure and to say what it means that things are secure, let's talk a little bit about bit security. I've heard that in a previous session where I was in the other room, you already discussed this, but I think this is one of the main things I want to maybe bring to your attention and discuss. What is our definition of bit security? And I will tell you what the definition is that we use in this formalization. I'm not saying this is the best or the good definition. I think it's a reasonable one, but there are maybe better ones.

So, very roughly bit security means you take the running time of the adversary, you divide it Sorry, you take the success probability of the adversary, you divide it by the running time and that should be at most two to the minus lambda for all adversaries. So, if we look at that in the random oracle model, we can replace running time or we can rather lower bound it by the number of queries. So, if you rewrite that, then bit security just means this. >> [clears throat] >> Okay, so let's look at this. What is this? This is the number of queries that the adversary makes or more specifically in the way we define it in this formalization, it's the number of queries to the random oracle that the entire experiment in which the adversary

runs will make. Okay, so this in particular includes the first invocation of key generation in our experiment. It includes when the adversary submits a message to be signed, the queries that the signer will make, and the queries that the adversary makes directly. Okay, and this is where I think things start to be a little bit controversial or like this is where we can discuss. Is this the right notion or should we just put only the queries that the adversary makes directly? If our key generation algorithm makes 2 to the 40 queries, let's say, or 2 to the 30, then this formalization means that there's actually no adversary where this thing is less than 2 to the 30, right? Because

already the key generation queries uh contribute to the 30. >> Yeah, have we tried asking the AI to try and write a proof where we only count the queries from the adversary? >> I have not, but I expect it's not that much different because it's just intuitively it's just an additive. >> So, why don't we just do that? >> We could. I'm just talking about the We could. Maybe we should, but that's Yeah. Um that's That's more conservative, for sure. Yeah.

>> Because we've spent so much time discussing this minute detail, we might as well just remove it if it's if the AI's can >> I'm perfectly fine with that. >> Okay. >> I just discuss what the formalization is that >> Okay, got it. >> But I'm I'm fine with it, yeah. So, uh I I just want to say again, I think it doesn't make a huge difference because it's an additive shift and not like you don't lose 40 bits or something uh because the key generation >> But I thought the reason we were doing this is because it makes the proof so much simpler. But maybe not. >> I don't have an intuition for why it should be simpler.

>> It doesn't matter. >> I think it's just a plus one plus minus one in the end. So, it's like 2 to the minus 128 plus 2 to the minus 40 or something. Very roughly. So >> So should I just clean this up, I guess? >> I guess we can, yeah. So I think for the sick dot golf, that's maybe the conclusion we should >> Mhm. >> use the the more conservative definition. But I think this is not a completely ridiculous definition. Um anyway, so now that we have that, let's go back to our lean uh code. So we had this game core, which was the the experiment specified in Lean. And if you remember, it was still relative to some oracles, namely the random oracle and the uniform sampling oracle. And now we

essentially take that and we implement the actual oracles. And for the random oracle, we count queries. Okay, and then what we get is something that doesn't have oracles anymore, but it's probabilistic. So it's a probabilistic computation that outputs two things: a boolean that says did the adversary win or did it lose? And uh a number that tells us how many queries did the adversary make. Okay. And then when when we have that, we can define the advantage. Let's just take the first thing and check whether it's true, put it inside a probability.

And then when we have that, we can implement the definition of what does it mean that we have bits of security. And this is exactly what we had on the slide. And this has hash query bound. Uh this just says whatever the random coins are, our queries are below Q. Okay? So it's not like with high probability we make at most Q queries or something like that. It means we make always at most Q queries. And um yeah, as I said, this is all the all the queries, but yeah, we can change the definition. And then when we have that, we can state our main uh theorem, 127 bits of security for Sphinx.

And uh I think I I said it in some session before, there's some intuition for why it's 127 and not 128 because essentially with every query that you make you have two two chances of breaking it. Either you find a pre-image or you find a target collision essentially. Um And then we can do the same thing for XMSS. Uh of course, you should not read that literally because this lives in the different lean code base where the definition here is slightly different because we are looking at the stateful scheme and the experiment is different, but we get a similar thing. Yes.

>> Um is the intention that this works for Is the intention that this works for signature schemes in general or restricted to signature schemes in the ROM because >> This only makes sense for the ROM. >> Yeah, because because if you have a street lock base signature scheme for example, you'd have to do a reduction >> Yeah, and the notion of bit security is only under assumptions about the bit security of the underlying hardness assumption. So, this is only for our schemes where we can have bounds that are information theoretic in the random oracle model.

>> Got it. >> And this is baked into the definition here. And um right. Okay, so towards the end let me just I think uh as I said, I'm not a lean expert, but I think what a lean talk should have is what is the trust the trust surface here. What do we trust? We trust of course that the lean we have this now formally verified. We know 127 bits of security and so on, but what do we assume here? We assume the lean lean kernel is uh is good, is free of bugs, mathlib is free of bugs. We have this a framework VC VIO that is used to model oracles like the signing oracle, the random oracle. We assume that these are

reasonably modeled like when the designers of VC VIO did their framework, they really modeled the random oracle correctly. We trust the random oracle heuristic here. Um and I want to emphasize all of this is in the ROM, not in the Q ROM. And I think when we do this, we should of course check that the axioms are reasonable, right? We don't have a a sorry there or other weird things. And then when we have that, we are happy. We have a random oracle base proof formally verified in Lean.

Okay. And I think the future directions or open questions are >> [clears throat] >> turn this into a Q ROM analysis. For that, I guess we will hope that VCVI supports Q ROM at some point. I'm not sure what the latest state is there. And yeah, this discussion around bit security, I think we we talked about it uh enough now. So, I think there should be one more slide, but no, maybe not. Anyway. Okay, that's that's it from my side, I think. If you have questions, >> [applause] >> Small comment.

When you actually do a >> Yeah, when you do a Merkle tree, you're computing two x's and you get a y. And so, for every query, you actually have two candidates for pre-image and one candidate. So, you have three targets overall. >> Why do you have two candidates? I mean, isn't the concatenation of that just one candidate? >> No, cuz when you do a pre-image, you can either have something else that matches the left half or the right half. >> Yeah, but that's what I would call a collision for the call below. >> It wouldn't be a collision.

Like, suppose I'm computing uh you know, I start from the root and I go backwards. Okay, so I I >> Yeah, but then every query that I make gives you both the left and the right child. >> No, so I'm I'm doing let's say the root. I'm I'm hashing X1 and X2 and I get the root. >> Mhm. >> And now I'm searching for a hash that matches X1. I'm trying [clears throat] to hash two things that go to X1. So, I'm like reversing the Merkle tree. >> Yeah, but that's that's the collision part of it, not >> No, there's no collision. I didn't do any collision.

>> You search for a hash that matches X1. >> No, I did a target collision. >> You did a collision for the invisible part. In honest In honest generation, you have preimages of X1. >> I'm saying something simple. After I do Q queries, okay, I have three Q targets that when I do my next query, the potential pool of targets that I'm trying to hit to create some event that is not supposed to happen is three times Q.

>> Yeah, that's >> Not two times Q. >> This also I don't think this is true because this everything is domain separated. I cannot attack everything at once. >> If everything is domain separated, then >> think this is quite important here that everything is domain separated. >> This is why Zcash uses domain separation per level. >> I mean, yeah, I mean this is also in these schemes I can in this in the Sphinx standard this also domain separated in XMSS. Yeah but Emil claims that this is actually 127.something bits of security. Yeah, because the two things are actually not 100% independent random events right?

>> If you're domain separated, then why do you then >> If I If I submit a query, then I have two chances. Either that query the the input to that query is the thing that also the honest signer has input, right? That's 2 to the 1 minus 128. Or it's a different thing and the output of it collides with what the signer has got as his output. This is different source of randomness. It's the output of the random oracle, and it's also one two to the minus 128. So, that's the intuition for for why there are two sort of this somewhat independent. It's not fully independent. That's why I think it's 127 plus epsilon. Uh but, uh that's the intuition I have at least for why

it's minus one bit. >> Okay. >> And the the thing is [clears throat] all analysis that we know that are written uh in a paper, they make abstractions, so they are three to four, and they make, you know, reduce to properties, and they have uh a few bits more of security loss, the tightest ones we know. Whereas, this is a monolithic kind of random oracle. Uh and if you see the history of of commits that Emil had in the in the pull request, it's like the AI managed to prove 124 or something, and then it slowly increased to the the target to 127.

>> We We had the same experience with that. It's actually much easier to get very tight security proofs by AI. Um it's hard [clears throat] to keep going until it loses uh that last one bit or whatever. >> Uh I also want to highlight here is that probably that after we find the scheme that we like who is signed a goal for with any other way, I think it still makes sense to then uh sit down and do a reduction to certain properties.

Most likely, this will not give you 127 bits of security, but uh it um achieves several valuable points. Uh one of which is that now we actually see what we want from the hash function. And um this can be really important, and this was, for example, even in the history of SLH-DSA, this was a useful case. Uh during the competition, we had the proof required properties and stuff. And then there was a person on the PQC forum that saw that for SHA-256 category three, certain property doesn't achieve the required security level.

This was enough to boost the parameters. And then the attack on the scheme using that uh the um property breakage showed that actually you can use uh that attack on the property to attack the scheme itself. And if the first person maybe didn't notice this attack on the property, maybe then the second person would not find the attack on the scheme. Uh, so this is one thing. Uh, yes. And uh another thing is again, when we talk about for example, uh I have now slightly improved uh reduction to properties. This gives

you 122 or 21 bits of security. Is the seven-bit security sounds fine? For me personally, it does because again, A, this is a reduction loss that here and there we have different properties, we sum them together and stuff like this. Second thing is again, here we count these hash queries as uh just one query and this is the price, but actually computation of the hash function cost something, storage in the memory cost something, some other work memory and stuff and stuff also uh give you something. And so besides having a fully ROM analysis, I think it would be also make sense to then do uh the

reduction to the properties. And yeah, and the QROM part is also in lean. I don't know how it is feasible at the moment, but we can do pen and paper. >> I think reduction a reduction to properties also gives you some intuition about why is the scheme secure, whereas this sort of monolithically improved that no one will read it. Just tells you, okay, this is secure, but not why. >> I I definitely prefer doing the reductions.

You can easily do reductions in the other direction. >> But you need to define the properties, or you let the submission to define the properties. And then if you let Collision resistance will not give you a super tight. You will have to increase the output sizes. So we have uh in the SLHDSA or in any fancy construction, we have much more properties that are not that widely used. Are they?

But maybe a new scheme will require a new property that it is not there yet. And so I I think if you require a reduction to properties, I would say you would probably should you should allow also to define the property. But if you allow to define the property, you also need to check whether it is nonsense property or it makes sense. >> Or it's just the property is the scheme is secure, right? So I think for an auto research challenge it's very good that we have something that doesn't rely on hardness assumptions.

>> Yeah. >> And that is just pure information theoretic in the realm. But then when we later pick something and want to understand it, then it's very good that we have reductions to simpler properties of the hash function. >> But it also means that you can't use lots of space schemes. >> Yeah. >> I think it will need something like that. >> I have a different question. >> Yeah. >> Um I I I had a look at the formalization for Sig Golf and there's some it's a little bit more complicated than in the presentation because there's also a cache and a witness and there's an expand stage. Can you elaborate on this a little bit? Like what is this in practice?

>> I think I would have to open up the definition but is I I don't know what the definition from the top of my head. I just know that I checked that it kind of makes sense. Uh, but the yeah, maybe someone more involved in Sig dot Golf can explain or write it down. I don't know. >> Yeah, I I can explain briefly. So basically um in some sense there's two types of signatures that we care about. There's the really compressed signature that we send over the wire and then there's the one that we feed as a witness to the ZKVM.

Now, one very example of a difference between the two is Merkle path pruning. So, you want to prune as much as possible before you send it over the wire. But then, when you send it as a witness to your ZKVM, you kind of want to do some of the work to unfurl it and and and and precompute the the the the bigger version. And another thing [clears throat] that you can do is send some non-deterministic hints to your ZKVM, for example, in the encoding stage or in other stages. So, what the expand program does is that it takes the ultra-compressed uh, signature, which is what we're trying to optimize in the metric, and then kind of blow it up so that the verification is actually cheaper in the

ZKVM. And, um, one of the interesting things here is that the strong unforgeability is only for the compressed signature. When you decompress it, if there's like multiple different hints that make the verifier pass, it doesn't really matter. >> So, is the goal about the The proof systems you choose will also I think it's what Uh you need to press underneath. >> Is the goal that the um proof systems you're using will also be uh information theoretically secure in the QROM?

So that everything composes. Um because if you're using >> Strictly speaking, nothing composes here. Because I mean, it's the same as in the recursion session. Like if you prove this thing in the ROM >> Mhm. >> and you let's say you only had this proof and no standard model proof whatsoever, then you had the same issue as when you do recursion. You have the relativized argument issue all over again, right? >> Well, this is the thing that >> for these schemes, we have standard model proofs. Maybe they are less tight. Whatever, but structurally, these standard model proofs show that even if you instantiate the hash function, there's still a reasonable argument to >> So So >> Which is different from

>> The The BCS 24 impossibility result about recursion aside, um if you use um uh computable efficient computable reductions as your um your target for what you're proving, then they compose because um >> Yeah, but this isn't This wasn't a ROM, not under reductions. >> You You can Okay, so you can do reductions in the ROM. >> Yeah, but they then they it doesn't compose. If you're speaking >> No, no. >> It does. >> It You need a relativized argument for that. This is exactly the the problem with recursion, and if you only have a proof in the ROM, that's kind of then you run into the same territory as when you do recursion.

So we need to do some heuristics to argue security. Whereas if you have a standard model proof plus a ROM proof, you have the best of both worlds, right? The ROM proof gives you good parameters. The standard model proofs gives you reassurance that we what we are doing here is actually backed up by reasonable assumptions about the hash function and not just by something that you know, works only in the ROM. >> So, so if you use the same idealized model for all of your proofs, then they compose.

>> No. If you prove stuff about the random oracle, it doesn't compose. That's exactly the point of the relativized arguments. That's exactly why recursion in the in the random oracle model why you cannot analyze that. Why we had to go to some, you know, standard model notion of knowledge soundness. If I prove something >> Okay, so if I have scheme A that uses scheme B um and I have a reduction um from a break of scheme B um to say a discrete log solution or whatever um in the ROM.

Okay? Um then uh I can compose that with a proof a reduction for the rest of scheme A. >> It depends on what you mean by compose. If you just run them next to each other, yes. But if one proves knowledge of the other, then this one uses makes non-black >> about proofs of knowledge. I'm talking just scheme A uses scheme B. >> Yeah, that works. >> if I have a break of >> That works, but your question was about a proof system that aggregates, for example, these signatures. And then you make non-black box use of the signature verifier.

>> Yes, the problem is the long non-black box use there. >> Yeah, exactly. And then when the signature verifier >> compose? >> Yeah, black box it does, but that's not what the SNARK aggregation will do. The SNARK aggregation will be very, very non-black box. It's >> Yeah, the the point is you you have many schemes that are working together to um for your overall protocol um where you are using black black box. They are making black box use of each other. Um and so you need to be able to compose the reductions um just outside the use of recursive proofs. They >> I mean that that works. As long as you properly domain separate stuff, it works for sure.

But in our setting we consider non-black box [snorts] composition. >> Okay. But the the thing is the the style of proof that you just did, where you're just proving the um advantage um uh in information theoretically pseudo random model that doesn't really compose in the same way because >> That's true. So uh that's why if you implement this, you should domain separate more. More than the proof requires. >> Or you could just use the computable reduction style throughout, which is what we can do if we are using the same >> context in which you apply it, right?

>> It It just works. Honestly, try it. >> I I don't know what your claim is. >> Okay, I I will um I will explain later offline because we're you we're going in circles. >> Amazing. Thank you, Darrel. Um Benedict, thank you so much for this fantastic presentation. >> [applause]