1	import Base
2	import ./aead/chacha20poly1305.bend as CP
3	import ./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	
37	type Alg is Data:
38	  CHACHA20_POLY1305{}
39	  XCHACHA20_POLY1305{}
40	  AES_128_GCM{}
41	  AES_256_GCM{}
42	
43	def 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	
50	def 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	
57	def tag_size() -> Nat:
58	  16n
59	
60	# ciphertext || tag (encrypt checks the key and nonce lengths first).
61	def 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).
69	def 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	
76	def 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	
79	def 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	
84	def 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	
87	def 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))