def nonce_size
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead.bend as Aeadimport Base
50def nonce_size(alg: Alg) -> Nat:
51 match alg:
52 case CHACHA20_POLY1305{}: 12n
53 case XCHACHA20_POLY1305{}: 24n
54 case AES_128_GCM{}: 12n
55 case AES_256_GCM{}: 12n
Uses (2)
Used by (14)
- bend-collections-laws-crypto@1.0.0.0/src/crypto/aead:valid
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof:decrypt_valid
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof:encrypt_valid
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof:valid_true
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof:ds_open
- …