check.bend

bend-osdev-cbc@0.1.0.0 · 130 lines · 14 definitions

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.
5import Base
6import bend-osdev-bytes@0.1.1.0/bytes.bend as B
7import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
8import bend-osdev-cbc@0.1.0.0/cbc.bend as C
9
10def 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
35def 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
43def 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)
51def 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
59def msg(n: Nat) -> B.Octets:
60  B.Octets.of_list(bytes.go(n, 7, Nil{}))
61
62def 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).
70def 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
75def 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
80def toy.enc(k: M.CmBlock, b: M.CmBlock) -> M.CmBlock:
81  M.CmBlock.xor(k, toy.rot(b))
82
83def toy.dec(k: M.CmBlock, c: M.CmBlock) -> M.CmBlock:
84  toy.unrot(M.CmBlock.xor(k, c))
85
86def key() -> M.CmBlock:
87  M.CmBlock{19088743, 2309737967, 4275878552, 1985229328}
88
89def key2() -> M.CmBlock:
90  M.CmBlock{2882400001, 305419896, 3735928559, 4027432973}
91
92def 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
99def 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