LAWS.bend

bend-osdev-cipher-core@0.1.0.0 · 121 lines · 16 definitions

1# Laws about cipher-core's public interface: 64-bit blocks survive their
2# byte form, the 64-bit modes refuse what is not whole blocks; and the
3# lemmas the ciphers' proofs share (XOR undone, the rotations and byte swaps
4# on bits undone, Feistel rounds undone, the 64-bit modes' layers), as laws.
5import Base
6import bend-osdev-bytes@0.1.1.0/bytes.bend as B
7import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
8import bend-osdev-cipher-core@0.1.0.0/modes64.bend as X
9
10# 64-bit blocks as bytes: a block read back from its 8 bytes is itself, 8
11# bytes read as a block are written back as those bytes, and a list of
12# blocks read back from its bytes is itself
13law block64_octets_round_trip:
14  for +b: L.LcBlock64
15  {L.LcBlock64.of_octets(L.LcBlock64.to_octets(b)) == Some{b} : Maybe<&2, L.LcBlock64>}
16
17law block64_octets_dual:
18  for +o: B.Octets
19  for +b: L.LcBlock64
20  for e: {L.LcBlock64.of_octets(o) == Some{b} : Maybe<&2, L.LcBlock64>}
21  {L.LcBlock64.to_octets(b) == o : B.Octets}
22
23law blocks64_octets_round_trip:
24  for +bs: List<&2, L.LcBlock64>
25  {X.Lc64.blocks_of(X.Lc64.octets_of(bs)) == Done{bs} : Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>}
26
27# Lemmas the ciphers' proofs share, as laws (a package's proofs can use
28# another package's laws, not its private lemmas). Each is stated simple
29# side first, the form a rewrite (%e : P) takes.
30
31# XOR undone, for every word of any width, every 32-bit word and every
32# 64-bit block
33law word_xor_cancel:
34  for n: Nat
35  for a: Word(n)
36  for b: Word(n)
37  {a == Word.xor(n, Word.xor(n, a, b), b) : Word(n)}
38
39law u32_xor_cancel:
40  for a: U32
41  for b: U32
42  {a == U32.xor(U32.xor(a, b), b) : U32}
43
44law block64_xor_cancel:
45  for a: L.LcBlock64
46  for b: L.LcBlock64
47  {b == L.LcBlock64.xor(a, L.LcBlock64.xor(a, b)) : L.LcBlock64}
48
49# the rotations by 1 and 31 bits on bits undo each other, and the byte swap
50# on bits undoes itself, for every word
51law rotl1_rotl31:
52  for x: U32
53  {x == L.lc.rotl1.bits(L.lc.rotl31.bits(x)) : U32}
54
55law rotl31_rotl1:
56  for x: U32
57  {x == L.lc.rotl31.bits(L.lc.rotl1.bits(x)) : U32}
58
59law bswap_bswap:
60  for x: U32
61  {x == L.lc.bswap.bits(L.lc.bswap.bits(x)) : U32}
62
63# Feistel rounds over any round function f and any round keys: the rounds
64# undone last to first undo the rounds, and the other way round
65law feistel_unrun_run:
66  for ~RK: Data
67  for ~f: RK -> U32 -> U32
68  for ks: List<&2, RK>
69  for +b: L.LcBlock64
70  {b == L.lc.fe.unrun(~RK, ~f, ks, L.lc.fe.run(~RK, ~f, ks, b)) : L.LcBlock64}
71
72law feistel_run_unrun:
73  for ~RK: Data
74  for ~f: RK -> U32 -> U32
75  for ks: List<&2, RK>
76  for +b: L.LcBlock64
77  {b == L.lc.fe.run(~RK, ~f, ks, L.lc.fe.unrun(~RK, ~f, ks, b)) : L.LcBlock64}
78
79# The 64-bit modes over any cipher: decryption after encryption on blocks is
80# the structural forms' (X.m64.ecb, X.m64.cbc.enc, X.m64.cbc.dec), over
81# which a cipher's own round trip proves the mode's by induction; and on
82# bytes, for the bytes of a list of blocks under the bytes of an IV, it is
83# the block layer's
84law modes64_ecb_blocks:
85  for ~K: Data
86  for ~enc: K -> L.LcBlock64 -> L.LcBlock64
87  for ~dec: K -> L.LcBlock64 -> L.LcBlock64
88  for +k: K
89  for +bs: List<&2, L.LcBlock64>
90  {X.m64.ecb(~K, ~dec, k, X.m64.ecb(~K, ~enc, k, bs)) == X.Lc64.ecb_decrypt_blocks(~K, ~dec, k, X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs)) : List<&2, L.LcBlock64>}
91
92law modes64_cbc_blocks:
93  for ~K: Data
94  for ~enc: K -> L.LcBlock64 -> L.LcBlock64
95  for ~dec: K -> L.LcBlock64 -> L.LcBlock64
96  for +k: K
97  for +iv: L.LcBlock64
98  for +bs: List<&2, L.LcBlock64>
99  {X.m64.cbc.dec(~K, ~dec, k, X.m64.cbc.enc(~K, ~enc, k, bs, iv), iv) == X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs)) : List<&2, L.LcBlock64>}
100
101law modes64_ecb_octets:
102  for ~K: Data
103  for ~enc: K -> L.LcBlock64 -> L.LcBlock64
104  for ~dec: K -> L.LcBlock64 -> L.LcBlock64
105  for +k: K
106  for +bs: List<&2, L.LcBlock64>
107  {Done{X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~dec, k, X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs)))} == Result.bind(&2, &2, L.LcError, B.Octets, B.Octets, X.Lc64.ecb_encrypt(~K, ~enc, k, X.Lc64.octets_of(bs)), c => X.Lc64.ecb_decrypt(~K, ~dec, k, c)) : Result<&2, &2, L.LcError, B.Octets>}
108
109law modes64_cbc_octets:
110  for ~K: Data
111  for ~enc: K -> L.LcBlock64 -> L.LcBlock64
112  for ~dec: K -> L.LcBlock64 -> L.LcBlock64
113  for +k: K
114  for +iv: L.LcBlock64
115  for +bs: List<&2, L.LcBlock64>
116  {Done{X.Lc64.octets_of(X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs)))} == Result.bind(&2, &2, L.LcError, B.Octets, B.Octets, X.Lc64.cbc_encrypt(~K, ~enc, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(bs)), c => X.Lc64.cbc_decrypt(~K, ~dec, k, L.LcBlock64.to_octets(iv), c)) : Result<&2, &2, L.LcError, B.Octets>}
117
118
119# the 64-bit modes refuse a message that is not whole blocks
120law modes64_not_whole_blocks:
121  {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, Unit, bs => Unit{}, X.Lc64.blocks_of(B.Octets.zeros(12n))) == Fail{L.LcNotBlockMultiple{12n}} : Result<&2, &2, L.LcError, Unit>}