Defensive Acceleration

Transcript

Welcome everyone to the second edition of the CAMBRIDGE POST-QUANTUM WORKSHOP. >> [applause] >> I AM SO INCREDIBLY excited to see this room brimming with talent. Like it's packed full of talent, packed full of uh, you know, familiar faces and new faces. And I really look forward to the next three days. Should be lots and lots of fun. I want to give a special thanks to many of you, most of you who are participating as speakers and moderators. This is going to be an event an attendee-led event, and there's going to be an opportunity for everyone to participate in the workshops uh, with

all of the whiteboards uh, that we have. And I want to give also a special shout-out to Will and Enikő who have been working tirelessly to uh, you know, make sure that all of the logistics are going to be running very smoothly. So, thanks again TO EVERYONE CONTRIBUTING. >> [applause] >> NOW, MANY OF YOU HAVE FLOWN A VERY long distance from countries all around the world, and we wanted to give you a taste of the Cambridge experience. So, about half of the room is staying in rooms provided by Jesus College. These are not dorm rooms. I'm told they're like luxury hotel rooms.

Um, and we're also going to have two fantastic dinners. We're going to have an an opening dinner at Westminster College, uh, and we're going to have a closing dinner at Murray Edwards. And this closing dinner is going to intersect with the second batch of people who are coming for the second batch of three-day workshops. So, we're going to have 120 crypto nerds all in one room for this dinner, which should be a lot of fun. Now, uh, the agenda is available publicly. If you go go pq.ethereum.org, there's a button for the for Cambridge or you can just go {slash} Cambridge.

And really what I want to highlight is that we have um two rooms each with a different theme every single day. So, we're going to have six different themes. And uh today's themes are performance in this room, the Alena Hall, and we also have privacy as a theme in the Sybilla room. Now, in addition to all of the talks that are going to be recorded and put on YouTube, you know, we're talking about uh you know close to 50 hours of content. Where we have uh workshops. So, um we're going to have four workshops per day. These are an hour and a half each, and this is really where the magic happens. At least this is where a lot of the magic happened last year, and we're

trying to duplicate that again this year. It's this in-person emergent behavior where, you know the new ideas and the new collaborations uh start. Now, one of the things that I want to talk about next is defensive acceleration. And this is somewhat a a reflection of my personal philosophy uh from the last few, you know, months. What I've uh observed is that the frontier is accelerating at a breakneck pace, and it's is really dizzying. And what should I do as an individual, you know, to make a contribution uh to to to to society? And my personal answer has been to focus on

a very small sliver of the frontier. Um so, my observation is that almost all of society that is accelerating the frontier is trying to enable new things. So, we have AI, we have robotics, we have quantum, we have bio. These are all amazingly powerful technologies that will create new good things. And there's like a very small sliver of the frontier which almost no one is looking into. Almost no one is investing into it. Highly under represented from a head count perspective and that is the part of the frontier that is focused on making sure on preventing that no bad things happen.

And I think this is what gives me a lot of motivation every day to you know to try and and make sure that as a society we have the infrastructure that we need to to to defend ourselves. I think a lot of the people here you know represent a very big subset of this defensive frontier. So what I'd like to talk about is some of the acceleration that we're starting to see and the timelines and the road maps and then I want to start talking about the solutions that we can start implementing. And the two big ingredients that I'm going to talk about are formal verification and hash based cryptography.

So this is uh breaking news in some sense but the the Ethereum Foundation has updated the straw map to bring forward um the uh the advent of of post quantum security for L1. So it used to be in the L star fork. Now we've shifted this by one hard fork uh to to to K star. And upgrading Ethereum L1 to post quantum security is going to be a journey because there's a lot of work to do at all layers of the stack from the consensus layer to the execution layer through the the data layer as well. So at the execution layer we have something called Lean Sphinx. This is our stateless signature scheme that users

