cts.bend

bend-osdev-crypto@0.1.0.0 · 103 lines · 9 definitions

1# CBC with ciphertext stealing over any block cipher (the block-cipher
2# interface, block.bend), in the variant CBC-CS3 of NIST SP 800-38A
3# Addendum, "Three Variants of Ciphertext Stealing for CBC Mode" (2010), the
4# one Kerberos 5 (RFC 3962) and the Linux kernel's "cts" use: a message of
5# at least one block, of any length, gives a ciphertext of the same length.
6#
7# For a message of exactly one block: C = E(P xor IV) (plain CBC). Longer,
8# with the message cut into P_1 .. P_(n-1) whole blocks and a last piece
9# P_n* of d bytes (1 to b, the block size b):
10#   C_1 .. C_(n-1) = CBC of P_1 .. P_(n-1) from the IV
11#   C_n = E((P_n* || 0^(b-d)) xor C_(n-1))
12#   the ciphertext: C_1 .. C_(n-2), C_n, the first d bytes of C_(n-1)
13# (CS3 swaps the last two blocks always, even when d = b). Decryption reads
14# C_n, recovers C_(n-1) from its first d bytes and the last b - d bytes of
15# D(C_n), and P_n* as the first d bytes of D(C_n) xor C_(n-1).
16#
17# The cipher works on bytes here (a block the format refuses stays as it
18# is). A message shorter than a block is refused (CrTooShort), and so is an
19# IV that is not one block (CrBadIvLength).
20import Base
21import bend-osdev-bytes@0.1.0.0/bytes.bend as B
22import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
23import bend-osdev-crypto@0.1.0.0/octets.bend as O
24
25# a block of bytes encrypted or decrypted (f is the cipher's enc or dec)
26def cr.cts.b.go(~K: Data, ~Blk: Data, ~f: K -> Blk -> Blk, ~blk_to: Blk -> B.Octets, +k: K, x: Maybe<&2, Blk>, +o: B.Octets) -> B.Octets:
27  match x:
28    case None{}:
29      o
30    case Some{b}:
31      blk_to(f(k, b))
32
33def cr.cts.b(~K: Data, ~Blk: Data, ~f: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, +o: B.Octets) -> B.Octets:
34  cr.cts.b.go(~K, ~Blk, ~f, ~blk_to, k, blk_of(o), o)
35
36# the pieces in order, as byte strings, onto acc
37def cr.cts.rcat(xs: List<&2, B.Octets>, acc: List<&2, B.Octets>) -> List<&2, B.Octets>:
38  match xs:
39    case Nil{}:
40      acc
41    case Con{h, t}:
42      cr.cts.rcat(t, Con{h, acc})
43
44def cr.cts.out(acc: List<&2, B.Octets>) -> B.Octets:
45  B.Octets.concat(cr.cts.rcat(acc, Nil{}))
46
47# Encryption over the pieces (at least two; the last 1 to b bytes) from the
48# chaining value v; acc holds the ciphertext so far, last first
49def cr.cts.enc.go(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ps: List<&2, List<&2, U32>>, +k: K, +v: B.Octets, acc: List<&2, B.Octets>) -> B.Octets:
50  match ps:
51    case Con{p, t}:
52      match t:
53        case Con{q, u}:
54          match u:
55            case Nil{}:
56              +x = cr.cts.b(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.xor(B.Octets.of_list(p), v))
57              +last = B.Octets.of_list(q)
58              +d = B.Octets.len(last)
59              +cn = cr.cts.b(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.xor(B.Octets.append(last, B.Octets.zeros(Nat.sub(bsize, d))), x))
60              cr.cts.out(Con{B.Octets.take(d, x), Con{cn, acc}})
61            case Con{r, w}:
62              +c = cr.cts.b(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.xor(B.Octets.of_list(p), v))
63              cr.cts.enc.go(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, Con{q, Con{r, w}}, k, c, Con{c, acc})
64        case Nil{}:
65          cr.cts.out(Con{cr.cts.b(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.xor(B.Octets.of_list(p), v)), acc})
66    case Nil{}:
67      cr.cts.out(acc)
68
69# Decryption over the pieces from the chaining value v
70def cr.cts.dec.go(~K: Data, ~Blk: Data, ~bsize: Nat, ~dec: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ps: List<&2, List<&2, U32>>, +k: K, +v: B.Octets, acc: List<&2, B.Octets>) -> B.Octets:
71  match ps:
72    case Con{p, t}:
73      match t:
74        case Con{q, u}:
75          match u:
76            case Nil{}:
77              +cn = B.Octets.of_list(p)
78              +xs = B.Octets.of_list(q)
79              +d = B.Octets.len(xs)
80              +z = cr.cts.b(~K, ~Blk, ~dec, ~blk_of, ~blk_to, k, cn)
81              +x = B.Octets.append(xs, B.Octets.drop(d, z))
82              +pn = O.CrOct.xor(B.Octets.take(d, z), xs)
83              cr.cts.out(Con{pn, Con{O.CrOct.xor(cr.cts.b(~K, ~Blk, ~dec, ~blk_of, ~blk_to, k, x), v), acc}})
84            case Con{r, w}:
85              +c = B.Octets.of_list(p)
86              cr.cts.dec.go(~K, ~Blk, ~bsize, ~dec, ~blk_of, ~blk_to, Con{q, Con{r, w}}, k, c, Con{O.CrOct.xor(cr.cts.b(~K, ~Blk, ~dec, ~blk_of, ~blk_to, k, c), v), acc})
87        case Nil{}:
88          cr.cts.out(Con{O.CrOct.xor(cr.cts.b(~K, ~Blk, ~dec, ~blk_of, ~blk_to, k, B.Octets.of_list(p)), v), acc})
89    case Nil{}:
90      cr.cts.out(acc)
91
92def cr.cts.check(+bsize: Nat, +iv: B.Octets, +n: Nat) -> Result<&2, &2, Cr.CrError, Unit>:
93  do Result<&2, &2, Cr.CrError, Unit>:
94    Cr.CrError.check(Nat.is_eq(B.Octets.len(iv), bsize), Cr.CrBadIvLength{B.Octets.len(iv)})
95    Cr.CrError.check(Bool.and(Nat.is_lt(0n, bsize), Nat.is_le(bsize, n)), Cr.CrTooShort{n})
96
97# CBC-CS3 encryption of m (at least one block) under a one-block IV
98def CrCts.encrypt(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, +iv: B.Octets, +m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
99  Result.map(&2, &2, Cr.CrError, Unit, B.Octets, u => cr.cts.enc.go(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, O.CrOct.pieces(bsize, B.Octets.to_list(m)), k, iv, Nil{}), cr.cts.check(bsize, iv, B.Octets.len(m)))
100
101# CBC-CS3 decryption
102def CrCts.decrypt(~K: Data, ~Blk: Data, ~bsize: Nat, ~dec: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, +iv: B.Octets, +c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
103  Result.map(&2, &2, Cr.CrError, Unit, B.Octets, u => cr.cts.dec.go(~K, ~Blk, ~bsize, ~dec, ~blk_of, ~blk_to, O.CrOct.pieces(bsize, B.Octets.to_list(c)), k, iv, Nil{}), cr.cts.check(bsize, iv, B.Octets.len(c)))