sbv-8.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright (c) Austin Seipp BSD3 erkokl@gmail.com experimental None Haskell2010

Documentation.SBV.Examples.Crypto.RC4

Description

An implementation of RC4 (AKA Rivest Cipher 4 or Alleged RC4/ARC4), using SBV. For information on RC4, see: http://en.wikipedia.org/wiki/RC4.

We make no effort to optimize the code, and instead focus on a clear implementation. In fact, the RC4 algorithm relies on in-place update of its state heavily for efficiency, and is therefore unsuitable for a purely functional implementation.

Synopsis

Types

RC4 State contains 256 8-bit values. We use the symbolically accessible full-binary type STree to represent the state, since RC4 needs access to the array via a symbolic index and it's important to minimize access time.

Construct the fully balanced initial tree, where the leaves are simply the numbers 0 through 255.

type Key = [SWord8] Source #

The key is a stream of Word8 values.

type RC4 = (S, SWord8, SWord8) Source #

Represents the current state of the RC4 stream: it is the S array along with the i and j index values used by the PRGA.

The PRGA

swap :: SWord8 -> SWord8 -> S -> S Source #

Swaps two elements in the RC4 array.

prga :: RC4 -> (SWord8, RC4) Source #

Implements the PRGA used in RC4. We return the new state and the next key value generated.

Key schedule

Constructs the state to be used by the PRGA using the given key.

keySchedule :: Key -> [SWord8] Source #

The key-schedule. Note that this function returns an infinite list.

Generate a key-schedule from a given key-string.

Encryption and Decryption

encrypt :: String -> String -> [SWord8] Source #

RC4 encryption. We generate key-words and xor it with the input. The following test-vectors are from Wikipedia http://en.wikipedia.org/wiki/RC4:

>>> concatMap hex2 $encrypt "Key" "Plaintext" "bbf316e8d940af0ad3"  >>> concatMap hex2$ encrypt "Wiki" "pedia"
"1021bf0420"

>>> concatMap hex2 \$ encrypt "Secret" "Attack at dawn"
"45a01f645fc35b383552544b9bf5"


decrypt :: String -> [SWord8] -> String Source #

RC4 decryption. Essentially the same as decryption. For the above test vectors we have:

>>> decrypt "Key" [0xbb, 0xf3, 0x16, 0xe8, 0xd9, 0x40, 0xaf, 0x0a, 0xd3]
"Plaintext"

>>> decrypt "Wiki" [0x10, 0x21, 0xbf, 0x04, 0x20]
"pedia"

>>> decrypt "Secret" [0x45, 0xa0, 0x1f, 0x64, 0x5f, 0xc3, 0x5b, 0x38, 0x35, 0x52, 0x54, 0x4b, 0x9b, 0xf5]
"Attack at dawn"


Verification

Prove that round-trip encryption/decryption leaves the plain-text unchanged. The theorem is stated parametrically over key and plain-text sizes. The expression performs the proof for a 40-bit key (5 bytes) and 40-bit plaintext (again 5 bytes).

Note that this theorem is trivial to prove, since it is essentially establishing xor'in the same value twice leaves a word unchanged (i.e., x xor y xor y = x). However, the proof takes quite a while to complete, as it gives rise to a fairly large symbolic trace.

hex2 :: (SymVal a, Show a, Integral a) => SBV a -> String Source #

For doctest purposes only