-
atomfried[m]would it be possible to write the security proofs in an interactive theorem prover (coq) which then would make the proofs much easier to check?
-
atomfried[m]has anyone done such a thing for security proofs before?
-
Rucknium[m]atomfried: That's kind of what I suggested here, but kayabaNerve said "No..." :P
-
Rucknium[m]
-
atomfried[m]haha, havent seen that, thanks
-
Rucknium[m]We potentially have a lot o security proofs ahead of us: Seraphis, Curve Trees, Bulletproofs++. It's a bottleneck for sure.
-
monerobull[m]kayabanerve: would FMPs reduce the needed data to sign transactions? since you dont have to reference outputs?
-
monerobull[m]its one of the problems for stuff like the foundation passport regarding monero
-
kayabanerve[m]Rucknium @rucknium:monero.social: I don't remember that being a topic of discussion. I'm unsure how valid the usage of Coq would be, and I'd imagine it varies among sections.
-
kayabanerve[m]monerobull: It still needs the tree path, even if it doesn't need decoys.
-
kayabanerve[m]eprint.iacr.org/2023/1071 New paper on security of SNARK protocola
-
Rucknium[m]I don't know what you mean. You said "don't contact Bailey" later in the log: libera.monerologs.net/monero-research-lab/20230607#c253852
-
kayabanerve[m]That wasn't about Coq yet about reaching out without proper scoping/justification.