modes64.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 177 lines · 26 definitions

1# Modes of operation for 64-bit block ciphers (DES, 3DES): ECB and CBC
2# (NIST SP 800-38A, sections 6.1 and 6.2), over any cipher on LcBlock64.
3#
4# cipher-modes' modes are written for 128-bit blocks (CmBlock), so a 64-bit
5# cipher cannot use them; these are the same modes on LcBlock64, with the
6# cipher as template arguments in cipher-modes' style:
7#   ~K: Data                                  the cipher's (expanded) key
8#   ~enc: K -> LcBlock64 -> LcBlock64         encrypt one block
9#   ~dec: K -> LcBlock64 -> LcBlock64         decrypt one block
10# for instance ~D.LcDesKey, ~D.LcDes.encrypt, ~D.LcDes.decrypt. For padding,
11# cipher-modes' Pkcs7.pad(8n, m) and Pkcs7.unpad(8n, m) take any block size.
12#
13# The block layer works on lists of blocks: chaining one call's last
14# ciphertext block into the next call's IV encrypts a long message in pieces.
15# The byte layer takes Octets of whole blocks.
16import Base
17import bend-osdev-bytes@0.1.0.0/bytes.bend as B
18import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
19
20# Block lists, structurally (the forms the proofs reason about)
21
22def m64.ecb(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
23  match bs:
24    case Nil{}:
25      Nil{}
26    case Con{b, t}:
27      Con{f(k, b), m64.ecb(~K, ~f, k, t)}
28
29# C_1 = E(P_1 xor IV), C_j = E(P_j xor C_(j-1))
30def m64.cbc.enc(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, iv: L.LcBlock64) -> List<&2, L.LcBlock64>:
31  match bs:
32    case Nil{}:
33      Nil{}
34    case Con{p, t}:
35      +c = enc(k, L.LcBlock64.xor(iv, p))
36      Con{c, m64.cbc.enc(~K, ~enc, k, t, c)}
37
38# P_1 = D(C_1) xor IV, P_j = D(C_j) xor C_(j-1)
39def m64.cbc.dec(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, iv: L.LcBlock64) -> List<&2, L.LcBlock64>:
40  match bs:
41    case Nil{}:
42      Nil{}
43    case Con{+c, t}:
44      Con{L.LcBlock64.xor(iv, dec(k, c)), m64.cbc.dec(~K, ~dec, k, t, c)}
45
46# The same, tail-recursive (the output so far kept reversed in acc), so a
47# message can be of any length: PROOF.bend proves each equal to its
48# structural form for every input
49
50def m64.rev_onto(bs: List<&2, L.LcBlock64>, acc: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
51  match bs:
52    case Nil{}:
53      acc
54    case Con{b, t}:
55      m64.rev_onto(t, Con{b, acc})
56
57def m64.ecb.go(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, acc: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
58  match bs:
59    case Nil{}:
60      m64.rev_onto(acc, Nil{})
61    case Con{b, t}:
62      m64.ecb.go(~K, ~f, k, t, Con{f(k, b), acc})
63
64def m64.cbc.enc.go(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, iv: L.LcBlock64, acc: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
65  match bs:
66    case Nil{}:
67      m64.rev_onto(acc, Nil{})
68    case Con{p, t}:
69      +c = enc(k, L.LcBlock64.xor(iv, p))
70      m64.cbc.enc.go(~K, ~enc, k, t, c, Con{c, acc})
71
72def m64.cbc.dec.go(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, iv: L.LcBlock64, acc: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
73  match bs:
74    case Nil{}:
75      m64.rev_onto(acc, Nil{})
76    case Con{+c, t}:
77      m64.cbc.dec.go(~K, ~dec, k, t, c, Con{L.LcBlock64.xor(iv, dec(k, c)), acc})
78
79# The block layer
80
81def Lc64.ecb_encrypt_blocks(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
82  m64.ecb.go(~K, ~enc, k, bs, Nil{})
83
84def Lc64.ecb_decrypt_blocks(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
85  m64.ecb.go(~K, ~dec, k, bs, Nil{})
86
87def Lc64.cbc_encrypt_blocks(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, iv: L.LcBlock64, bs: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
88  m64.cbc.enc.go(~K, ~enc, k, bs, iv, Nil{})
89
90def Lc64.cbc_decrypt_blocks(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, iv: L.LcBlock64, bs: List<&2, L.LcBlock64>) -> List<&2, L.LcBlock64>:
91  m64.cbc.dec.go(~K, ~dec, k, bs, iv, Nil{})
92
93# The byte layer
94
95# the bytes as whole blocks (reversed onto acc), or None if bytes are left over
96def m64.split(xs: List<&2, U32>, acc: List<&2, L.LcBlock64>) -> Maybe<&2, List<&2, L.LcBlock64>>:
97  match xs:
98    case Nil{}:
99      Some{m64.rev_onto(acc, Nil{})}
100    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, t}}}}}}}}:
101      m64.split(t, Con{L.lc.block8(a0, a1, a2, a3, a4, a5, a6, a7), acc})
102    case _:
103      None{}
104
105# the bytes of the blocks (reversed) in front of acc
106def m64.join(rs: List<&2, L.LcBlock64>, acc: List<&2, U32>) -> List<&2, U32>:
107  match rs:
108    case Nil{}:
109      acc
110    case Con{b, t}:
111      m64.join(t, L.lc.block_bytes(b, acc))
112
113def m64.octets(bs: List<&2, L.LcBlock64>) -> B.Octets:
114  B.Octets.of_list(m64.join(m64.rev_onto(bs, Nil{}), Nil{}))
115
116def m64.blocks(+n: Nat, m: Maybe<&2, List<&2, L.LcBlock64>>) -> Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>:
117  match m:
118    case None{}:
119      Fail{L.LcNotBlockMultiple{n}}
120    case Some{bs}:
121      Done{bs}
122
123# the message as whole blocks, or LcNotBlockMultiple
124def Lc64.blocks_of(+o: B.Octets) -> Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>:
125  m64.blocks(B.Octets.len(o), m64.split(B.Octets.to_list(o), Nil{}))
126
127# the blocks' bytes, in order
128def Lc64.octets_of(bs: List<&2, L.LcBlock64>) -> B.Octets:
129  m64.octets(bs)
130
131def m64.iv(m: Maybe<&2, L.LcBlock64>, +n: Nat) -> Result<&2, &2, L.LcError, L.LcBlock64>:
132  match m:
133    case None{}:
134      Fail{L.LcBadIvLength{n}}
135    case Some{b}:
136      Done{b}
137
138def Lc64.ecb_encrypt(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, m: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
139  Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, bs => Lc64.octets_of(Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs)), Lc64.blocks_of(m))
140
141def Lc64.ecb_decrypt(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, c: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
142  Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, bs => Lc64.octets_of(Lc64.ecb_decrypt_blocks(~K, ~dec, k, bs)), Lc64.blocks_of(c))
143
144def m64.cbc.e2(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, v: L.LcBlock64, r: Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>) -> Result<&2, &2, L.LcError, B.Octets>:
145  match r:
146    case Fail{e}:
147      Fail{e}
148    case Done{bs}:
149      Done{Lc64.octets_of(Lc64.cbc_encrypt_blocks(~K, ~enc, k, v, bs))}
150
151def m64.cbc.e1(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, r: Result<&2, &2, L.LcError, L.LcBlock64>, +m: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
152  match r:
153    case Fail{e}:
154      Fail{e}
155    case Done{v}:
156      m64.cbc.e2(~K, ~enc, k, v, Lc64.blocks_of(m))
157
158def m64.cbc.d2(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, v: L.LcBlock64, r: Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>) -> Result<&2, &2, L.LcError, B.Octets>:
159  match r:
160    case Fail{e}:
161      Fail{e}
162    case Done{bs}:
163      Done{Lc64.octets_of(Lc64.cbc_decrypt_blocks(~K, ~dec, k, v, bs))}
164
165def m64.cbc.d1(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, r: Result<&2, &2, L.LcError, L.LcBlock64>, +c: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
166  match r:
167    case Fail{e}:
168      Fail{e}
169    case Done{v}:
170      m64.cbc.d2(~K, ~dec, k, v, Lc64.blocks_of(c))
171
172# m (whole blocks) under the 8-byte iv
173def Lc64.cbc_encrypt(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +iv: B.Octets, +m: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
174  m64.cbc.e1(~K, ~enc, k, m64.iv(L.LcBlock64.of_octets(iv), B.Octets.len(iv)), m)
175
176def Lc64.cbc_decrypt(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +iv: B.Octets, +c: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
177  m64.cbc.d1(~K, ~dec, k, m64.iv(L.LcBlock64.of_octets(iv), B.Octets.len(iv)), c)