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).
16	import Base
17	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
18	import ./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
23	def 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	
30	def 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	
45	def 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	
60	def 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
64	def 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
70	def 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
78	type 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]
83	def 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
92	type 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]]
96	def 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	
104	def rc4.step.st(r: LcRc4Step) -> LcRc4State:
105	  match r:
106	    case LcRc4Step{st, k}:
107	      st
108	
109	def 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	
117	def 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	
125	def 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.
134	type 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	
140	def 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	
147	type LcRc4Run is Data:
148	  LcRc4Run{st: LcRc4State, out: List<&2, U32>}
149	
150	def 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	
158	def 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
164	def 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	
171	def 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
181	def 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)
188	def 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
192	def LcRc4.update(st: LcRc4State, m: B.Octets) -> LcRc4Out:
193	  rc4.out(rc4.go(B.Octets.to_list(m), st, Nil{}))
194	
195	def LcRc4.out_state(o: LcRc4Out) -> LcRc4State:
196	  match o:
197	    case LcRc4Out{st, d}:
198	      st
199	
200	def 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
206	def 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
210	def LcRc4.keystream(st: LcRc4State, n: Nat) -> LcRc4Out:
211	  LcRc4.update(st, B.Octets.zeros(n))