LAWS.bend

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

1# Laws of PKCS #7 padding (pkcs7.bend), for every block size and message:
2# unpadding undoes padding, and padding gives a whole number of blocks; and
3# RFC 5652's padding examples, with the refusals of bad padding. The proofs
4# rest on bytes' and u32's laws only.
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-pkcs7@0.1.0.0/pkcs7.bend as P
9
10# Unpadding undoes padding, for every block size bs and message m: when bs
11# is one the padding takes (1 to 255), unpad(pad(m)) is m; when it is not,
12# both refuse alike (CmBadBlockSize)
13law pkcs7_round_trip:
14  for +bs: Nat
15  for +m: B.Octets
16  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, P.Pkcs7.pad(bs, m), c => P.Pkcs7.unpad(bs, c)) == Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => m, P.Pkcs7.pad(bs, m)) : Result<&2, &2, M.CmError, B.Octets>}
17
18# A padded message is a whole number of blocks, for every block size and
19# message
20law pkcs7_pad_blocks:
21  for +bs: Nat
22  for +m: B.Octets
23  {Result.map(&2, &2, M.CmError, B.Octets, Nat, c => Nat.mod(B.Octets.len(c), bs), P.Pkcs7.pad(bs, m)) == Result.map(&2, &2, M.CmError, B.Octets, Nat, c => 0n, P.Pkcs7.pad(bs, m)) : Result<&2, &2, M.CmError, Nat>}
24
25# PKCS #7 (RFC 5652, 6.3): the empty message becomes a whole block of 16s; 15 bytes gain one 1
26law pkcs7_pad_empty:
27  {P.Pkcs7.pad(16n, B.Octets.empty()) == Done{B.Octets.of_list([16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16])} : Result<&2, &2, M.CmError, B.Octets>}
28
29law pkcs7_pad_15:
30  {P.Pkcs7.pad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23])) == Done{B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 1])} : Result<&2, &2, M.CmError, B.Octets>}
31
32law pkcs7_unpad_15:
33  {P.Pkcs7.unpad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 1])) == Done{B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23])} : Result<&2, &2, M.CmError, B.Octets>}
34
35# a last byte of 0, or one the bytes before it contradict, is bad padding
36law pkcs7_unpad_zero:
37  {P.Pkcs7.unpad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 0])) == Fail{M.CmBadPadding{}} : Result<&2, &2, M.CmError, B.Octets>}
38
39law pkcs7_unpad_mixed:
40  {P.Pkcs7.unpad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 2, 3, 3])) == Fail{M.CmBadPadding{}} : Result<&2, &2, M.CmError, B.Octets>}