would be um uh making use of for uh for their transactions. At the consensus layer we would have Linux MSS which are stateful signatures for the validators and then in the middle we'd have Lean DA which is a post quantum solution for data availability sampling. Now, powering all of these solutions is our engine, Lean VM, that is doing most of the the heavy lifting cryptographically speaking. So, let's say a a a fully fledged ZK VM um that is doing this the signature aggregation at the EL and at the DL, and is also so the CL and EL and is also producing the data availability sampling

proofs for for the DL. Now, in addition to Ethereum roadmaps accelerating, the quantum roadmaps are also accelerating. Um I was talking to Connor this morning. There's like new error correction codes that are invented every week. There's new decoding algorithms, breakthroughs happening every every week now. Um and there's also breakthroughs at in the high-level algorithms, specifically Shor's algorithm, which is relevant for us. So, uh back in March, Google had this paper which brought the latency of Shor down to 10 minutes and made it very relevant for Bitcoin and the Bitcoin mempool.

This was brought down to 3.5 minutes of latency with a a really fun auto research project called ECDSA.fail, the very first open auto research project. And this latency is going down. Okay? There's going to be more breakthroughs that brings this down to a matter of of seconds. And that means that the Ethereum mempool itself will not be a place to protect um vulnerable uh transactions. Now, last year we had Steve Brierley, um the founder uh of a of a local Cambridge uh quantum company called Riverlane. You know, they have uh over 100 employees. He gave a fantastic talk,

and he's going to be giving the keynote dinner talk uh later today. And last year he made some really bold claims. He said that Q day is going to happen between 2030 and 2032. And really the room was shocked back then because the mental model that we had a year ago was that Q day was around 2035. But nowadays it's kind of taken for granted that yes, the timelines have moved forward and 2030 to 2032 is indeed correct. So he was uh he front-run that that trend. And the other prediction that he made is that um keys would get broken in seconds. And here you are, you know, in a matter of just 1 year he has been vindicated with

this particular uh amazing prediction at the time. Now, within the Ethereum Foundation I would now argue that post-quantum security has become the number one priority. It started off as priority maybe number eight. And then it gradually became more and more and more important to the point that now it is arguably the number one priority. And I think the some of the people that we have here, including top brass from the Ethereum Foundation, we have the executive director, we have the three um uh leads of the the the protocol cluster. This is a reflection of how important the topic is for us. And part of the reason why it's so important

right now is because we don't have much time. By the next workshop in 1 year's time, in 12 months, we're going to need all of the signatures to be production-ready. We're going to need Lean VM to be production-ready. And the reason is that they would be launching um on mainnet in early 2028. And for the signature schemes in particular, once we've launched them, there's no going back. Um the most likely they will be extremely sticky and the designs that we launch with will uh will persist for for for many years to come.

But possibly possibly decades or centuries. On the other hand, LinVM, it's okay if it's not perfect because it's infrastructure that's hidden behind the scenes that we can upgrade at every hard fork. Okay. Now, I'd like to talk a little bit about AI timelines and this has been you know a topic that has developed over the last few days and and weeks. So, just a few days ago we had OpenAI, I think, really show conclusively that mathematical superintelligence is here.

They dropped hundreds of of mathematical results and there's this guy called Lex Fridman who maintains a website that keeps track of the top 500 open mathematical problems, at least according to his methodology. And 90 of those 500 top mathematical problems were solved in one fell swoop. And when you start looking at the details, it starts becoming even more amazing. So, it took an average of 3 hours per problem that was solved and it took just one single prompt to to one single agent to solve to get the the the the vast majority of the results. And on

top of all of these mind-blowing details, some of the results that were found went directly in opposition of human intuition. Things that no human mathematician would have predicted actually were were were were proven. Now, I think we should ask ourselves if we have reached mathematical superintelligence, have we also reached cryptanalysis superintelligence? And we do have people out there that are starting to you know put clarify that yes, this is something that we should expect. So, we have Scott Aaronson who very recently in a blog post made it clear that AI companies

