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

Copyright | (c) Austin Seipp
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Examples.Crypto.RC4

Contents

- Types
- The PRGA
- Key schedule
- Encryption and Decryption
- Verification

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

- type S = STree Word8 Word8
- initS :: S
- type Key = [SWord8]
- type RC4 = (S, SWord8, SWord8)
- swap :: SWord8 -> SWord8 -> S -> S
- prga :: RC4 -> (SWord8, RC4)
- initRC4 :: Key -> S
- keySchedule :: Key -> [SWord8]
- keyScheduleString :: String -> [SWord8]
- encrypt :: String -> String -> [SWord8]
- decrypt :: String -> [SWord8] -> String
- rc4IsCorrect :: IO ThmResult

# Types

type S = STree Word8 Word8 Source #

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.

initS :: S Source #

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

initRC4 :: Key -> S Source #

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.

keyScheduleString :: String -> [SWord8] Source #

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 hex $ encrypt "Key" "Plaintext"
    "bbf316e8d940af0ad3"

    >>> concatMap hex $ encrypt "Wiki" "pedia"
    "1021bf0420"

    >>> concatMap hex $ 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

rc4IsCorrect :: IO ThmResult Source #

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.