1	# Modes of operation for 64-bit block ciphers (DES, 3DES): ECB and CBC
2	# (NIST SP 800-38A, sections 6.1 and 6.2), over any cipher on LcBlock64.
3	#
4	# cipher-modes' modes are written for 128-bit blocks (CmBlock), so a 64-bit
5	# cipher cannot use them; these are the same modes on LcBlock64, with the
6	# cipher as template arguments in cipher-modes' style:
7	#   ~K: Data                                  the cipher's (expanded) key
8	#   ~enc: K -> LcBlock64 -> LcBlock64         encrypt one block
9	#   ~dec: K -> LcBlock64 -> LcBlock64         decrypt one block
10	# for instance ~D.LcDesKey, ~D.LcDes.encrypt, ~D.LcDes.decrypt. For padding,
11	# cipher-modes' Pkcs7.pad(8n, m) and Pkcs7.unpad(8n, m) take any block size.
12	#
13	# The block layer works on lists of blocks: chaining one call's last
14	# ciphertext block into the next call's IV encrypts a long message in pieces.
15	# The byte layer takes Octets of whole blocks.
16	import Base
17	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
18	import ./legacy_ciphers.bend as L
19	
20	# Block lists, structurally (the forms the proofs reason about)
21	
22	def m64.ecb(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
23	  match bs:
24	    case Nil{}:
25	      Nil{}
26	    case Con{b, t}:
27	      Con{f(k, b), m64.ecb(~K, ~f, k, t)}
28	
29	# C_1 = E(P_1 xor IV), C_j = E(P_j xor C_(j-1))
30	def m64.cbc.enc(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, iv: L.LcBlock64) -> List<&2, L.LcBlock64>:
31	  match bs:
32	    case Nil{}:
33	      Nil{}
34	    case Con{p, t}:
35	      +c = enc(k, L.LcBlock64.xor(iv, p))
36	      Con{c, m64.cbc.enc(~K, ~enc, k, t, c)}
37	
38	# P_1 = D(C_1) xor IV, P_j = D(C_j) xor C_(j-1)
39	def m64.cbc.dec(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, iv: L.LcBlock64) -> List<&2, L.LcBlock64>:
40	  match bs:
41	    case Nil{}:
42	      Nil{}
43	    case Con{+c, t}:
44	      Con{L.LcBlock64.xor(iv, dec(k, c)), m64.cbc.dec(~K, ~dec, k, t, c)}
45	
46	# The same, tail-recursive (the output so far kept reversed in acc), so a
47	# message can be of any length: PROOF.bend proves each equal to its
48	# structural form for every input
49	
50	def m64.rev_onto(bs: List<&2, L.LcBlock64>, acc: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
51	  match bs:
52	    case Nil{}:
53	      acc
54	    case Con{b, t}:
55	      m64.rev_onto(t, Con{b, acc})
56	
57	def m64.ecb.go(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, acc: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
58	  match bs:
59	    case Nil{}:
60	      m64.rev_onto(acc, Nil{})
61	    case Con{b, t}:
62	      m64.ecb.go(~K, ~f, k, t, Con{f(k, b), acc})
63	
64	def m64.cbc.enc.go(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, iv: L.LcBlock64, acc: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
65	  match bs:
66	    case Nil{}:
67	      m64.rev_onto(acc, Nil{})
68	    case Con{p, t}:
69	      +c = enc(k, L.LcBlock64.xor(iv, p))
70	      m64.cbc.enc.go(~K, ~enc, k, t, c, Con{c, acc})
71	
72	def m64.cbc.dec.go(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, iv: L.LcBlock64, acc: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
73	  match bs:
74	    case Nil{}:
75	      m64.rev_onto(acc, Nil{})
76	    case Con{+c, t}:
77	      m64.cbc.dec.go(~K, ~dec, k, t, c, Con{L.LcBlock64.xor(iv, dec(k, c)), acc})
78	
79	# The block layer
80	
81	def Lc64.ecb_encrypt_blocks(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
82	  m64.ecb.go(~K, ~enc, k, bs, Nil{})
83	
84	def Lc64.ecb_decrypt_blocks(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
85	  m64.ecb.go(~K, ~dec, k, bs, Nil{})
86	
87	def Lc64.cbc_encrypt_blocks(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, iv: L.LcBlock64, bs: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
88	  m64.cbc.enc.go(~K, ~enc, k, bs, iv, Nil{})
89	
90	def Lc64.cbc_decrypt_blocks(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, iv: L.LcBlock64, bs: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
91	  m64.cbc.dec.go(~K, ~dec, k, bs, iv, Nil{})
92	
93	# The byte layer
94	
95	# the bytes as whole blocks (reversed onto acc), or None if bytes are left over
96	def m64.split(xs: List<&2, U32>, acc: List<&2, L.LcBlock64>) -> Maybe<&2, List<&2, L.LcBlock64>>:
97	  match xs:
98	    case Nil{}:
99	      Some{m64.rev_onto(acc, Nil{})}
100	    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, t}}}}}}}}:
101	      m64.split(t, Con{L.lc.block8(a0, a1, a2, a3, a4, a5, a6, a7), acc})
102	    case _:
103	      None{}
104	
105	# the bytes of the blocks (reversed) in front of acc
106	def m64.join(rs: List<&2, L.LcBlock64>, acc: List<&2, U32>) -> List<&2, U32>:
107	  match rs:
108	    case Nil{}:
109	      acc
110	    case Con{b, t}:
111	      m64.join(t, L.lc.block_bytes(b, acc))
112	
113	def m64.octets(bs: List<&2, L.LcBlock64>) -> B.Octets:
114	  B.Octets.of_list(m64.join(m64.rev_onto(bs, Nil{}), Nil{}))
115	
116	def m64.blocks(+n: Nat, m: Maybe<&2, List<&2, L.LcBlock64>>) -> Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>:
117	  match m:
118	    case None{}:
119	      Fail{L.LcNotBlockMultiple{n}}
120	    case Some{bs}:
121	      Done{bs}
122	
123	# the message as whole blocks, or LcNotBlockMultiple
124	def Lc64.blocks_of(+o: B.Octets) -> Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>:
125	  m64.blocks(B.Octets.len(o), m64.split(B.Octets.to_list(o), Nil{}))
126	
127	# the blocks' bytes, in order
128	def Lc64.octets_of(bs: List<&2, L.LcBlock64>) -> B.Octets:
129	  m64.octets(bs)
130	
131	def m64.iv(m: Maybe<&2, L.LcBlock64>, +n: Nat) -> Result<&2, &2, L.LcError, L.LcBlock64>:
132	  match m:
133	    case None{}:
134	      Fail{L.LcBadIvLength{n}}
135	    case Some{b}:
136	      Done{b}
137	
138	def Lc64.ecb_encrypt(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, m: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
139	  Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, bs => Lc64.octets_of(Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs)), Lc64.blocks_of(m))
140	
141	def Lc64.ecb_decrypt(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, c: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
142	  Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, bs => Lc64.octets_of(Lc64.ecb_decrypt_blocks(~K, ~dec, k, bs)), Lc64.blocks_of(c))
143	
144	def m64.cbc.e2(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, v: L.LcBlock64, r: Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>) -> Result<&2, &2, L.LcError, B.Octets>:
145	  match r:
146	    case Fail{e}:
147	      Fail{e}
148	    case Done{bs}:
149	      Done{Lc64.octets_of(Lc64.cbc_encrypt_blocks(~K, ~enc, k, v, bs))}
150	
151	def m64.cbc.e1(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, r: Result<&2, &2, L.LcError, L.LcBlock64>, +m: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
152	  match r:
153	    case Fail{e}:
154	      Fail{e}
155	    case Done{v}:
156	      m64.cbc.e2(~K, ~enc, k, v, Lc64.blocks_of(m))
157	
158	def m64.cbc.d2(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, v: L.LcBlock64, r: Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>) -> Result<&2, &2, L.LcError, B.Octets>:
159	  match r:
160	    case Fail{e}:
161	      Fail{e}
162	    case Done{bs}:
163	      Done{Lc64.octets_of(Lc64.cbc_decrypt_blocks(~K, ~dec, k, v, bs))}
164	
165	def m64.cbc.d1(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, r: Result<&2, &2, L.LcError, L.LcBlock64>, +c: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
166	  match r:
167	    case Fail{e}:
168	      Fail{e}
169	    case Done{v}:
170	      m64.cbc.d2(~K, ~dec, k, v, Lc64.blocks_of(c))
171	
172	# m (whole blocks) under the 8-byte iv
173	def Lc64.cbc_encrypt(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +iv: B.Octets, +m: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
174	  m64.cbc.e1(~K, ~enc, k, m64.iv(L.LcBlock64.of_octets(iv), B.Octets.len(iv)), m)
175	
176	def Lc64.cbc_decrypt(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +iv: B.Octets, +c: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
177	  m64.cbc.d1(~K, ~dec, k, m64.iv(L.LcBlock64.of_octets(iv), B.Octets.len(iv)), c)