lrw.bend

bend-osdev-crypto@0.1.0.0 · 151 lines · 18 definitions

1# LRW over any 128-bit block cipher (the block-cipher interface, block.bend):
2# the tweakable block cipher of M. Liskov, R. Rivest, D. Wagner, "Tweakable
3# Block Ciphers" (CRYPTO 2002), theorem 2, as the IEEE P1619 draft proposal
4# "Tweakable Narrow-block Encryption" (draft 1.00, October 2004) specifies
5# LRW-AES for storage: a key pair (Key1, the cipher's key; Key2, a 16-byte
6# tweak key), and for the block at logical index I
7#   T = Key2 (x) I,  C = E(Key1, P xor T) xor T,  P = D(Key1, C xor T) xor T
8# with (x) the product in GF(2^128) modulo x^128 + x^7 + x^2 + x + 1 on
9# 16-byte big-endian numbers (bend-osdev-gf's Gf128.mul_be) and I a 16-byte
10# big-endian number (draft section 6.1). Consecutive blocks have consecutive
11# indices. The key is Key1 followed by Key2 (the Linux kernel's "lrw"
12# layout); the IV is the index of the first block.
13#
14# A tweak is made a block through the cipher's block format (~blk_of); a
15# format that refused 16 bytes would leave the block untweaked, in both
16# directions, so decryption undoes encryption whatever the format, for every
17# key, tweak key, index and list of blocks wherever the cipher's decryption
18# undoes its encryption: a law per 128-bit instance (gen/instances.py,
19# <c>_lrw_round_trip).
20import Base
21import bend-osdev-bytes@0.1.0.0/bytes.bend as B
22import bend-osdev-gf@0.1.0.0/gf128.bend as G
23import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
24import bend-osdev-crypto@0.1.0.0/modes.bend as Md
25
26# the tweak of index i under the tweak key k2, as a block
27def cr.lrw.tweak(~Blk: Data, ~blk_of: B.Octets -> Maybe<&2, Blk>, +k2: G.Gf128, i: G.Gf128) -> Maybe<&2, Blk>:
28  blk_of(G.Gf128.to_octets(G.Gf128.mul_be(k2, i)))
29
30# one block under a tweak
31def cr.lrw.benc(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, t: Maybe<&2, Blk>, p: Blk) -> Blk:
32  match t:
33    case None{}:
34      enc(k, p)
35    case Some{+x}:
36      bxor(enc(k, bxor(p, x)), x)
37
38def cr.lrw.bdec(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, t: Maybe<&2, Blk>, c: Blk) -> Blk:
39  match t:
40    case None{}:
41      dec(k, c)
42    case Some{+x}:
43      bxor(dec(k, bxor(c, x)), x)
44
45def cr.lrw.carry(z: Bool, +w: U32) -> U32:
46  match z:
47    case True{}:
48      U32.add(w, 1)
49    case False{}:
50      w
51
52# i + 1, modulo 2^128
53def cr.lrw.inc(i: G.Gf128) -> G.Gf128:
54  match i:
55    case G.Gf128{w0, w1, w2, w3}:
56      +a3 = U32.add(w3, 1)
57      +c3 = U32.is_eq(a3, 0)
58      +a2 = cr.lrw.carry(c3, w2)
59      +c2 = Bool.and(c3, U32.is_eq(a2, 0))
60      +a1 = cr.lrw.carry(c2, w1)
61      +c1 = Bool.and(c2, U32.is_eq(a1, 0))
62      G.Gf128{cr.lrw.carry(c1, w0), a1, a2, a3}
63
64# Structural forms (the proofs' reference): the blocks from index i
65
66def cr.lrw.enc(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, +k: K, +k2: G.Gf128, bs: List<&2, Blk>, +i: G.Gf128) -> List<&2, Blk>:
67  match bs:
68    case Nil{}:
69      Nil{}
70    case Con{p, t}:
71      Con{cr.lrw.benc(~K, ~Blk, ~enc, ~bxor, k, cr.lrw.tweak(~Blk, ~blk_of, k2, i), p), cr.lrw.enc(~K, ~Blk, ~enc, ~bxor, ~blk_of, k, k2, t, cr.lrw.inc(i))}
72
73def cr.lrw.dec(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, +k: K, +k2: G.Gf128, bs: List<&2, Blk>, +i: G.Gf128) -> List<&2, Blk>:
74  match bs:
75    case Nil{}:
76      Nil{}
77    case Con{c, t}:
78      Con{cr.lrw.bdec(~K, ~Blk, ~dec, ~bxor, k, cr.lrw.tweak(~Blk, ~blk_of, k2, i), c), cr.lrw.dec(~K, ~Blk, ~dec, ~bxor, ~blk_of, k, k2, t, cr.lrw.inc(i))}
79
80# The loops that run
81
82def cr.lrw.enc.go(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, +k: K, +k2: G.Gf128, bs: List<&2, Blk>, +i: G.Gf128, acc: List<&2, Blk>) -> List<&2, Blk>:
83  match bs:
84    case Nil{}:
85      Md.cr.blks.rev_onto(~Blk, acc, Nil{})
86    case Con{p, t}:
87      cr.lrw.enc.go(~K, ~Blk, ~enc, ~bxor, ~blk_of, k, k2, t, cr.lrw.inc(i), Con{cr.lrw.benc(~K, ~Blk, ~enc, ~bxor, k, cr.lrw.tweak(~Blk, ~blk_of, k2, i), p), acc})
88
89def cr.lrw.dec.go(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, +k: K, +k2: G.Gf128, bs: List<&2, Blk>, +i: G.Gf128, acc: List<&2, Blk>) -> List<&2, Blk>:
90  match bs:
91    case Nil{}:
92      Md.cr.blks.rev_onto(~Blk, acc, Nil{})
93    case Con{c, t}:
94      cr.lrw.dec.go(~K, ~Blk, ~dec, ~bxor, ~blk_of, k, k2, t, cr.lrw.inc(i), Con{cr.lrw.bdec(~K, ~Blk, ~dec, ~bxor, k, cr.lrw.tweak(~Blk, ~blk_of, k2, i), c), acc})
95
96# LRW on blocks: key k, tweak key k2, the first block's index i (the next
97# call's index is i plus the number of blocks)
98def CrLrw.encrypt_blocks(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, +k: K, +k2: G.Gf128, +i: G.Gf128, bs: List<&2, Blk>) -> List<&2, Blk>:
99  cr.lrw.enc.go(~K, ~Blk, ~enc, ~bxor, ~blk_of, k, k2, bs, i, Nil{})
100
101def CrLrw.decrypt_blocks(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, +k: K, +k2: G.Gf128, +i: G.Gf128, bs: List<&2, Blk>) -> List<&2, Blk>:
102  cr.lrw.dec.go(~K, ~Blk, ~dec, ~bxor, ~blk_of, k, k2, bs, i, Nil{})
103
104# The key pair: the cipher's key schedule and the tweak key
105type CrLrwKey<-K: Data> is Data:
106  CrLrwKey{k: K, t: G.Gf128}
107
108def cr.lrw.gf(+n: Nat, r: Result<&2, &2, G.Gf128Error, G.Gf128>) -> Result<&2, &2, Cr.CrError, G.Gf128>:
109  match r:
110    case Fail{e}:
111      Fail{Cr.CrBadKeyLength{n}}
112    case Done{x}:
113      Done{x}
114
115# a raw key: the cipher's key followed by the 16-byte tweak key
116# (CrBadKeyLength for a key of 16 bytes or fewer, or one the cipher refuses)
117def CrLrw.key(~K: Data, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, +o: B.Octets) -> Result<&2, &2, Cr.CrError, CrLrwKey<K>>:
118  +n = B.Octets.len(o)
119  do Result<&2, &2, Cr.CrError, CrLrwKey<K>>:
120    Cr.CrError.check(Nat.is_lt(16n, n), Cr.CrBadKeyLength{n})
121    k : K <- key(B.Octets.take(Nat.sub(n, 16n), o))
122    t : G.Gf128 <- cr.lrw.gf(n, G.Gf128.of_octets(B.Octets.drop(Nat.sub(n, 16n), o)))
123    return CrLrwKey{k, t}
124
125def cr.lrw.index.of(+n: Nat, r: Result<&2, &2, G.Gf128Error, G.Gf128>) -> Result<&2, &2, Cr.CrError, G.Gf128>:
126  match r:
127    case Fail{e}:
128      Fail{Cr.CrBadIvLength{n}}
129    case Done{x}:
130      Done{x}
131
132def cr.lrw.index(+iv: B.Octets) -> Result<&2, &2, Cr.CrError, G.Gf128>:
133  cr.lrw.index.of(B.Octets.len(iv), G.Gf128.of_octets(iv))
134
135# LRW on bytes: a message of whole blocks; the IV is the first block's
136# 16-byte big-endian index (CrBadIvLength, CrNotBlockMultiple otherwise)
137def CrLrw.encrypt(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, kk: CrLrwKey<K>, +iv: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
138  match kk:
139    case CrLrwKey{+k, +k2}:
140      do Result<&2, &2, Cr.CrError, B.Octets>:
141        i : G.Gf128 <- cr.lrw.index(iv)
142        bs : List<&2, Blk> <- Md.CrModes.blocks_of(~Blk, ~bsize, ~blk_of, m)
143        return Md.CrModes.octets_of(~Blk, ~blk_to, CrLrw.encrypt_blocks(~K, ~Blk, ~enc, ~bxor, ~blk_of, k, k2, i, bs))
144
145def CrLrw.decrypt(~K: Data, ~Blk: Data, ~bsize: Nat, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, kk: CrLrwKey<K>, +iv: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
146  match kk:
147    case CrLrwKey{+k, +k2}:
148      do Result<&2, &2, Cr.CrError, B.Octets>:
149        i : G.Gf128 <- cr.lrw.index(iv)
150        bs : List<&2, Blk> <- Md.CrModes.blocks_of(~Blk, ~bsize, ~blk_of, c)
151        return Md.CrModes.octets_of(~Blk, ~blk_to, CrLrw.decrypt_blocks(~K, ~Blk, ~dec, ~bxor, ~blk_of, k, k2, i, bs))