check.bend

bend-osdev-pkcs7@0.1.0.0 · 90 lines · 7 definitions

1# PKCS #7 padding (RFC 5652, 6.3): padding to 16 and to 8 bytes, unpadding
2# back, and every refusal: bad padding, a bad block size, a padded message
3# that is not whole blocks, and an empty one.
4import Base
5import bend-osdev-bytes@0.1.1.0/bytes.bend as B
6import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
7import bend-osdev-pkcs7@0.1.0.0/pkcs7.bend as P
8
9def err(e: M.CmError) -> String:
10  match e:
11    case M.CmBadKeyLength{n}:
12      "CmBadKeyLength"
13    case M.CmBadIvLength{n}:
14      "CmBadIvLength"
15    case M.CmBadTweakLength{n}:
16      "CmBadTweakLength"
17    case M.CmBadNonceLength{n}:
18      "CmBadNonceLength"
19    case M.CmBadTagLength{n}:
20      "CmBadTagLength"
21    case M.CmBadBlockSize{n}:
22      "CmBadBlockSize"
23    case M.CmNotBlockMultiple{n}:
24      "CmNotBlockMultiple"
25    case M.CmTooShort{n}:
26      "CmTooShort"
27    case M.CmTooLong{n}:
28      "CmTooLong"
29    case M.CmBadPadding{}:
30      "CmBadPadding"
31    case M.CmTagMismatch{}:
32      "CmTagMismatch"
33
34def res(r: Result<&2, &2, M.CmError, B.Octets>) -> String:
35  match r:
36    case Fail{e}:
37      "fail " ++ err(e)
38    case Done{v}:
39      B.Octets.hex(v)
40
41# whether r is m
42def back(r: Result<&2, &2, M.CmError, B.Octets>, +m: B.Octets) -> String:
43  match r:
44    case Fail{e}:
45      "fail " ++ err(e)
46    case Done{o}:
47      Bool.show(B.Octets.is_eq(o, m))
48
49# n pseudo-random bytes (a linear congruential generator)
50def bytes.go(n: Nat, +s: U32, acc: List<&2, U32>) -> List<&2, U32>:
51  match n:
52    case 0n:
53      acc
54    case 1n+p:
55      +s2 = U32.add(U32.mul(s, 1103515245), 12345)
56      bytes.go(p, s2, Con{U32.and(U32.shrn(s2, 16n), 255), acc})
57
58def msg(n: Nat) -> B.Octets:
59  B.Octets.of_list(bytes.go(n, 7, Nil{}))
60
61def iv() -> B.Octets:
62  B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15])
63
64def main() -> IO(Unit):
65  +m15 = msg(15n)
66  +m1000 = msg(1000n)
67  do IO<Unit>:
68    IO.print("pad_16_empty " ++ res(P.Pkcs7.pad(16n, B.Octets.empty())))
69    IO.print("pad_16_15 " ++ res(P.Pkcs7.pad(16n, m15)))
70    IO.print("pad_8_5 " ++ res(P.Pkcs7.pad(8n, msg(5n))))
71    IO.print("unpad_16_15 " ++ back(Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, P.Pkcs7.pad(16n, m15), c => P.Pkcs7.unpad(16n, c)), m15))
72    IO.print("unpad_255_1000 " ++ back(Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, P.Pkcs7.pad(255n, m1000), c => P.Pkcs7.unpad(255n, c)), m1000))
73    IO.print("pad_0 " ++ res(P.Pkcs7.pad(0n, m15)))
74    IO.print("pad_256 " ++ res(P.Pkcs7.pad(256n, m15)))
75    IO.print("unpad_zero " ++ res(P.Pkcs7.unpad(16n, B.Octets.append(m15, B.Octets.of_list([0])))))
76    IO.print("unpad_mixed " ++ res(P.Pkcs7.unpad(16n, B.Octets.append(B.Octets.take(13n, m15), B.Octets.of_list([2, 3, 3])))))
77    IO.print("unpad_not_whole " ++ res(P.Pkcs7.unpad(16n, m15)))
78    IO.print("unpad_empty " ++ res(P.Pkcs7.unpad(16n, B.Octets.empty())))
79
80#|pad_16_empty 10101010101010101010101010101010
81#|pad_16_15 ed12be13cda1312e22251392744e6c01
82#|pad_8_5 1392744e6c030303
83#|unpad_16_15 True
84#|unpad_255_1000 True
85#|pad_0 fail CmBadBlockSize
86#|pad_256 fail CmBadBlockSize
87#|unpad_zero fail CmBadPadding
88#|unpad_mixed fail CmBadPadding
89#|unpad_not_whole fail CmNotBlockMultiple
90#|unpad_empty fail CmTooShort