have started trying to see if AIs can break our cryptography. And they're doing so gingerly and discreetly, I stealthily. And that makes sense, right? Because this is a matter of national security and agencies like the NSA will be, you know, breathing down the necks of these uh AI labs. And then we have top mathematicians like Peter Scholze, possibly one of the greatest living mathematicians, an absolute genius who had the Fields Medal at the age of 30. What he says is what is worrying me the most at the moment is actually the insecurity of cryptography. What is worrying me the

most? His number one worry is the insecurity of cryptography. He says, "Finding algorithms breaking standard cryptographic assumptions uh cryptographic protocols is a number theory problem whose difficulty does, to my non-expert eyes, not significantly exceed what these systems are now capable of." Now, what we're starting to see is a few droplets of blood uh in the world of cryptanalysis. There's like some schemes out there, so SIKE, I so gently base, Hawk, lattice-based, McEliece code-based. And then this new result from literally just a few hours ago that provides a sub-exponential attack on the on on on on on lattice-based schemes such as ML-DSA,

and all sorts of other things that haven't been published just because, you know, academics are still writing down the results or because of censorship from um for reasons of national security. And so historically, what we've had is that the Overton window of focus has been on this quantum risk. And now I've basically updated my mental model for crypto for cryptographic risk. I now think of it as a as a bimodal risk distribution. So, in addition to the quantum risk, there's a smaller risk, the AI risk here.

And the reason why it's smaller is that there's there's a possibility that classical computers just fundamentally can't break some of our hardest cryptographic problems. But, this is a a non-zero bump, and the important thing is that this bump happens before the quantum risk. Okay, so from the timeline's perspective, we already have mathematical superintelligence, and that would be the thing that would lead to the emergence of this of this new bump. So, what I think we should be doing is expanding the Overton window, and just a few days ago, the window was kind of shut open with this tweet that I put out which you know, was essentially a bomb

that was dropped in the community and led to a lot of discussion, and I'm sure we will discuss it later in this in this workshop. And maybe all of this acceleration is going to lead to the firm roadmap accelerating even further. Maybe we should get everything done in a matter of two forks, and this is something that Kev has been advocating for, and something that is starting to seem more and more reasonable. Okay, so we have this incredible acceleration. What are some of the tools that would allow us to constructively respond to those emerging threats? Well, one of them is formal verification.

We're going to talk in great depth about formal verification in this workshop. We're going to have five different talks which has lean four in in in the title. And really, the way that I think about it is that Lean 4 is the new rust. It's a new level of abstraction. So we used to write code with in your low-level, you know, byte code and then we move to so-called high-level languages like rust and now we're moving to ultra high-level languages like like Lean 4. And you know, it's in the in a few in a few months it's going to look like you know like archaic to be writing rust manually.

So one of the reasons why Lean 4 is so powerful is this idea of minimizing the trusted code base. So on the bottom here we have the trusted code base in red. On the top we have the untrusted code. And really what you have to worry about as someone who's writing in Lean 4 is properly describing the goal that you're trying to achieve. What is the security property that you're trying to achieve? So in the case of a signature schemes you want to describe what does it mean to have 128 bits of security in the random oracle model. And this is an exercise that we have gone through at the Firm Foundation and the the results are really shocking. It takes only 100

lines of Lean 4 code to very precisely describe in excruciating detail what it means to be a signature scheme with 128 bits of security in the random oracle model. And that's the the main thing that you have to write and read and audit and understand in great depth. Everything else you don't have to worry as much. So technically speaking there's two other parts of the trusted code base. There's the kernel. Um that's not something that you have to write and you know, most people are not going to to be worried about reading it either. This is more of a of a public good if you will and there's a whole discussion that we can have about the kernel.

And then there's the the semantics of the ISA in which you're going to be implementing things. So, this might be a virtual ISA like RISC-V in the context of ZK-VMs, or it could be like actual hardware ISAs like ARM and and x86. And then everything else is untrusted and done by the AIs. So, once you have the the goal, the AI can go design a security a signature scheme like Lin Spanks, which has the property that you want. It can prove that it has 128 bits of of security in the random oracle model. And then not only that, it can actually implement it in bytecode and prove that the bytecode is correct. And this is exactly what we're doing with with Sig

