inst_rc4.bend

bend-osdev-crypto@0.1.0.0 · 27 lines · 3 definitions

1# RC4 as a stream cipher: legacy-ciphers' RC4 (RFC 6229's description), and
2# RC4-drop[n] (RFC 4345). RC4 is broken (RFC 7465 forbids it in TLS): it is
3# here to read and write what already uses it. The instance:
4#   ~R.LcRc4State, ~R.LcRc4Out, ~CrRc4.start, ~R.LcRc4.update,
5#   ~R.LcRc4.out_state, ~R.LcRc4.out_data
6# and with the first n keystream bytes dropped, ~CrRc4.start_drop(~n) in
7# place of ~CrRc4.start.
8import Base
9import bend-osdev-bytes@0.1.0.0/bytes.bend as B
10import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
11import bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend as R
12import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
13import bend-osdev-crypto@0.1.0.0/inst_lc.bend as LC
14
15def cr.rc4.start(+n: Nat, r: Result<&2, &2, L.LcError, R.LcRc4State>) -> Result<&2, &2, Cr.CrError, R.LcRc4State>:
16  do Result<&2, &2, Cr.CrError, R.LcRc4State>:
17    Cr.CrError.check(Nat.is_eq(n, 0n), Cr.CrBadIvLength{n})
18    LC.CrLc.lift(~R.LcRc4State, r)
19
20# the state for a key of 1 to 256 bytes (CrBadKeyLength otherwise); RC4 has
21# no IV, so the IV must be empty (CrBadIvLength otherwise)
22def CrRc4.start(key: B.Octets, iv: B.Octets) -> Result<&2, &2, Cr.CrError, R.LcRc4State>:
23  cr.rc4.start(B.Octets.len(iv), R.LcRc4.start(key))
24
25# the same, with the first n keystream bytes dropped (RC4-drop[n])
26def CrRc4.start_drop(~n: Nat, key: B.Octets, iv: B.Octets) -> Result<&2, &2, Cr.CrError, R.LcRc4State>:
27  cr.rc4.start(B.Octets.len(iv), R.LcRc4.start_drop(key, n))