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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Crypto.Prince

Contents

- Types
- Key expansion
- Main algorithm
- Round constants
- Test vectors
- Code generation

Description

Implementation of Prince encryption and decrytion, following the spec https://eprint.iacr.org/2012/529.pdf

Synopsis

- type Block = SWord 64
- type PT = Block
- type Key = Block
- type CT = Block
- type Nibble = SWord 8
- expandKey :: Key -> Key
- prop_ExpandKey :: IO ()
- encrypt :: PT -> Key -> Key -> CT
- decrypt :: CT -> Key -> Key -> PT
- prince :: Block -> Key -> Key -> Key -> Block
- princeCore :: Key -> Block -> Block
- round :: Key -> Block -> Int -> Block
- invRound :: Key -> Block -> Int -> Block
- m :: Block -> Block
- mInv :: Block -> Block
- sr :: Block -> Block
- srInv :: Block -> Block
- prop_sr :: Predicate
- m' :: Block -> Block
- mat :: [[Int]]
- mMult :: Block -> Block
- nonLinear :: [Nibble] -> Nibble -> Block -> Block
- sBox :: Block -> Block
- sBoxInv :: Block -> Block
- prop_SBox :: Predicate
- rConstants :: Int -> SWord 64
- prop_RoundKeys :: SBool
- toNibbles :: SWord 64 -> [Nibble]
- fromNibbles :: [Nibble] -> SWord 64
- testVectors :: SBool
- showBlock :: Block -> String
- codeGen :: IO ()

# Documentation

    >>> -- For doctest purposes only:
    >>> import Data.SBV

# Types

type Block = SWord 64 Source #

Section 2: Prince is essentially a 64-bit cipher, with 128-bit key, coming in two parts.

type PT = Block Source #

Plantext is simply a block.

type Key = Block Source #

Key is again a 64-bit block.

type CT = Block Source #

Cypher text is another 64-bit block.

type Nibble = SWord 8 Source #

A nibble is 4-bits. Ideally, we would like to represent a nibble by `SWord 4`; and indeed SBV can do that for verification purposes just fine. Unfortunately, the SBV's C compiler doesn't support 4-bit bit-vectors, as there's nothing meaningful in the C-land that we can map it to. Thus, we represent a nibble with 8-bits. The top 4 bits will always be 0.

# Key expansion

expandKey :: Key -> Key Source #

Expanding a key, from Section 3.4 of the spec.

prop_ExpandKey :: IO () Source #

expandKey(x) = x has a unique solution. We have:

    >>> prop_ExpandKey
    Q.E.D.

encrypt :: PT -> Key -> Key -> CT Source #

Section 2: Encryption

decrypt :: CT -> Key -> Key -> PT Source #

Decryption

# Main algorithm

prince :: Block -> Key -> Key -> Key -> Block Source #

Basic prince algorithm

princeCore :: Key -> Block -> Block Source #

Core prince. It's essentially folding of 12 rounds stitched together:

round :: Key -> Block -> Int -> Block Source #

Forward round.

invRound :: Key -> Block -> Int -> Block Source #

Backend round.

m :: Block -> Block Source #

M transformation.

mInv :: Block -> Block Source #

Inverse of M.

sr :: Block -> Block Source #

SR.

srInv :: Block -> Block Source #

Inverse of SR:

prop_sr :: Predicate Source #

Prove sr and srInv are inverses: We have:

    >>> prove prop_sr
    Q.E.D.

m' :: Block -> Block Source #

M' transformation

mat :: [[Int]] Source #

The matrix as described in Section 3.3

mMult :: Block -> Block Source #

Multiplication.

nonLinear :: [Nibble] -> Nibble -> Block -> Block Source #

Non-linear transformation of a block

sBox :: Block -> Block Source #

SBox transformation.

sBoxInv :: Block -> Block Source #

Inverse SBox transformation.

prop_SBox :: Predicate Source #

Prove that sbox and sBoxInv are inverses: We have:

    >>> prove prop_SBox
    Q.E.D.

# Round constants

rConstants :: Int -> SWord 64 Source #

Round constants

prop_RoundKeys :: SBool Source #

Round-constants property: rc_i `xor` rc_{11-i} is constant. We have:

    >>> prop_RoundKeys
    True

toNibbles :: SWord 64 -> [Nibble] Source #

Convert a 64 bit word to nibbles

fromNibbles :: [Nibble] -> SWord 64 Source #

Convert from nibbles to a 64 bit word

# Test vectors

testVectors :: SBool Source #

From Appendix A of the spec. We have:

    >>> testVectors
    True

showBlock :: Block -> String Source #

Nicely show a concrete block.

# Code generation

codeGen :: IO () Source #

Generating C code for the encryption block.