1	# CBC, cipher block chaining (NIST SP 800-38A, section 6.2), over any 128-bit
2	# block cipher (see mode-core.bend for the template arguments):
3	#   C_1 = E(P_1 xor IV),  C_j = E(P_j xor C_(j-1))
4	#   P_1 = D(C_1) xor IV,  P_j = D(C_j) xor C_(j-1)
5	# The block layer (encrypt_blocks, decrypt_blocks) works on lists of blocks;
6	# chaining one call's last ciphertext block into the next call's IV encrypts a
7	# long message in pieces. The byte layer takes Octets: a whole number of
8	# blocks, or any length with PKCS #7 padding (pkcs7.bend).
9	import Base
10	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
11	import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
12	import bend-osdev-pkcs7@0.1.0.0/pkcs7.bend as P
13	
14	# The block layer
15	
16	def cbc.enc(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>:
17	  match bs:
18	    case Nil{}:
19	      Nil{}
20	    case Con{p, t}:
21	      +c = enc(k, M.CmBlock.xor(iv, p))
22	      Con{c, cbc.enc(~K, ~enc, k, t, c)}
23	
24	def cbc.dec(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>:
25	  match bs:
26	    case Nil{}:
27	      Nil{}
28	    case Con{+c, t}:
29	      Con{M.CmBlock.xor(iv, dec(k, c)), cbc.dec(~K, ~dec, k, t, c)}
30	
31	# The same, tail-recursive (the ciphertext so far kept reversed in acc), so a
32	# message can be of any length: PROOF.bend proves each equal to its structural
33	# form above for every input
34	
35	def cbc.enc.go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock, acc: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
36	  match bs:
37	    case Nil{}:
38	      M.cm.blocks.rev_onto(acc, Nil{})
39	    case Con{p, t}:
40	      +c = enc(k, M.CmBlock.xor(iv, p))
41	      cbc.enc.go(~K, ~enc, k, t, c, Con{c, acc})
42	
43	def cbc.enc.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>:
44	  cbc.enc.go(~K, ~enc, k, bs, iv, Nil{})
45	
46	def cbc.dec.go(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock, acc: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
47	  match bs:
48	    case Nil{}:
49	      M.cm.blocks.rev_onto(acc, Nil{})
50	    case Con{+c, t}:
51	      cbc.dec.go(~K, ~dec, k, t, c, Con{M.CmBlock.xor(iv, dec(k, c)), acc})
52	
53	def cbc.dec.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>:
54	  cbc.dec.go(~K, ~dec, k, bs, iv, Nil{})
55	
56	def Cbc.encrypt_blocks(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: M.CmBlock, bs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
57	  cbc.enc.fast(~K, ~enc, k, bs, iv)
58	
59	def Cbc.decrypt_blocks(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: M.CmBlock, bs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
60	  cbc.dec.fast(~K, ~dec, k, bs, iv)
61	
62	# The byte layer
63	
64	def cbc.iv(o: B.Octets) -> Result<&2, &2, M.CmError, M.CmBlock>:
65	  +xs = B.Octets.to_list(o)
66	  M.cm.need_block(xs, M.CmBadIvLength{B.len(xs)})
67	
68	# the whole blocks under v, or CmNotBlockMultiple(n) if bytes are left over
69	def cbc.e2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
70	  match s:
71	    case M.CmSplit{bs, tail}:
72	      match tail:
73	        case Nil{}:
74	          Done{B.Octets.of_list(M.cm.join(cbc.enc(~K, ~enc, k, bs, v)))}
75	        case Con{h, t}:
76	          Fail{M.CmNotBlockMultiple{n}}
77	
78	def cbc.e1(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
79	  match r:
80	    case Fail{e}:
81	      Fail{e}
82	    case Done{v}:
83	      cbc.e2(~K, ~enc, k, v, M.cm.split(xs), B.len(xs))
84	
85	def cbc.d2(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
86	  match s:
87	    case M.CmSplit{bs, tail}:
88	      match tail:
89	        case Nil{}:
90	          Done{B.Octets.of_list(M.cm.join(cbc.dec(~K, ~dec, k, bs, v)))}
91	        case Con{h, t}:
92	          Fail{M.CmNotBlockMultiple{n}}
93	
94	def cbc.d1(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
95	  match r:
96	    case Fail{e}:
97	      Fail{e}
98	    case Done{v}:
99	      cbc.d2(~K, ~dec, k, v, M.cm.split(xs), B.len(xs))
100	
101	# m (a whole number of blocks) under the 16-byte iv
102	# The byte layer, tail-recursive: what Cbc.encrypt and Cbc.decrypt run
103	# (cbc.e1 .. cbc.d2 are the structural forms; PROOF.bend: cbcp.e1_eq, d1_eq)
104	
105	def cbc.e2.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
106	  match s:
107	    case M.CmSplit{bs, tail}:
108	      match tail:
109	        case Nil{}:
110	          Done{B.Octets.of_list(M.cm.join_onto.fast(cbc.enc.fast(~K, ~enc, k, bs, v), Nil{}))}
111	        case Con{h, t}:
112	          Fail{M.CmNotBlockMultiple{n}}
113	
114	def cbc.e1.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
115	  match r:
116	    case Fail{e}:
117	      Fail{e}
118	    case Done{v}:
119	      cbc.e2.fast(~K, ~enc, k, v, M.cm.split.fast(xs), B.len.fast(xs))
120	
121	def cbc.d2.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
122	  match s:
123	    case M.CmSplit{bs, tail}:
124	      match tail:
125	        case Nil{}:
126	          Done{B.Octets.of_list(M.cm.join_onto.fast(cbc.dec.fast(~K, ~dec, k, bs, v), Nil{}))}
127	        case Con{h, t}:
128	          Fail{M.CmNotBlockMultiple{n}}
129	
130	def cbc.d1.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
131	  match r:
132	    case Fail{e}:
133	      Fail{e}
134	    case Done{v}:
135	      cbc.d2.fast(~K, ~dec, k, v, M.cm.split.fast(xs), B.len.fast(xs))
136	
137	# Cbc.encrypt and Cbc.decrypt through the structural forms (the laws' proofs
138	# reason about these; PROOF.bend proves them equal to the public defs)
139	def Cbc.encrypt.ref(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
140	  cbc.e1(~K, ~enc, k, cbc.iv(iv), B.Octets.to_list(m))
141	
142	def Cbc.decrypt.ref(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
143	  cbc.d1(~K, ~dec, k, cbc.iv(iv), B.Octets.to_list(c))
144	
145	def Cbc.encrypt(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
146	  cbc.e1.fast(~K, ~enc, k, cbc.iv(iv), B.Octets.to_list(m))
147	
148	def Cbc.decrypt(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
149	  cbc.d1.fast(~K, ~dec, k, cbc.iv(iv), B.Octets.to_list(c))
150	
151	# m of any length, PKCS #7 padded to whole blocks, then encrypted
152	def Cbc.encrypt_padded(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
153	  do Result<&2, &2, M.CmError, B.Octets>:
154	    padded : B.Octets <- P.Pkcs7.pad(16n, m)
155	    Cbc.encrypt(~K, ~enc, k, iv, padded)
156	
157	# decrypted, then the padding checked and removed (CmBadPadding)
158	def Cbc.decrypt_padded(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, +c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
159	  +n = B.Octets.len(c)
160	  do Result<&2, &2, M.CmError, B.Octets>:
161	    M.cm.check(Nat.is_lt(0n, n), M.CmTooShort{n})
162	    padded : B.Octets <- Cbc.decrypt(~K, ~dec, k, iv, c)
163	    P.Pkcs7.unpad(16n, padded)