1	# CBC over a toy permutation (below): the block and byte layers both ways,
2	# padding, and the refusals; and 32 KB through CBC and back. The
3	# specification's vectors (SP 800-38A F.2) run over AES in
4	# bend-osdev-aes-modes' check.bend.
5	import Base
6	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
7	import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
8	import ./cbc.bend as C
9	
10	def err(e: M.CmError) -> String:
11	  match e:
12	    case M.CmBadKeyLength{n}:
13	      "CmBadKeyLength"
14	    case M.CmBadIvLength{n}:
15	      "CmBadIvLength"
16	    case M.CmBadTweakLength{n}:
17	      "CmBadTweakLength"
18	    case M.CmBadNonceLength{n}:
19	      "CmBadNonceLength"
20	    case M.CmBadTagLength{n}:
21	      "CmBadTagLength"
22	    case M.CmBadBlockSize{n}:
23	      "CmBadBlockSize"
24	    case M.CmNotBlockMultiple{n}:
25	      "CmNotBlockMultiple"
26	    case M.CmTooShort{n}:
27	      "CmTooShort"
28	    case M.CmTooLong{n}:
29	      "CmTooLong"
30	    case M.CmBadPadding{}:
31	      "CmBadPadding"
32	    case M.CmTagMismatch{}:
33	      "CmTagMismatch"
34	
35	def res(r: Result<&2, &2, M.CmError, B.Octets>) -> String:
36	  match r:
37	    case Fail{e}:
38	      "fail " ++ err(e)
39	    case Done{v}:
40	      B.Octets.hex(v)
41	
42	# whether r is m
43	def back(r: Result<&2, &2, M.CmError, B.Octets>, +m: B.Octets) -> String:
44	  match r:
45	    case Fail{e}:
46	      "fail " ++ err(e)
47	    case Done{o}:
48	      Bool.show(B.Octets.is_eq(o, m))
49	
50	# n pseudo-random bytes (a linear congruential generator)
51	def bytes.go(n: Nat, +s: U32, acc: List<&2, U32>) -> List<&2, U32>:
52	  match n:
53	    case 0n:
54	      acc
55	    case 1n+p:
56	      +s2 = U32.add(U32.mul(s, 1103515245), 12345)
57	      bytes.go(p, s2, Con{U32.and(U32.shrn(s2, 16n), 255), acc})
58	
59	def msg(n: Nat) -> B.Octets:
60	  B.Octets.of_list(bytes.go(n, 7, Nil{}))
61	
62	def iv() -> B.Octets:
63	  B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15])
64	
65	# A toy permutation of blocks, NOT a cipher: the words rotated, then XOR
66	# with the key block. Enough to run the mode's code paths (encryption and
67	# decryption differ, so mixing them up shows); the mode is tested against
68	# its specification over AES in bend-osdev-aes-modes (the specifications'
69	# vectors) and in ref/ (against Python's cryptography).
70	def toy.rot(b: M.CmBlock) -> M.CmBlock:
71	  match b:
72	    case M.CmBlock{w0, w1, w2, w3}:
73	      M.CmBlock{w1, w2, w3, w0}
74	
75	def toy.unrot(b: M.CmBlock) -> M.CmBlock:
76	  match b:
77	    case M.CmBlock{w0, w1, w2, w3}:
78	      M.CmBlock{w3, w0, w1, w2}
79	
80	def toy.enc(k: M.CmBlock, b: M.CmBlock) -> M.CmBlock:
81	  M.CmBlock.xor(k, toy.rot(b))
82	
83	def toy.dec(k: M.CmBlock, c: M.CmBlock) -> M.CmBlock:
84	  toy.unrot(M.CmBlock.xor(k, c))
85	
86	def key() -> M.CmBlock:
87	  M.CmBlock{19088743, 2309737967, 4275878552, 1985229328}
88	
89	def key2() -> M.CmBlock:
90	  M.CmBlock{2882400001, 305419896, 3735928559, 4027432973}
91	
92	def hexs(bs: List<&2, M.CmBlock>) -> String:
93	  match bs:
94	    case Nil{}:
95	      ""
96	    case Con{b, t}:
97	      M.CmBlock.hex(b) ++ hexs(t)
98	
99	def main() -> IO(Unit):
100	  +b1 : M.CmBlock = M.CmBlock{1122867, 1146447479, 2291772091, 3437096703}
101	  +b2 : M.CmBlock = M.CmBlock{1, 2, 3, 4}
102	  +m48 = msg(48n)
103	  +m21 = msg(21n)
104	  +big = msg(32768n)
105	  do IO<Unit>:
106	    IO.print("cbc_blocks " ++ hexs(C.Cbc.encrypt_blocks(~M.CmBlock, ~toy.enc, key(), key2(), [b1, b2])))
107	    IO.print("cbc_blocks_back " ++ hexs(C.Cbc.decrypt_blocks(~M.CmBlock, ~toy.dec, key(), key2(), C.Cbc.encrypt_blocks(~M.CmBlock, ~toy.enc, key(), key2(), [b1, b2]))))
108	    IO.print("cbc_enc " ++ res(C.Cbc.encrypt(~M.CmBlock, ~toy.enc, key(), iv(), m48)))
109	    IO.print("cbc_back " ++ back(Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.Cbc.encrypt(~M.CmBlock, ~toy.enc, key(), iv(), m48), c => C.Cbc.decrypt(~M.CmBlock, ~toy.dec, key(), iv(), c)), m48))
110	    IO.print("cbc_padded_enc " ++ res(C.Cbc.encrypt_padded(~M.CmBlock, ~toy.enc, key(), iv(), m21)))
111	    IO.print("cbc_padded_back " ++ back(Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.Cbc.encrypt_padded(~M.CmBlock, ~toy.enc, key(), iv(), m21), c => C.Cbc.decrypt_padded(~M.CmBlock, ~toy.dec, key(), iv(), c)), m21))
112	    IO.print("cbc_padded_empty_back " ++ back(Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.Cbc.encrypt_padded(~M.CmBlock, ~toy.enc, key(), iv(), B.Octets.empty()), c => C.Cbc.decrypt_padded(~M.CmBlock, ~toy.dec, key(), iv(), c)), B.Octets.empty()))
113	    IO.print("cbc_not_whole_blocks " ++ res(C.Cbc.encrypt(~M.CmBlock, ~toy.enc, key(), iv(), msg(17n))))
114	    IO.print("cbc_short_iv " ++ res(C.Cbc.encrypt(~M.CmBlock, ~toy.enc, key(), B.Octets.take(15n, iv()), m48)))
115	    IO.print("cbc_padded_empty_ciphertext " ++ res(C.Cbc.decrypt_padded(~M.CmBlock, ~toy.dec, key(), iv(), B.Octets.empty())))
116	    IO.print("cbc_bad_padding " ++ res(Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.Cbc.encrypt(~M.CmBlock, ~toy.enc, key(), iv(), B.Octets.zeros(16n)), c => C.Cbc.decrypt_padded(~M.CmBlock, ~toy.dec, key(), iv(), c))))
117	    IO.print("cbc_32k " ++ back(Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.Cbc.encrypt(~M.CmBlock, ~toy.enc, key(), iv(), big), c => C.Cbc.decrypt(~M.CmBlock, ~toy.dec, key(), iv(), c)), big))
118	
119	#|cbc_blocks 57427568df9fd9bbc20c946add88ff22debc9cde4ba75986235445be21164779
120	#|cbc_blocks_back 00112233445566778899aabbccddeeff00000001000000020000000300000004
121	#|cbc_enc 581a5d37558aaff7f1053e55b60b5efd353eca1da279d0466c19820c40db694db0973410cb906af02c739db90187eab3
122	#|cbc_back True
123	#|cbc_padded_enc 6c64ae723fb10a45c3ff96b28a71fe7552994429415f50567fa64fe609a2e82c
124	#|cbc_padded_back True
125	#|cbc_padded_empty_back True
126	#|cbc_not_whole_blocks fail CmNotBlockMultiple
127	#|cbc_short_iv fail CmBadIvLength
128	#|cbc_padded_empty_ciphertext fail CmTooShort
129	#|cbc_bad_padding fail CmBadPadding
130	#|cbc_32k True