cbc.bend

bend-osdev-cbc@0.1.0.0 · 163 lines · 23 definitions

1# CBC, cipher block chaining (NIST SP 800-38A, section 6.2), over any 128-bit
2# block cipher (see mode-core.bend for the template arguments):
3#   C_1 = E(P_1 xor IV),  C_j = E(P_j xor C_(j-1))
4#   P_1 = D(C_1) xor IV,  P_j = D(C_j) xor C_(j-1)
5# The block layer (encrypt_blocks, decrypt_blocks) works on lists of blocks;
6# chaining one call's last ciphertext block into the next call's IV encrypts a
7# long message in pieces. The byte layer takes Octets: a whole number of
8# blocks, or any length with PKCS #7 padding (pkcs7.bend).
9import Base
10import bend-osdev-bytes@0.1.1.0/bytes.bend as B
11import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
12import bend-osdev-pkcs7@0.1.0.0/pkcs7.bend as P
13
14# The block layer
15
16def cbc.enc(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>:
17  match bs:
18    case Nil{}:
19      Nil{}
20    case Con{p, t}:
21      +c = enc(k, M.CmBlock.xor(iv, p))
22      Con{c, cbc.enc(~K, ~enc, k, t, c)}
23
24def cbc.dec(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>:
25  match bs:
26    case Nil{}:
27      Nil{}
28    case Con{+c, t}:
29      Con{M.CmBlock.xor(iv, dec(k, c)), cbc.dec(~K, ~dec, k, t, c)}
30
31# The same, tail-recursive (the ciphertext so far kept reversed in acc), so a
32# message can be of any length: PROOF.bend proves each equal to its structural
33# form above for every input
34
35def cbc.enc.go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock, acc: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
36  match bs:
37    case Nil{}:
38      M.cm.blocks.rev_onto(acc, Nil{})
39    case Con{p, t}:
40      +c = enc(k, M.CmBlock.xor(iv, p))
41      cbc.enc.go(~K, ~enc, k, t, c, Con{c, acc})
42
43def cbc.enc.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>:
44  cbc.enc.go(~K, ~enc, k, bs, iv, Nil{})
45
46def cbc.dec.go(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock, acc: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
47  match bs:
48    case Nil{}:
49      M.cm.blocks.rev_onto(acc, Nil{})
50    case Con{+c, t}:
51      cbc.dec.go(~K, ~dec, k, t, c, Con{M.CmBlock.xor(iv, dec(k, c)), acc})
52
53def cbc.dec.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, iv: M.CmBlock) -> List<&2, M.CmBlock>:
54  cbc.dec.go(~K, ~dec, k, bs, iv, Nil{})
55
56def Cbc.encrypt_blocks(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: M.CmBlock, bs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
57  cbc.enc.fast(~K, ~enc, k, bs, iv)
58
59def Cbc.decrypt_blocks(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: M.CmBlock, bs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
60  cbc.dec.fast(~K, ~dec, k, bs, iv)
61
62# The byte layer
63
64def cbc.iv(o: B.Octets) -> Result<&2, &2, M.CmError, M.CmBlock>:
65  +xs = B.Octets.to_list(o)
66  M.cm.need_block(xs, M.CmBadIvLength{B.len(xs)})
67
68# the whole blocks under v, or CmNotBlockMultiple(n) if bytes are left over
69def cbc.e2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
70  match s:
71    case M.CmSplit{bs, tail}:
72      match tail:
73        case Nil{}:
74          Done{B.Octets.of_list(M.cm.join(cbc.enc(~K, ~enc, k, bs, v)))}
75        case Con{h, t}:
76          Fail{M.CmNotBlockMultiple{n}}
77
78def cbc.e1(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
79  match r:
80    case Fail{e}:
81      Fail{e}
82    case Done{v}:
83      cbc.e2(~K, ~enc, k, v, M.cm.split(xs), B.len(xs))
84
85def cbc.d2(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
86  match s:
87    case M.CmSplit{bs, tail}:
88      match tail:
89        case Nil{}:
90          Done{B.Octets.of_list(M.cm.join(cbc.dec(~K, ~dec, k, bs, v)))}
91        case Con{h, t}:
92          Fail{M.CmNotBlockMultiple{n}}
93
94def cbc.d1(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
95  match r:
96    case Fail{e}:
97      Fail{e}
98    case Done{v}:
99      cbc.d2(~K, ~dec, k, v, M.cm.split(xs), B.len(xs))
100
101# m (a whole number of blocks) under the 16-byte iv
102# The byte layer, tail-recursive: what Cbc.encrypt and Cbc.decrypt run
103# (cbc.e1 .. cbc.d2 are the structural forms; PROOF.bend: cbcp.e1_eq, d1_eq)
104
105def cbc.e2.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
106  match s:
107    case M.CmSplit{bs, tail}:
108      match tail:
109        case Nil{}:
110          Done{B.Octets.of_list(M.cm.join_onto.fast(cbc.enc.fast(~K, ~enc, k, bs, v), Nil{}))}
111        case Con{h, t}:
112          Fail{M.CmNotBlockMultiple{n}}
113
114def cbc.e1.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
115  match r:
116    case Fail{e}:
117      Fail{e}
118    case Done{v}:
119      cbc.e2.fast(~K, ~enc, k, v, M.cm.split.fast(xs), B.len.fast(xs))
120
121def cbc.d2.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, v: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
122  match s:
123    case M.CmSplit{bs, tail}:
124      match tail:
125        case Nil{}:
126          Done{B.Octets.of_list(M.cm.join_onto.fast(cbc.dec.fast(~K, ~dec, k, bs, v), Nil{}))}
127        case Con{h, t}:
128          Fail{M.CmNotBlockMultiple{n}}
129
130def cbc.d1.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
131  match r:
132    case Fail{e}:
133      Fail{e}
134    case Done{v}:
135      cbc.d2.fast(~K, ~dec, k, v, M.cm.split.fast(xs), B.len.fast(xs))
136
137# Cbc.encrypt and Cbc.decrypt through the structural forms (the laws' proofs
138# reason about these; PROOF.bend proves them equal to the public defs)
139def Cbc.encrypt.ref(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
140  cbc.e1(~K, ~enc, k, cbc.iv(iv), B.Octets.to_list(m))
141
142def Cbc.decrypt.ref(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
143  cbc.d1(~K, ~dec, k, cbc.iv(iv), B.Octets.to_list(c))
144
145def Cbc.encrypt(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
146  cbc.e1.fast(~K, ~enc, k, cbc.iv(iv), B.Octets.to_list(m))
147
148def Cbc.decrypt(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
149  cbc.d1.fast(~K, ~dec, k, cbc.iv(iv), B.Octets.to_list(c))
150
151# m of any length, PKCS #7 padded to whole blocks, then encrypted
152def Cbc.encrypt_padded(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
153  do Result<&2, &2, M.CmError, B.Octets>:
154    padded : B.Octets <- P.Pkcs7.pad(16n, m)
155    Cbc.encrypt(~K, ~enc, k, iv, padded)
156
157# decrypted, then the padding checked and removed (CmBadPadding)
158def Cbc.decrypt_padded(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, iv: B.Octets, +c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
159  +n = B.Octets.len(c)
160  do Result<&2, &2, M.CmError, B.Octets>:
161    M.cm.check(Nat.is_lt(0n, n), M.CmTooShort{n})
162    padded : B.Octets <- Cbc.decrypt(~K, ~dec, k, iv, c)
163    P.Pkcs7.unpad(16n, padded)