Golf and have been extremely successful at. And this I guess is a good a good segue to the second superpower of formal verification and ultra-high-level programming languages, which is auto research. Now, we can have constraints that mean that the AI can't can't do bad things. Like, all of any input from the AI is is is thoroughly checked and must be must be provable. And we we already have three auto research challenges that have led to, mind-blowing optimizations that humans arguably would have never been able to find themselves.

And one of the most exciting auto research that I'm looking forward to is recursion.fast. Because this is the moment where AIs design proof systems. And in some sense, you know, try and do the work that many of you in this room, top cryptographers, have been have been doing for for for a very long time. So, instead of having humans design polynomial commitment schemes like like FRI and and and wear and you know, you just let the AI loose and have it design its own proof system.

And in the context of this workshop, the Ethereum Foundation organized 20 in the max licenses. So, we have 10 cloud licenses, we have 10 codex licenses. And I'm hoping during the workshop, not only do you do whiteboarding, but you do a little bit of prompting on the side, and that we see in real time the frontier advance while we're while we're progressing during this workshop. And you know, auto research is going to be really big part. We're going to have nine different talks and and workshops on on auto research.

Okay, so that's formal verification. An incredibly powerful that went from in some sense really impractical and and sci-fi to extremely practical and and and and commoditized in a matter of a few months. Now, the final thing that I want to touch upon is is hash-based crypto. So, what we're trying to achieve here with Ethereum is to have all of Ethereum L1 built with just what one hash function. And one observation is that we need hash functions everywhere in blockchains. Right, we need it in a single transaction hash and sign. We need it when you form a block of transactions to build the blockchain.

We need it when you execute transactions with the state tree. It's just the a sunk cost. If we if hash functions break, then you know, we're we're really utterly cooked. Um but the the exercise here is how much can we squeeze from this one hash function? And the answer is everything. And then the question becomes which hash function to use? And here we have a really exciting initiative called hash smash that uh Zuko will be talking about uh later today. >> [clears throat] >> Now, this is a little screenshot from the the the Lean VM readme, and it kind of gives you a flavor of the level of security that we're trying to achieve.

So, we want 128 bits of soundness in the random oracle model. We don't want any proximity gap conjectures. We want end-to-end formal verification, and also we want a traditional hash function like one in the SHA or in the Blake families. Now, there are a few caveats that we're still working on, and this is very much a topic of the workshop. So, we need to put more work to understand Fiat-Shamir and recursion heuristics. And there's also like a little detail, which is that we might target 127 bits instead of 128 bits, but again, that's a detail.

And that's like some of the work that that we need to figure out. Now, one amazing development of the last few months when it comes to SNARKs is binary fields. Okay, we've had pioneers who are here in the room, Jim and Ben, who really opened the Overton window with with binary fields. But in the last few months, we have had the stars align in an incredible way, something that I think no one would have expected. So, star number one is Nvidia. Nvidia exposed a new instruction as part of CUDA 13.3, and we're going to have Jean-Luc

talk about this later today. And this instruction allowed for extremely fast proving on Nvidia GPUs, which is something that we need. The second amazing breakthrough is Flock. And we're you know, we're really privileged to have Ron in the room who can who can talk about it. And really what Flock did is that it allows us to move away from Poseidon and embrace these these much more traditional hash functions in the SHA, in the Blake, and and SHA uh families.

And then finally there's been another breakthrough literally in the last few weeks uh Beats uh and we're going to have uh Albert and Remco talk about it uh very very shortly uh today. And this this this work resolved the the final open research problem for binary fields, which is how do you do fast integer multiplications on on binary field. And when it comes to to performance, we're talking about 1 million hashes per second with Flock proven on a laptop CPU, which is amazing. And we're talking about 10 million multiplications proven per second over 10 million proven per second uh on a laptop CPU thanks to to

