12:33:48 <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?
12:33:49 <atomfried[m]> has anyone done such a thing for security proofs before?
13:20:41 <Rucknium[m]> atomfried: That's kind of what I suggested here, but kayabaNerve said "No..." :P
13:20:41 <Rucknium[m]> https://libera.monerologs.net/monero-research-lab/20230607#c253530
13:26:01 <atomfried[m]> haha, havent seen that, thanks
13:32:09 <Rucknium[m]> We potentially have a lot o security proofs ahead of us: Seraphis, Curve Trees, Bulletproofs++. It's a bottleneck for sure.
13:57:37 <monerobull[m]> kayabanerve: would FMPs reduce the needed data to sign transactions? since you dont have to reference outputs?
13:59:09 <monerobull[m]> its one of the problems for stuff like the foundation passport regarding monero
14:57:32 <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.
14:57:56 <kayabanerve[m]> monerobull: It still needs the tree path, even if it doesn't need decoys.
15:07:33 <kayabanerve[m]> https://eprint.iacr.org/2023/1071 New paper on security of SNARK protocola
16:48:52 <Rucknium[m]> I don't know what you mean. You said "don't contact Bailey" later in the log: https://libera.monerologs.net/monero-research-lab/20230607#c253852
19:59:19 <kayabanerve[m]> That wasn't about Coq yet about reaching out without proper scoping/justification.