rc4.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 211 lines · 28 definitions

1# RC4 (ARC4), the stream cipher, as RFC 6229 ("Test Vectors for the Stream
2# Cipher RC4", 2011) describes it: a key-scheduling algorithm that permutes
3# the 256-byte state S under a key of 1 to 256 bytes, then an output
4# algorithm that yields one keystream byte per step, XORed into the data.
5#
6# RC4 is broken: RFC 7465 (2015) forbids it in TLS, and its keystream is
7# biased. It is here only to read and write data that old formats and
8# protocols already hold (for compatibility); never use it to protect new
9# data.
10#
11# The state (S, i, j) is Data: S is a 256-entry table (a tree read and
12# written by the bits of an index), so the cipher is a pure function of its
13# state and the laws can quantify over states. Data arrives in pieces:
14# LcRc4.update takes the state and a piece and answers the next state and
15# the piece encrypted (or decrypted: it is the same operation).
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# The table S
21
22# the bits of i (below 2^d) that pick its entry, most significant first
23def rc4.path(d: Nat, +i: U32) -> List<&2, Bool>:
24  match d:
25    case 0n:
26      Nil{}
27    case 1n+(+p):
28      Con{U32.is_eq(L.lc.bit(i, p), 1), rc4.path(p, i)}
29
30def rc4.get(t: L.LcTab, path: List<&2, Bool>) -> U32:
31  match t:
32    case L.LcLeaf{v}:
33      v
34    case L.LcNode{l, r}:
35      match path:
36        case Nil{}:
37          0
38        case Con{b, rest}:
39          match b:
40            case True{}:
41              rc4.get(r, rest)
42            case False{}:
43              rc4.get(l, rest)
44
45def rc4.set(t: L.LcTab, path: List<&2, Bool>, v: U32) -> L.LcTab:
46  match t:
47    case L.LcLeaf{w}:
48      L.LcLeaf{v}
49    case L.LcNode{l, r}:
50      match path:
51        case Nil{}:
52          L.LcNode{l, r}
53        case Con{b, rest}:
54          match b:
55            case True{}:
56              L.LcNode{l, rc4.set(r, rest, v)}
57            case False{}:
58              L.LcNode{rc4.set(l, rest, v), r}
59
60def rc4.at(+s: L.LcTab, +i: U32) -> U32:
61  rc4.get(s, rc4.path(8n, i))
62
63# S with entries i and j exchanged
64def rc4.swap(+s: L.LcTab, +i: U32, +j: U32) -> L.LcTab:
65  +a = rc4.at(s, i)
66  +b = rc4.at(s, j)
67  rc4.set(rc4.set(s, rc4.path(8n, i), b), rc4.path(8n, j), a)
68
69# the identity permutation 0 .. 255
70def rc4.ident(n: Nat, +i: U32) -> List<&2, U32>:
71  match n:
72    case 0n:
73      Nil{}
74    case 1n+p:
75      Con{i, rc4.ident(p, U32.add(i, 1))}
76
77# The state (opaque): S, i and j
78type LcRc4State is Data:
79  LcRc4State{s: L.LcTab, i: U32, j: U32}
80
81# The key-scheduling algorithm: for i = 0 .. 255,
82#   j = j + S[i] + key[i mod keylength]; swap S[i] and S[j]
83def rc4.ksa(n: Nat, +key: List<&2, U32>, +klen: Nat, +s: L.LcTab, +i: U32, +j: U32) -> L.LcTab:
84  match n:
85    case 0n:
86      s
87    case 1n+p:
88      +j2 = U32.and(255, U32.add(U32.add(j, rc4.at(s, i)), L.lc.at(key, Nat.mod(U32.to_nat(i), klen))))
89      rc4.ksa(p, key, klen, rc4.swap(s, i, j2), U32.add(i, 1), j2)
90
91# One step of the output algorithm: the next state and keystream byte
92type LcRc4Step is Data:
93  LcRc4Step{st: LcRc4State, k: U32}
94
95#   i = i + 1; j = j + S[i]; swap S[i] and S[j]; the byte S[S[i] + S[j]]
96def rc4.next(st: LcRc4State) -> LcRc4Step:
97  match st:
98    case LcRc4State{+s, i, j}:
99      +i2 = U32.and(255, U32.add(i, 1))
100      +j2 = U32.and(255, U32.add(j, rc4.at(s, i2)))
101      +s2 = rc4.swap(s, i2, j2)
102      LcRc4Step{LcRc4State{s2, i2, j2}, rc4.at(s2, U32.and(255, U32.add(rc4.at(s2, i2), rc4.at(s2, j2))))}
103
104def rc4.step.st(r: LcRc4Step) -> LcRc4State:
105  match r:
106    case LcRc4Step{st, k}:
107      st
108
109def rc4.step.k(r: LcRc4Step) -> U32:
110  match r:
111    case LcRc4Step{st, k}:
112      k
113
114# The data, structurally (the form the proofs reason about): each byte XOR
115# the next keystream byte, and the state after the bytes
116
117def rc4.xs(xs: List<&2, U32>, st: LcRc4State) -> List<&2, U32>:
118  match xs:
119    case Nil{}:
120      Nil{}
121    case Con{x, t}:
122      +n = rc4.next(st)
123      Con{B.byte(U32.xor(x, rc4.step.k(n))), rc4.xs(t, rc4.step.st(n))}
124
125def rc4.after(xs: List<&2, U32>, st: LcRc4State) -> LcRc4State:
126  match xs:
127    case Nil{}:
128      st
129    case Con{x, t}:
130      rc4.after(t, rc4.step.st(rc4.next(st)))
131
132# A piece of data through the cipher: the state after it, and its bytes
133# encrypted (or decrypted). Open: a caller may match it.
134type LcRc4Out is Data:
135  LcRc4Out{state: LcRc4State, data: B.Octets}
136
137# The same, tail-recursive (the output so far kept reversed in acc), so data
138# can be of any length: PROOF.bend proves it equal to the structural form
139
140def rc4.rev_onto(xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
141  match xs:
142    case Nil{}:
143      acc
144    case Con{h, t}:
145      rc4.rev_onto(t, Con{h, acc})
146
147type LcRc4Run is Data:
148  LcRc4Run{st: LcRc4State, out: List<&2, U32>}
149
150def rc4.go(xs: List<&2, U32>, st: LcRc4State, acc: List<&2, U32>) -> LcRc4Run:
151  match xs:
152    case Nil{}:
153      LcRc4Run{st, rc4.rev_onto(acc, Nil{})}
154    case Con{x, t}:
155      +n = rc4.next(st)
156      rc4.go(t, rc4.step.st(n), Con{B.byte(U32.xor(x, rc4.step.k(n))), acc})
157
158def rc4.out(r: LcRc4Run) -> LcRc4Out:
159  match r:
160    case LcRc4Run{st, out}:
161      LcRc4Out{st, B.Octets.of_list(out)}
162
163# drop n keystream bytes
164def rc4.drop(n: Nat, st: LcRc4State) -> LcRc4State:
165  match n:
166    case 0n:
167      st
168    case 1n+p:
169      rc4.drop(p, rc4.step.st(rc4.next(st)))
170
171def rc4.start.pick(ok: Bool, +key: List<&2, U32>, +klen: Nat) -> Result<&2, &2, L.LcError, LcRc4State>:
172  match ok:
173    case True{}:
174      Done{LcRc4State{rc4.ksa(256n, key, klen, L.lc.tab(8n, rc4.ident(256n, 0)), 0, 0), 0, 0}}
175    case False{}:
176      Fail{L.LcBadKeyLength{klen}}
177
178# The cipher
179
180# the state after the key-scheduling algorithm, for a key of 1 to 256 bytes
181def LcRc4.start(key: B.Octets) -> Result<&2, &2, L.LcError, LcRc4State>:
182  +xs = B.Octets.to_list(key)
183  +n = B.len(xs)
184  rc4.start.pick(Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, 256n)), xs, n)
185
186# the state after dropping the first n keystream bytes (RC4-drop[n]; RFC 4345
187# drops 1536 for SSH's arcfour128 and arcfour256)
188def LcRc4.start_drop(key: B.Octets, n: Nat) -> Result<&2, &2, L.LcError, LcRc4State>:
189  Result.map(&2, &2, L.LcError, LcRc4State, LcRc4State, st => rc4.drop(n, st), LcRc4.start(key))
190
191# the next piece of data, encrypted or decrypted, and the state after it
192def LcRc4.update(st: LcRc4State, m: B.Octets) -> LcRc4Out:
193  rc4.out(rc4.go(B.Octets.to_list(m), st, Nil{}))
194
195def LcRc4.out_state(o: LcRc4Out) -> LcRc4State:
196  match o:
197    case LcRc4Out{st, d}:
198      st
199
200def LcRc4.out_data(o: LcRc4Out) -> B.Octets:
201  match o:
202    case LcRc4Out{st, d}:
203      d
204
205# the data under a key, in one call
206def LcRc4.crypt(key: B.Octets, m: B.Octets) -> Result<&2, &2, L.LcError, B.Octets>:
207  Result.map(&2, &2, L.LcError, LcRc4State, B.Octets, st => LcRc4.out_data(LcRc4.update(st, m)), LcRc4.start(key))
208
209# the next n keystream bytes (the data n zero bytes), and the state after them
210def LcRc4.keystream(st: LcRc4State, n: Nat) -> LcRc4Out:
211  LcRc4.update(st, B.Octets.zeros(n))