Beats. And then out of nowhere, just literally a few hours ago, >> [laughter] >> um we have um Sreenath that came up with Magnetar. It's an insane story. One guy, Sreenath, wrote an entire RISC-V ZKVM. And he came up with all sorts of new ideas for binary fields that are complementary to Flock and BitZ. And he he has performance that allows us to reach 10 MHz on a laptop CPU. So you can prove the execution of RISC-V at the rate of 10 million cycles per second, which is absolutely insane. And we're

going to have Sreenath talk about this later today as well. Now this is my final slide. And really this is an invitation to really push the frontier and open your mind. There was a bunch of preconceptions when it comes to hash functions. Things that people were just saying and saying and repeating mindlessly. Things like threshold signing is impossible with hash functions. Things like hardware signing is impractical. It's just too slow on the Ledger Nano S.

Things like hash functions um can't do encryption. Well, it turns out that we have all sorts of ideas that refute these preconceptions. And these are ideas that we're going to talk about in this workshop. So, now we can do threshold signing in under 1 second. We can do hardware signing on a Ledger Nano S Plus in under 1 second. And there's even some ideas to do ephemeral encryption, which is what we need for ephemeral one only using hashes. So, if you have an encrypted mem pool, for example, you only need encryption for a few seconds.

And that's the kind of thing that it turns out we can do with hash functions. So, with that, I'd like to say thank you and open it up for discussion. >> [applause] >> So, you had the nice diagram with the the trusted base and everything above the line in green. Um So, is it required, do you think, to um also get the AI to produce human understandable documentation of

everything it's doing, including the stuff in the green section? >> Yeah, great question. So, uh in terms of of readability, um right now AI is kind of stuck. Um but I I am I am hopeful. One of the reasons is that we can give them we can give them a goal, which is very measurable, which is come up with the shortest proof possible. Uh and you know, there's um there's this this this book called uh uh proofs proofs on the book or something, where you You you you the the goal is to try and find the shortest and cleanest proof for for for every result.

And I think I'm hopeful at least that AI's will be able to to to do auto research on simplicity and and and readability. Right now, what we're starting to see is that proofs are monstrous, like hundreds of thousands of of of lean proof code. Um and you know, one I think acceptable philosophy is just to be zen about it and say, you know, so long as you you you trust the kernel and you trust the property then you shouldn't have to read it. But I think um the blockchain space has such uh of of an emphasis on security that you know, we owe it upon ourselves to at the very least understand the proofs um and and and and have them be

digestible. But the way the way that I think about it is that there's a there's a hierarchy of of human readability. So, at the very very top you have the the the property here. This this needs to be like totally transparent and and and human readable. Um and then, you know, you have the bytecode. So, you have the the scheme that you that you develop that, you know, needs to be reasonably simple. It's something that you can you can draw a diagram on the whiteboard. Maybe in the case for example of lean Sphinx is just a just a a dag basically.

And then the the bytecode is something that is next level in the hierarchy. Like today, no one reads bytecode that comes out of a compiler, right? You just you just read the high-level code. And then somewhere somewhere in between the bytecode and the scheme lies the the the the mathematical proof of of soundness. Um and I think it's it's okay to to relax the the requirements from a readability standpoint, but still important to to have some some readability. >> Yeah, I I found that um the comments are often not in sync with the code. So, you you can tell it to produce um good comments and uh

uh a high-level design document, and then there is nothing that is completely tractable tying that to the actual leak of um And so, you you have to explicitly uh um ask the AI to to keep that back back. They can find a bunch of bugs, but how do you know that that goes away? >> [snorts] >> Right. So um earlier this year, there was a soundness bug in uh Lin uh kernel.

Uh more than one. Uh can you give us a bit of history of this? And if we can actually um solve them from good, because otherwise we're just moving uh the trust assumption to the kernel, and we might have false proof generated. >> Yeah. I mean, actually you have the person right next to you who can answer that question. >> Yes, there is there was a formal one sound about it in the kernel. Um there is soundness bug. Is that all? >> Uh you need to be closer.

