~/jendhub

LAWS.bend

bend-osdev-cipher-modes@0.1.0.0 · 162 lines · 22 definitions

1# Laws about the public interface of every mode. The block cipher is the
2# template arguments ~K, ~enc, ~dec; laws that need decryption to undo
3# encryption take that as a hypothesis, ~inv, so they hold for every cipher
4# that satisfies it (AES's inverse is tested, not proved: see the README).
5import Base
6import bend-osdev-bytes@0.1.0.0/bytes.bend as B
7import bend-osdev-word64@0.1.0.0/word64.bend as W
8import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
9import bend-osdev-cipher-modes@0.1.0.0/aes.bend as X
10import bend-osdev-cipher-modes@0.1.0.0/pkcs7.bend as P
11import bend-osdev-cipher-modes@0.1.0.0/cbc.bend as C
12import bend-osdev-cipher-modes@0.1.0.0/xts.bend as T
13import bend-osdev-cipher-modes@0.1.0.0/ccm.bend as CC
14import bend-osdev-cipher-modes@0.1.0.0/cmac.bend as CM
15import bend-osdev-cipher-modes@0.1.0.0/aes_modes.bend as D
16
17# Properties, for every input
18
19# CBC on blocks: decryption undoes encryption, for every key, IV and message
20law cbc_blocks_round_trip:
21  for ~K: Data
22  for ~enc: K -> M.CmBlock -> M.CmBlock
23  for ~dec: K -> M.CmBlock -> M.CmBlock
24  for ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}
25  for +k: K
26  for iv: M.CmBlock
27  for bs: List<&2, M.CmBlock>
28  {C.Cbc.decrypt_blocks(~K, ~dec, k, iv, C.Cbc.encrypt_blocks(~K, ~enc, k, iv, bs)) == bs : List<&2, M.CmBlock>}
29
30# CBC on bytes: for every 16-byte IV and every message of whole blocks,
31# encryption succeeds and decryption gives the message back
32law cbc_round_trip:
33  for ~K: Data
34  for ~enc: K -> M.CmBlock -> M.CmBlock
35  for ~dec: K -> M.CmBlock -> M.CmBlock
36  for ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}
37  for +k: K
38  for +iv: B.Octets
39  for +m: B.Octets
40  for hi: {B.Octets.len(iv) == 16n : Nat}
41  for hm: {Nat.mod(B.Octets.len(m), 16n) == 0n : Nat}
42  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.Cbc.encrypt(~K, ~enc, k, iv, m), c => C.Cbc.decrypt(~K, ~dec, k, iv, c)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
43
44# XTS on blocks: decryption undoes encryption, for every data key and every
45# starting tweak (T_0 = Xts.tweak(k2, i), so every k2 and i are covered)
46law xts_blocks_round_trip:
47  for ~K: Data
48  for ~enc: K -> M.CmBlock -> M.CmBlock
49  for ~dec: K -> M.CmBlock -> M.CmBlock
50  for ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}
51  for +k1: K
52  for t: M.CmBlock
53  for bs: List<&2, M.CmBlock>
54  {T.Xts.decrypt_blocks(~K, ~dec, k1, t, T.Xts.encrypt_blocks(~K, ~enc, k1, t, bs)) == bs : List<&2, M.CmBlock>}
55
56# CMAC in pieces: the state after a ++ b is the state after a, then b, for
57# every cipher, key and state (so start, update .. update, finish is the MAC
58# of the pieces joined)
59law cmac_streaming:
60  for ~K: Data
61  for ~enc: K -> M.CmBlock -> M.CmBlock
62  for +k: K
63  for s: CM.CmacState
64  for +a: B.Octets
65  for +b: B.Octets
66  {CM.Cmac.update(~K, ~enc, k, s, B.Octets.append(a, b)) == CM.Cmac.update(~K, ~enc, k, CM.Cmac.update(~K, ~enc, k, s, a), b) : CM.CmacState}
67
68# XTS on bytes, with ciphertext stealing: for every 16-byte sequence number
69# and every data unit of at least 16 bytes, encryption succeeds and
70# decryption gives the data unit back
71law xts_round_trip:
72  for ~K: Data
73  for ~enc: K -> M.CmBlock -> M.CmBlock
74  for ~dec: K -> M.CmBlock -> M.CmBlock
75  for ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}
76  for +k1: K
77  for +k2: K
78  for +i: B.Octets
79  for +p: B.Octets
80  for hi: {B.Octets.len(i) == 16n : Nat}
81  for hp: {Nat.is_le(16n, B.Octets.len(p)) == True{} : Bool}
82  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, T.Xts.encrypt(~K, ~enc, k1, k2, i, p), c => T.Xts.decrypt(~K, ~enc, ~dec, k1, k2, i, c)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
83
84# CCM: decryption accepts what encryption produced and gives the message
85# back, for every cipher, key, tag length, nonce, associated data and
86# message; when the parameters are refused, both refuse alike
87law ccm_round_trip:
88  for ~K: Data
89  for ~enc: K -> M.CmBlock -> M.CmBlock
90  for +k: K
91  for +m: Nat
92  for +nonce: B.Octets
93  for +aad: B.Octets
94  for +p: B.Octets
95  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, CC.Ccm.encrypt(~K, ~enc, k, m, nonce, aad, p), c => CC.Ccm.decrypt(~K, ~enc, k, m, nonce, aad, c)) == Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => p, CC.Ccm.encrypt(~K, ~enc, k, m, nonce, aad, p)) : Result<&2, &2, M.CmError, B.Octets>}
96
97# A block written as Octets reads back as the same block, for every block
98law block_octets_round_trip:
99  for +b: M.CmBlock
100  {M.CmBlock.of_octets(M.CmBlock.to_octets(b)) == Some{b} : Maybe<&2, M.CmBlock>}
101
102# Vectors: the specifications' own test values, proved by computation. The
103# checker evaluates AES slowly and keeps what it evaluates, so only these fit
104# in its memory; every other vector of the four specifications (all of SP
105# 800-38A F.2.1, F.2.2, F.2.5 and F.2.6; IEEE 1619 vectors 2 and 15 to 18;
106# RFC 3610 packets 1 to 3; RFC 4493 examples 2 to 4; and every decryption)
107# runs compiled in check.bend.
108
109# FIPS 197 Appendix C.1: the named default cipher (AES-128) encrypts one block
110law aes128_fips197_c1:
111  {Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(X.CmAes.encrypt(k, M.CmBlock{1122867, 1146447479, 2291772091, 3437096703})), X.CmAes.key128(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]))) == Done{B.Octets.of_list([105, 196, 224, 216, 106, 123, 4, 48, 216, 205, 183, 128, 112, 180, 197, 90])} : Result<&2, &2, M.CmError, B.Octets>}
112
113# a key of a length AES-128 and AES-256 do not have is refused
114law aes_bad_key_length:
115  {D.CmAes.cbc_encrypt(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42])) == Fail{M.CmBadKeyLength{15n}} : Result<&2, &2, M.CmError, B.Octets>}
116
117# NIST SP 800-38A Appendix F.2.1, CBC-AES128: its first block
118law cbc_sp800_38a_f21_block1:
119  {D.CmAes.cbc_encrypt(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42])) == Done{B.Octets.of_list([118, 73, 171, 172, 129, 25, 178, 70, 206, 233, 142, 155, 18, 233, 25, 125])} : Result<&2, &2, M.CmError, B.Octets>}
120
121# the byte layer refuses a message that is not whole blocks, and a short IV
122law cbc_not_whole_blocks:
123  {D.CmAes.cbc_encrypt(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42, 174])) == Fail{M.CmNotBlockMultiple{17n}} : Result<&2, &2, M.CmError, B.Octets>}
124
125law cbc_short_iv:
126  {D.CmAes.cbc_encrypt(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42])) == Fail{M.CmBadIvLength{15n}} : Result<&2, &2, M.CmError, B.Octets>}
127
128# PKCS #7 (RFC 5652, 6.3): the empty message becomes a whole block of 16s; 15 bytes gain one 1
129law pkcs7_pad_empty:
130  {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>}
131
132law pkcs7_pad_15:
133  {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>}
134
135law pkcs7_unpad_15:
136  {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>}
137
138# a last byte of 0, or one the bytes before it contradict, is bad padding
139law pkcs7_unpad_zero:
140  {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>}
141
142law pkcs7_unpad_mixed:
143  {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>}
144
145# a data unit shorter than a block is refused
146law xts_short:
147  {D.CmAes.xts_encrypt(B.Octets.of_list([255, 254, 253, 252, 251, 250, 249, 248, 247, 246, 245, 244, 243, 242, 241, 240, 191, 190, 189, 188, 187, 186, 185, 184, 183, 182, 181, 180, 179, 178, 177, 176]), B.Octets.of_list([154, 120, 86, 52, 18, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])) == Fail{M.CmTooShort{15n}} : Result<&2, &2, M.CmError, B.Octets>}
148
149# the sequence number of sector n: n little-endian, zero-filled to 16 bytes
150law xts_sector:
151  {T.Xts.sector(W.W64.from_parts(0, 2591577138)) == B.Octets.of_list([50, 84, 120, 154, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) : B.Octets}
152
153# a tag of odd length, and a nonce of 6 bytes, are refused
154law ccm_bad_tag_length:
155  {D.CmAes.ccm_encrypt(B.Octets.of_list([192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207]), 7n, B.Octets.of_list([0, 0, 0, 3, 2, 1, 0, 160, 161, 162, 163, 164, 165]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7]), B.Octets.of_list([8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30])) == Fail{M.CmBadTagLength{7n}} : Result<&2, &2, M.CmError, B.Octets>}
156
157law ccm_bad_nonce_length:
158  {D.CmAes.ccm_encrypt(B.Octets.of_list([192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207]), 8n, B.Octets.of_list([0, 0, 0, 3, 2, 1]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7]), B.Octets.of_list([8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30])) == Fail{M.CmBadNonceLength{6n}} : Result<&2, &2, M.CmError, B.Octets>}
159
160# RFC 4493 section 4: the AES-CMAC subkey K1
161law cmac_rfc4493_k1:
162  {Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(CM.Cmac.subkey1(~X.CmAesKey, ~X.CmAes.encrypt, k)), X.CmAes.key128(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]))) == Done{B.Octets.of_list([251, 238, 214, 24, 53, 113, 51, 102, 124, 133, 224, 143, 114, 54, 168, 222])} : Result<&2, &2, M.CmError, B.Octets>}