3 ms·
the types of arguments and proofs used in cryptography are notoriously difficult to mechanize, a little bit of lean isn’t going to go get anywhere close to stat
by cmrx64 1y ago
the types of arguments and proofs used in cryptography are notoriously difficult to mechanize, a little bit of lean isn’t going to go get anywhere close to stating a security property.
eg CryptHOL needs a ton of infrastructure, and in still very limited: https://eprint.iacr.org/2017/753.pdf https://eprint.iacr.org/2017/753.pdf
- nioj 1y agoThere is also SSProve which has similar goal to CryptHOL: https://dl.acm.org/doi/full/10.1145/3594735 https://dl.acm.org/doi/full/10.1145/3594735 https://github.com/SSProve/ssprove https://github.com/SSProve/ssprove