>> Oh, that's good. >> Yeah. >> Check check. Oh yeah, this is better. Uh okay, so with soundness bug, so um the kernel, I guess for background, is the amount of code that is fully trusted, because that is what checks the proofs in any proof assistant. Uh the complexity of the kernel depends on >> the underlying type theory for example. And designers which is the people who can decide how much they want to put in the kernel and how much they part of the hours proving promising uh without adding it to the kernel.

Um every proof assistant has a couple of bugs as far as I know, and they need to get them fixed. Fixing them is quite good, which is what we intend to do. Uh the reference manual that is used in this talk for Lean, for example, is about 2,000 2,000 lines of fast C++ code. So, there's not a lot of code, but it's very complex code. And the other like proof series is also very complex because it's a very type dependent language. Um when there are bugs in the kernel, the main thing is that if you show it false, um the kernel will accept it, and that's that. The moral of the story is you know, kind of similar to having sound logic in a proof.

Um where there are bugs, there's also due to the fact that Lean was leading particular, it's a heavily extendable language um for, you know, fairly historical reasons, which is that Thierry De Moura did not want to deal with too many feature requests, and said just do it yourself. Uh this is very helpful, but it means that obviously if you have a kernel that has to accept proofs that come from a high-level language that is very easily extendable, then, you know, there are more things that can go wrong. Um what can be done to make the kernel far more trustworthy is obviously formalizing more of the kernel and the underlying type theory of Lean and the implementations of type theory in the kernel over time.

There was a PhD thesis um and a master's thesis on kind of, you know, Lean for Lean, which is this implementation of the kernel itself in Lean, and which has progressively, you know, has been progressing in formalizing different aspects of the kernel and Lean's type theory. That is not yet complete. Um that is ongoing work. There are things like the inductive types, uh which are very tricky to formalize, which haven't been formalized, I think, you know, essentially for any other kernel either. Um I do believe we will eventually have a kernel that is fully formalized and better understood, and that Lean's type theory will be better understood.

But, it's I guess important to know that this is essentially open type theory research, and not just a matter of engineering or being lazy, but, you know, there are actual problems to solve and understand better. Um and uh and yeah, this doesn't mean that I think there's a huge chance that things break. For example, I mean, I maintain Alcubierre. This has about 300,000 lines of code. I would be extremely confident that we don't have any kernel bugs that we're not aware of, and I would bet, you know, whatever money I have on this. Um if someone wants to disprove this in the week, you know, during [laughter] the weekend, feel free. Um >> No, I'm going to tell you it's not a problem. Um it's not a problem for um non-adversarial um formalizations.

>> Yeah. >> Um It would This Yeah. Um these really are corner cases, and you're not going to hit them. If your goal is um you're designing a complicated thing, you want to make sure that you haven't made a mistake. Um uh unless you're literally just telling an AI to um to produce um a proof, no matter what, which obviously you should not do, because you should see my previous question. Um >> Right.

>> if we're doing things that produce human-understandable proofs, then they will not exploit um bugs in the Lean 4 kernel. I I I would be extremely surprised if that happened. >> Uh yeah, but I think it's also, like, you can take measures to also reduce the likelihood of bugs. Uh for what it's worth, actually, I do think that, like, we've seen a lot of issues with the inductive types in the kernel. I do know for a fact that it is possible to reconstruct inductive types without having them in the kernel. And maybe, you know, one thing to pitch to the Lean 4 is to, like, put in with AI the hard work that is maybe now less hard to remove parts of the kernel and move them out of the kernel. That would be a good idea.

>> Yeah. >> And inductive types outside of the kernel was done for Martin-Löf type theory in the '80s or something. So, it's it's doable, just extremely laborious. >> [clears throat] >> Completely opposite question question on the opposite side, let's say, not not lean verification. You mentioned hash-based signature on the ledger in less than 1 second. What kind of signature is cuz the last numbers I had in mind was like SPHINCS plus, you know, uh essentially the standard.

