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