src/crypto/aead.bend

bend-collections-laws-crypto@1.0.0.0 · 88 lines · 10 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead/chacha20poly1305.bend as CP
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/aesgcm.bend as GCM
4
5# Authenticated encryption with associated data (RFC 5116 shape).
6#
7#   encrypt(alg, key, nonce, aad, plaintext) -> Maybe(ciphertext || tag)
8#   decrypt(alg, key, nonce, aad, ciphertext || tag) -> Maybe(plaintext)
9#
10# Bytes are U32 values < 256. Every algorithm has a 16-byte tag appended to
11# the ciphertext. encrypt returns None unless the key and nonce have the
12# algorithm's lengths (key_size, nonce_size); decrypt also returns None for
13# an input shorter than the tag and whenever the tag is not the one computed
14# over aad and ciphertext (a forgery, a wrong key/nonce/aad, a modified
15# ciphertext), before any plaintext is produced.
16#
17#   algorithm            key  nonce  tag   standard
18#   CHACHA20_POLY1305    32   12     16    RFC 8439 2.8
19#   XCHACHA20_POLY1305   32   24     16    draft-irtf-cfrg-xchacha-03
20#   AES_128_GCM          16   12     16    FIPS 197 + SP 800-38D
21#   AES_256_GCM          32   12     16    FIPS 197 + SP 800-38D
22#
23# Adding an algorithm: a constructor of Alg, its row in key_size and
24# nonce_size, and its case in seal and open (the per-algorithm functions,
25# which may do their own length checks); encrypt and decrypt check the
26# lengths and dispatch, and the laws in proofs/crypto/aead/laws.bend are
27# proved by one case per algorithm.
28#
29# Proved (proofs/crypto/aead/): each algorithm equals its specification
30# (spec/crypto/chacha20poly1305.bend, spec/crypto/aes/gcm.bend),
31# decrypt(encrypt(x)) == Some(x) for every key, nonce, aad and plaintext of
32# the right lengths, and decrypt rejects ciphertext || t for every 16-byte t
33# other than the tag the specification computes. Constant time is not
34# provable in Bend (no timing model); the code does not branch or index on
35# secret bytes except for the final accept/reject.
36
37type Alg is Data:
38  CHACHA20_POLY1305{}
39  XCHACHA20_POLY1305{}
40  AES_128_GCM{}
41  AES_256_GCM{}
42
43def key_size(alg: Alg) -> Nat:
44  match alg:
45    case CHACHA20_POLY1305{}: 32n
46    case XCHACHA20_POLY1305{}: 32n
47    case AES_128_GCM{}: 16n
48    case AES_256_GCM{}: 32n
49
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
56
57def tag_size() -> Nat:
58  16n
59
60# ciphertext || tag (encrypt checks the key and nonce lengths first).
61def seal(alg: Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +pt: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
62  match alg:
63    case CHACHA20_POLY1305{}: Some{CP.seal(key, nonce, aad, pt)}
64    case XCHACHA20_POLY1305{}: Some{CP.xseal(key, nonce, aad, pt)}
65    case AES_128_GCM{}: GCM.aes128_gcm_encrypt(key, nonce, aad, pt)
66    case AES_256_GCM{}: GCM.aes256_gcm_encrypt(key, nonce, aad, pt)
67
68# The plaintext of ciphertext || tag, or None (decrypt checks the lengths first).
69def open(alg: Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +data: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
70  match alg:
71    case CHACHA20_POLY1305{}: CP.open(key, nonce, aad, data)
72    case XCHACHA20_POLY1305{}: CP.xopen(key, nonce, aad, data)
73    case AES_128_GCM{}: GCM.aes128_gcm_decrypt(key, nonce, aad, data)
74    case AES_256_GCM{}: GCM.aes256_gcm_decrypt(key, nonce, aad, data)
75
76def valid(+alg: Alg, +key: List<&2, U32>, +nonce: List<&2, U32>) -> Bool:
77  Bool.and(Nat.is_eq(List.length(&2, U32, key), key_size(alg)), Nat.is_eq(List.length(&2, U32, nonce), nonce_size(alg)))
78
79def when_open(ok: Bool, r: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
80  match ok:
81    case True{}: r
82    case False{}: None{}
83
84def encrypt(+alg: Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +pt: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
85  when_open(valid(alg, key, nonce), seal(alg, key, nonce, aad, pt))
86
87def decrypt(+alg: Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +data: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
88  when_open(valid(alg, key, nonce), open(alg, key, nonce, aad, data))