Uh so, so what kind of hash functions are there and which workshops are are these to be going to be discussed? >> Yeah, yeah. So, we'll discuss this. Uh amazingly, some variants of SPHINCS+ can be signed in 1 second, but we have We have a meal who raised his hand. Do you want to answer the the question? >> You can just take your SPHINCS to say that has 2 to the 24 lifetime on this. And you replace H from 22 to 26, K from 6 to 24, A from 24 to 10, and you get 2 second signing on the ledger on SPHINCS+.

So, essentially, I simply modifying a little bit the parameters of the SPHINCS, like not the SLH-DSA. It's the new the new candidate that is only one layer that has like one tree that has 2 to the 24 lifetime. You make it You make the force a little bit bigger below to make them easier to sign, and it works on the ledger. Like key gen 1 minute, signing 1 second. >> Okay, which workshop going to be that? >> Sorry? >> In which workshop you going to present that?

>> Tomorrow. So, we have a whole company, Riva, that got acquired by Project 11. They came up with these amazing tricks. You know, they have pre-computation tricks, grinding tricks, they do all sorts of hinting and assistance. We will be discussing this uh tomorrow, I believe. >> Thanks. >> Yeah. And you know, I didn't want to put, you know, the the the pic- the pictures of people and and and whatnot, but the the people saying these things were like experts in their in their in their domains. So, threshold signing was is impossible. That came That quote came from the founder of an MPC company.

Hardware signing is impossible came from the CTO of a hardware signing company. And encryption is impossible came from one of the, you know, world's most famous, you know, cryptographers. So, don't always trust the experts, kind of. There are ways to be creative and and go around things. >> I always knew they were wrong. >> Okay, good. >> Uh by encryption, you probably mean key agreement here, right? >> Yeah, public key encryption, yeah. Yeah. Connor?

>> You mentioned 127 bits in the Is there a bit more information there? >> Yeah, so Emil can can uh and Bendik can talk about this, but uh basically, it turns out that um because we're dealing with uh hash digests that are 128 bits, um there's a little bit of a rounding error where So, there's a there's a very small attack that that takes 0. >> out of the 128. So, we can prove 127.3. >> Um and the the the solution to get 128 bits would be to go to the next level of digest size, uh which, you know, would be just extremely expensive for 0.7 uh bits of additional security.

>> Great, thanks. >> It would be like a very small difference there or if you can confirm that the lean XMSS does not completely comply with the SLH DSA standard because with the full compliance with the SLH DSA standard you only reach 126.83 I think. At least that's what I have. >> We have lots of raised hands Emil and then >> [laughter] >> Okay, so I think there's an intuitive reason why it's 127 and not 128. So let's say you make a hash query as an adversary then you have two kind of distinct and independent chances of

winning. Either the input that you provide to that to that hash query hits something that the honest signer used during key generation or the output of your hash query which is a completely different source of randomness uh collides with what the signer had. So that's the intuition for why there's sort of two chances per query which gives you roughly one bit. So that's the first thing I want to say and the second is it all depends on your definition of bit security and it's kind of a little bit unclear and we will talk about this in in the session about lean XMSS and lean spinks in in lean about this definition of bit security.

So uh the 127 is for a certain definition we have a proof in lean um but it's a little bit debatable. We can talk about that in the session. >> So so can you redefine it to get back 128? >> [laughter] >> In a natural way I mean. >> Relatively natural. >> Sure, just plus one. >> [laughter] >> There there is a 0.7. >> There is a reason why the caches um target security level is 125 bits.

>> Oh, interesting. >> Yeah. It's it's similar. It's not exactly the same problem but it yeah. >> It's also if you the 127, we have a proof for that in Lean, but in the in the random oracle model, all the proofs that are written in papers uh that are meant to be understandable for humans are less tight. So, there's an additional security loss that comes from doing abstractions and reducing it to concrete properties of hash functions, which I think is a good practice, and then you get even less. You don't get 127, you get I don't know, 120 or something.

Even for the standardized parameters. >> Okay.