law rc4_stream_streaming_data

bend-osdev-crypto@0.1.0.0 · LAWS.bend:1163

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend as R

1163# RC4 (legacy-ciphers): the output of a ++ b is the output of a, then of b from the state after a
1164law rc4_stream_streaming_data:
1165  for +s: R.LcRc4State
1166  for +a: B.Octets
1167  for +b: B.Octets
1168  {R.LcRc4.out_data(R.LcRc4.update(s, B.Octets.append(a, b))) == B.Octets.append(R.LcRc4.out_data(R.LcRc4.update(s, a)), R.LcRc4.out_data(R.LcRc4.update(R.LcRc4.out_state(R.LcRc4.update(s, a)), b))) : B.Octets}