-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Crypto.Prince
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Implementation of Prince encryption and decrytion, following the spec
-- <https://eprint.iacr.org/2012/529.pdf>
-----------------------------------------------------------------------------

{-# LANGUAGE CPP              #-}
{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE ParallelListComp #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Documentation.SBV.Examples.Crypto.Prince where

import Prelude hiding(round)
import Numeric

import Data.SBV
import Data.SBV.Tools.CodeGen

#ifndef HADDOCK
-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV
#endif

-- * Types
-- | Section 2: Prince is essentially a 64-bit cipher, with 128-bit key, coming in two parts.
type Block = SWord 64

-- | Plantext is simply a block.
type PT = Block

-- | Key is again a 64-bit block.
type Key = Block

-- | Cypher text is another 64-bit block.
type CT = Block

-- | 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.
type Nibble = SWord 8

-- * Key expansion

-- | Expanding a key, from Section 3.4 of the spec.
expandKey :: Key -> Key
expandKey :: SWord 64 -> SWord 64
expandKey SWord 64
k = (SWord 64
k SWord 64 -> Int -> SWord 64
forall a. Bits a => a -> Int -> a
`rotateR` Int
1) SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` (SWord 64
k SWord 64 -> Int -> SWord 64
forall a. Bits a => a -> Int -> a
`shiftR` Int
63)

-- | expandKey(x) = x has a unique solution. We have:
--
-- >>> prop_ExpandKey
-- Q.E.D.
prop_ExpandKey :: IO ()
prop_ExpandKey :: IO ()
prop_ExpandKey = do let lim :: Int
lim = Int
10
                    ms <- AllSatResult -> [WordN 64]
forall a. SatModel a => AllSatResult -> [a]
extractModels (AllSatResult -> [WordN 64]) -> IO AllSatResult -> IO [WordN 64]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SMTConfig -> (SWord 64 -> SBool) -> IO AllSatResult
forall a. Satisfiable a => SMTConfig -> a -> IO AllSatResult
allSatWith SMTConfig
z3{allSatMaxModelCount = Just lim}
                                                       (\SWord 64
x -> SWord 64
x SWord 64 -> SWord 64 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 64 -> SWord 64
expandKey SWord 64
x)
                    case length ms of
                      Int
0 -> String -> IO ()
putStrLn String
"No solutions to equation `x == expandKey x`!"
                      Int
1 -> String -> IO ()
putStrLn String
"Q.E.D."
                      Int
n -> do let qual :: String
qual = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
lim then String
"at least " else String
""
                              String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Failed. There are " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
qual String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" solutions to `x == expandKey x`!"
                              (WordN 64 -> IO ()) -> [WordN 64] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\WordN 64
i -> String -> IO ()
putStrLn (String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ WordN 64 -> String
forall a. Show a => a -> String
show WordN 64
i)) ([WordN 64]
ms :: [WordN 64])


-- | Section 2: Encryption
encrypt :: PT -> Key -> Key -> CT
encrypt :: SWord 64 -> SWord 64 -> SWord 64 -> SWord 64
encrypt SWord 64
pt SWord 64
k0 SWord 64
k1 = SWord 64 -> SWord 64 -> SWord 64 -> SWord 64 -> SWord 64
prince SWord 64
k0 SWord 64
k0' SWord 64
k1 SWord 64
pt
   where k0' :: SWord 64
k0' = SWord 64 -> SWord 64
expandKey SWord 64
k0

-- | Decryption
decrypt :: CT -> Key -> Key -> PT
decrypt :: SWord 64 -> SWord 64 -> SWord 64 -> SWord 64
decrypt SWord 64
ct SWord 64
k0 SWord 64
k1 = SWord 64 -> SWord 64 -> SWord 64 -> SWord 64 -> SWord 64
prince SWord 64
k0' SWord 64
k0 (SWord 64
k1 SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` SWord 64
alpha) SWord 64
ct
  where k0' :: SWord 64
k0'   = SWord 64 -> SWord 64
expandKey SWord 64
k0
        alpha :: SWord 64
alpha = SWord 64
0xc0ac29b7c97c50dd

-- * Main algorithm

-- | Basic prince algorithm
prince :: Block -> Key -> Key -> Key -> Block
prince :: SWord 64 -> SWord 64 -> SWord 64 -> SWord 64 -> SWord 64
prince SWord 64
k0 SWord 64
k0' SWord 64
k1 SWord 64
inp = SWord 64
out
   where start :: SWord 64
start = SWord 64
inp SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` SWord 64
k0
         end :: SWord 64
end   = SWord 64 -> SWord 64 -> SWord 64
princeCore SWord 64
k1 SWord 64
start
         out :: SWord 64
out   = SWord 64
end SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` SWord 64
k0'

-- | Core prince. It's essentially folding of 12 rounds stitched together:
princeCore :: Key -> Block -> Block
princeCore :: SWord 64 -> SWord 64 -> SWord 64
princeCore SWord 64
k1 SWord 64
inp = SWord 64
end
   where start :: SWord 64
start    = SWord 64
inp SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` SWord 64
k1 SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` Int -> SWord 64
rConstants Int
0
         front5 :: SWord 64
front5   = (SWord 64 -> Int -> SWord 64) -> SWord 64 -> [Int] -> SWord 64
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (SWord 64 -> SWord 64 -> Int -> SWord 64
round SWord 64
k1) SWord 64
start    [Int
1 .. Int
5]
         midPoint :: SWord 64
midPoint = SWord 64 -> SWord 64
sBoxInv (SWord 64 -> SWord 64)
-> (SWord 64 -> SWord 64) -> SWord 64 -> SWord 64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 64 -> SWord 64
m' (SWord 64 -> SWord 64)
-> (SWord 64 -> SWord 64) -> SWord 64 -> SWord 64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 64 -> SWord 64
sBox (SWord 64 -> SWord 64) -> SWord 64 -> SWord 64
forall a b. (a -> b) -> a -> b
$ SWord 64
front5
         back5 :: SWord 64
back5    = (SWord 64 -> Int -> SWord 64) -> SWord 64 -> [Int] -> SWord 64
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (SWord 64 -> SWord 64 -> Int -> SWord 64
invRound SWord 64
k1) SWord 64
midPoint [Int
6..Int
10]
         end :: SWord 64
end      = SWord 64
back5 SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` Int -> SWord 64
rConstants Int
11 SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` SWord 64
k1

-- | Forward round.
round :: Key -> Block -> Int -> Block
round :: SWord 64 -> SWord 64 -> Int -> SWord 64
round SWord 64
k1 SWord 64
b Int
i = SWord 64
k1 SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` Int -> SWord 64
rConstants Int
i SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` SWord 64 -> SWord 64
m (SWord 64 -> SWord 64
sBox SWord 64
b)

-- | Backend round.
invRound :: Key -> Block -> Int -> Block
invRound :: SWord 64 -> SWord 64 -> Int -> SWord 64
invRound SWord 64
k1 SWord 64
b Int
i = SWord 64 -> SWord 64
sBoxInv (SWord 64 -> SWord 64
mInv (Int -> SWord 64
rConstants Int
i SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` (SWord 64
b SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` SWord 64
k1)))

-- | M transformation.
m :: Block -> Block
m :: SWord 64 -> SWord 64
m = SWord 64 -> SWord 64
sr (SWord 64 -> SWord 64)
-> (SWord 64 -> SWord 64) -> SWord 64 -> SWord 64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 64 -> SWord 64
m'

-- | Inverse of M.
mInv :: Block -> Block
mInv :: SWord 64 -> SWord 64
mInv = SWord 64 -> SWord 64
m' (SWord 64 -> SWord 64)
-> (SWord 64 -> SWord 64) -> SWord 64 -> SWord 64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 64 -> SWord 64
srInv

-- | SR.
sr :: Block -> Block
sr :: SWord 64 -> SWord 64
sr SWord 64
b = [SWord 8] -> SWord 64
fromNibbles [SWord 8
n0, SWord 8
n5, SWord 8
n10, SWord 8
n15, SWord 8
n4, SWord 8
n9, SWord 8
n14, SWord 8
n3, SWord 8
n8, SWord 8
n13, SWord 8
n2, SWord 8
n7, SWord 8
n12, SWord 8
n1, SWord 8
n6, SWord 8
n11]
  where [SWord 8
n0, SWord 8
n1, SWord 8
n2, SWord 8
n3, SWord 8
n4, SWord 8
n5, SWord 8
n6, SWord 8
n7, SWord 8
n8, SWord 8
n9, SWord 8
n10, SWord 8
n11, SWord 8
n12, SWord 8
n13, SWord 8
n14, SWord 8
n15] = SWord 64 -> [SWord 8]
toNibbles SWord 64
b

-- | Inverse of SR:
srInv :: Block -> Block
srInv :: SWord 64 -> SWord 64
srInv SWord 64
b = [SWord 8] -> SWord 64
fromNibbles [SWord 8
n0, SWord 8
n1, SWord 8
n2, SWord 8
n3, SWord 8
n4, SWord 8
n5, SWord 8
n6, SWord 8
n7, SWord 8
n8, SWord 8
n9, SWord 8
n10, SWord 8
n11, SWord 8
n12, SWord 8
n13, SWord 8
n14, SWord 8
n15]
  where [SWord 8
n0, SWord 8
n5, SWord 8
n10, SWord 8
n15, SWord 8
n4, SWord 8
n9, SWord 8
n14, SWord 8
n3, SWord 8
n8, SWord 8
n13, SWord 8
n2, SWord 8
n7, SWord 8
n12, SWord 8
n1, SWord 8
n6, SWord 8
n11] = SWord 64 -> [SWord 8]
toNibbles SWord 64
b

-- | Prove sr and srInv are inverses: We have:
--
-- >>> prove prop_sr
-- Q.E.D.
prop_sr :: Predicate
prop_sr :: Predicate
prop_sr = do b <- String -> Symbolic (SWord 64)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"block"
             return $   b .== sr (srInv b)
                    .&& b .== srInv (sr b)

-- | M' transformation
m' :: Block -> Block
m' :: SWord 64 -> SWord 64
m' = SWord 64 -> SWord 64
mMult

-- | The matrix as described in Section 3.3
mat :: [[Int]]
mat :: [[Int]]
mat = [[Int]]
res
  where m0 :: [[Int]]
m0 = [[Int
0, Int
0, Int
0, Int
0], [Int
0, Int
1, Int
0, Int
0], [Int
0, Int
0, Int
1, Int
0], [Int
0, Int
0, Int
0, Int
1]]
        m1 :: [[Int]]
m1 = [[Int
1, Int
0, Int
0, Int
0], [Int
0, Int
0, Int
0, Int
0], [Int
0, Int
0, Int
1, Int
0], [Int
0, Int
0, Int
0, Int
1]]
        m2 :: [[Int]]
m2 = [[Int
1, Int
0, Int
0, Int
0], [Int
0, Int
1, Int
0, Int
0], [Int
0, Int
0, Int
0, Int
0], [Int
0, Int
0, Int
0, Int
1]]
        m3 :: [[Int]]
m3 = [[Int
1, Int
0, Int
0, Int
0], [Int
0, Int
1, Int
0, Int
0], [Int
0, Int
0, Int
1, Int
0], [Int
0, Int
0, Int
0, Int
0]]

        rows :: [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[a]]
as [[a]]
bs [[a]]
cs [[a]]
ds = [[a]
a [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
b [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
c [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
d | [a]
a <- [[a]]
as | [a]
b <- [[a]]
bs | [a]
c <- [[a]]
cs | [a]
d <- [[a]]
ds ]

        m0' :: [[Int]]
m0' = [[[Int]]] -> [[Int]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
m0 [[Int]]
m1 [[Int]]
m2 [[Int]]
m3, [[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
m1 [[Int]]
m2 [[Int]]
m3 [[Int]]
m0, [[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
m2 [[Int]]
m3 [[Int]]
m0 [[Int]]
m1, [[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
m3 [[Int]]
m0 [[Int]]
m1 [[Int]]
m2]
        m1' :: [[Int]]
m1' = [[[Int]]] -> [[Int]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
m1 [[Int]]
m2 [[Int]]
m3 [[Int]]
m0, [[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
m2 [[Int]]
m3 [[Int]]
m0 [[Int]]
m1, [[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
m3 [[Int]]
m0 [[Int]]
m1 [[Int]]
m2, [[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
m0 [[Int]]
m1 [[Int]]
m2 [[Int]]
m3]

        zs :: [[Int]]
zs  = Int -> [Int] -> [[Int]]
forall a. Int -> a -> [a]
replicate Int
16 (Int -> Int -> [Int]
forall a. Int -> a -> [a]
replicate Int
16 Int
0)
        res :: [[Int]]
res = [[[Int]]] -> [[Int]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
m0' [[Int]]
zs  [[Int]]
zs  [[Int]]
zs, [[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
zs  [[Int]]
m1' [[Int]]
zs  [[Int]]
zs, [[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
zs  [[Int]]
zs  [[Int]]
m1' [[Int]]
zs, [[Int]] -> [[Int]] -> [[Int]] -> [[Int]] -> [[Int]]
forall {a}. [[a]] -> [[a]] -> [[a]] -> [[a]] -> [[a]]
rows [[Int]]
zs  [[Int]]
zs  [[Int]]
zs  [[Int]]
m0']

-- | Multiplication.
mMult :: Block -> Block
mMult :: SWord 64 -> SWord 64
mMult SWord 64
b | [[Int]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Int]]
mat Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64           = String -> SWord 64
forall a. HasCallStack => String -> a
error (String -> SWord 64) -> String -> SWord 64
forall a b. (a -> b) -> a -> b
$ String
"mMult: Expected 64 rows, got       : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([[Int]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Int]]
mat)
        | ([Int] -> Bool) -> [[Int]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64) (Int -> Bool) -> ([Int] -> Int) -> [Int] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) [[Int]]
mat = String -> SWord 64
forall a. HasCallStack => String -> a
error (String -> SWord 64) -> String -> SWord 64
forall a b. (a -> b) -> a -> b
$ String
"mMult: Expected 64 on each row, got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, Int)] -> String
forall a. Show a => a -> String
show [(Int, Int)
p | p :: (Int, Int)
p@(Int
_, Int
l) <- [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1::Int)..] (([Int] -> Int) -> [[Int]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Int]]
mat), Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64]
        | Bool
True                       = [SBool] -> SWord 64
forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE ([SBool] -> SWord 64) -> [SBool] -> SWord 64
forall a b. (a -> b) -> a -> b
$ ([Int] -> SBool) -> [[Int]] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> SBool
mult [[Int]]
mat
  where bits :: [SBool]
bits = SWord 64 -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SWord 64
b

        mult :: [Int] -> SBool
        mult :: [Int] -> SBool
mult [Int]
row = (SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SBool -> SBool -> SBool
(.<+>) SBool
sFalse ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ (Int -> SBool -> SBool) -> [Int] -> [SBool] -> [SBool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> SBool -> SBool
mul [Int]
row [SBool]
bits

        mul :: Int -> SBool -> SBool
        mul :: Int -> SBool -> SBool
mul Int
0 SBool
_ = SBool
sFalse
        mul Int
1 SBool
v = SBool
v
        mul Int
i SBool
_ = String -> SBool
forall a. HasCallStack => String -> a
error (String -> SBool) -> String -> SBool
forall a b. (a -> b) -> a -> b
$ String
"mMult: Unexpected constant: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

-- | Non-linear transformation of a block
nonLinear :: [Nibble] -> Nibble -> Block -> Block
nonLinear :: [SWord 8] -> SWord 8 -> SWord 64 -> SWord 64
nonLinear [SWord 8]
box SWord 8
def = [SWord 8] -> SWord 64
fromNibbles ([SWord 8] -> SWord 64)
-> (SWord 64 -> [SWord 8]) -> SWord 64 -> SWord 64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SWord 8 -> SWord 8) -> [SWord 8] -> [SWord 8]
forall a b. (a -> b) -> [a] -> [b]
map SWord 8 -> SWord 8
s ([SWord 8] -> [SWord 8])
-> (SWord 64 -> [SWord 8]) -> SWord 64 -> [SWord 8]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 64 -> [SWord 8]
toNibbles
  where s :: Nibble -> Nibble
        s :: SWord 8 -> SWord 8
s = [SWord 8] -> SWord 8 -> SWord 8 -> SWord 8
forall b.
(Ord b, SymVal b, Num b, Num (SBV b)) =>
[SWord 8] -> SWord 8 -> SBV b -> SWord 8
forall a b.
(Mergeable a, Ord b, SymVal b, Num b, Num (SBV b)) =>
[a] -> a -> SBV b -> a
select [SWord 8]
box SWord 8
def

-- | SBox transformation.
sBox :: Block -> Block
sBox :: SWord 64 -> SWord 64
sBox = [SWord 8] -> SWord 8 -> SWord 64 -> SWord 64
nonLinear [SWord 8
0xB, SWord 8
0xF, SWord 8
0x3, SWord 8
0x2, SWord 8
0xA, SWord 8
0xC, SWord 8
0x9, SWord 8
0x1, SWord 8
0x6, SWord 8
0x7, SWord 8
0x8, SWord 8
0x0, SWord 8
0xE, SWord 8
0x5, SWord 8
0xD, SWord 8
0x4] SWord 8
0x0

-- | Inverse SBox transformation.
sBoxInv :: Block -> Block
sBoxInv :: SWord 64 -> SWord 64
sBoxInv = [SWord 8] -> SWord 8 -> SWord 64 -> SWord 64
nonLinear [SWord 8
0xB, SWord 8
0x7, SWord 8
0x3, SWord 8
0x2, SWord 8
0xF, SWord 8
0xD, SWord 8
0x8, SWord 8
0x9, SWord 8
0xA, SWord 8
0x6, SWord 8
0x4, SWord 8
0x0, SWord 8
0x5, SWord 8
0xE, SWord 8
0xC, SWord 8
0x1] SWord 8
0x0

-- | Prove that sbox and sBoxInv are inverses: We have:
--
-- >>> prove prop_SBox
-- Q.E.D.
prop_SBox :: Predicate
prop_SBox :: Predicate
prop_SBox = do b <- String -> Symbolic (SWord 64)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"block"
               return $   b .== sBoxInv (sBox b)
                      .&& b .== sBox (sBoxInv b)

-- * Round constants

-- | Round constants
rConstants :: Int -> SWord 64
rConstants :: Int -> SWord 64
rConstants  Int
0 = SWord 64
0x0000000000000000
rConstants  Int
1 = SWord 64
0x13198a2e03707344
rConstants  Int
2 = SWord 64
0xa4093822299f31d0
rConstants  Int
3 = SWord 64
0x082efa98ec4e6c89
rConstants  Int
4 = SWord 64
0x452821e638d01377
rConstants  Int
5 = SWord 64
0xbe5466cf34e90c6c
rConstants  Int
6 = SWord 64
0x7ef84f78fd955cb1
rConstants  Int
7 = SWord 64
0x85840851f1ac43aa
rConstants  Int
8 = SWord 64
0xc882d32f25323c54
rConstants  Int
9 = SWord 64
0x64a51195e0e3610d
rConstants Int
10 = SWord 64
0xd3b5a399ca0c2399
rConstants Int
11 = SWord 64
0xc0ac29b7c97c50dd
rConstants Int
n  = String -> SWord 64
forall a. HasCallStack => String -> a
error (String -> SWord 64) -> String -> SWord 64
forall a b. (a -> b) -> a -> b
$ String
"rConstants called with invalid round number: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n

-- | Round-constants property: rc_i `xor` rc_{11-i} is constant. We have:
--
-- >>> prop_RoundKeys
-- True
prop_RoundKeys :: SBool
prop_RoundKeys :: SBool
prop_RoundKeys = [SBool] -> SBool
sAnd [SWord 64
magic SWord 64 -> SWord 64 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Int -> SWord 64
rConstants Int
i SWord 64 -> SWord 64 -> SWord 64
forall a. Bits a => a -> a -> a
`xor` Int -> SWord 64
rConstants (Int
11Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i) | Int
i <- [Int
0 .. Int
11]]
  where magic :: SWord 64
magic = Int -> SWord 64
rConstants Int
11

-- | Convert a 64 bit word to nibbles
toNibbles :: SWord 64 -> [Nibble]
toNibbles :: SWord 64 -> [SWord 8]
toNibbles = (SWord 8 -> [SWord 8]) -> [SWord 8] -> [SWord 8]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SWord 8 -> [SWord 8]
nibbles ([SWord 8] -> [SWord 8])
-> (SWord 64 -> [SWord 8]) -> SWord 64 -> [SWord 8]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 64 -> [SWord 8]
forall a. ByteConverter a => a -> [SWord 8]
toBytes
  where nibbles :: SWord 8 -> [Nibble]
        nibbles :: SWord 8 -> [SWord 8]
nibbles SWord 8
b = [SWord 8
b SWord 8 -> Int -> SWord 8
forall a. Bits a => a -> Int -> a
`shiftR` Int
4, SWord 8
b SWord 8 -> SWord 8 -> SWord 8
forall a. Bits a => a -> a -> a
.&. SWord 8
0xF]

-- | Convert from nibbles to a 64 bit word
fromNibbles :: [Nibble] -> SWord 64
fromNibbles :: [SWord 8] -> SWord 64
fromNibbles [SWord 8]
xs
  | [SWord 8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
16 = String -> SWord 64
forall a. HasCallStack => String -> a
error (String -> SWord 64) -> String -> SWord 64
forall a b. (a -> b) -> a -> b
$ String
"fromNibbles: Incorrect number of nibbles, expected 16, got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([SWord 8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 8]
xs)
  | Bool
True            = [SWord 8] -> SWord 64
forall a. ByteConverter a => [SWord 8] -> a
fromBytes ([SWord 8] -> SWord 64) -> [SWord 8] -> SWord 64
forall a b. (a -> b) -> a -> b
$ [SWord 8] -> [SWord 8]
forall {a}. Bits a => [a] -> [a]
cvt [SWord 8]
xs
  where cvt :: [a] -> [a]
cvt (a
n1 : a
n2 : [a]
ns) = (a
n1 a -> Int -> a
forall a. Bits a => a -> Int -> a
`shiftL` Int
4 a -> a -> a
forall a. Bits a => a -> a -> a
.|. a
n2) a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a]
cvt [a]
ns
        cvt [a]
_              = []

-- * Test vectors

-- | From Appendix A of the spec. We have:
--
-- >>> testVectors
-- True
testVectors :: SBool
testVectors :: SBool
testVectors = [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$  [SWord 64 -> SWord 64 -> SWord 64 -> SWord 64
encrypt SWord 64
pt SWord 64
k0 SWord 64
k1 SWord 64 -> SWord 64 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 64
ct | (SWord 64
pt, SWord 64
k0, SWord 64
k1, SWord 64
ct) <- [(SWord 64, SWord 64, SWord 64, SWord 64)]
tvs]
                   [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ [SWord 64 -> SWord 64 -> SWord 64 -> SWord 64
decrypt SWord 64
ct SWord 64
k0 SWord 64
k1 SWord 64 -> SWord 64 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 64
pt | (SWord 64
pt, SWord 64
k0, SWord 64
k1, SWord 64
ct) <- [(SWord 64, SWord 64, SWord 64, SWord 64)]
tvs]
   where tvs :: [(SWord 64, SWord 64, SWord 64, SWord 64)]
         tvs :: [(SWord 64, SWord 64, SWord 64, SWord 64)]
tvs = [ (SWord 64
0x0000000000000000, SWord 64
0x0000000000000000, SWord 64
0x0000000000000000, SWord 64
0x818665aa0d02dfda)
               , (SWord 64
0xffffffffffffffff, SWord 64
0x0000000000000000, SWord 64
0x0000000000000000, SWord 64
0x604ae6ca03c20ada)
               , (SWord 64
0x0000000000000000, SWord 64
0xffffffffffffffff, SWord 64
0x0000000000000000, SWord 64
0x9fb51935fc3df524)
               , (SWord 64
0x0000000000000000, SWord 64
0x0000000000000000, SWord 64
0xffffffffffffffff, SWord 64
0x78a54cbe737bb7ef)
               , (SWord 64
0x0123456789abcdef, SWord 64
0x0000000000000000, SWord 64
0xfedcba9876543210, SWord 64
0xae25ad3ca8fa9ccf)
               ]

-- | Nicely show a concrete block.
showBlock :: Block -> String
showBlock :: SWord 64 -> String
showBlock SWord 64
b =  case SWord 64 -> Maybe (WordN 64)
forall a. SymVal a => SBV a -> Maybe a
unliteral SWord 64
b of
                 Just WordN 64
v  -> String
"0x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
pad (WordN 64 -> String -> String
forall a. Integral a => a -> String -> String
showHex WordN 64
v String
"")
                 Maybe (WordN 64)
Nothing -> String -> String
forall a. HasCallStack => String -> a
error String
"showBlock: Symbolic input!"
  where pad :: String -> String
pad String
s = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
16 (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
reverse String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat Char
'0'

-- * Code generation

-- | Generating C code for the encryption block.
codeGen :: IO ()
codeGen :: IO ()
codeGen = Maybe String -> String -> SBVCodeGen () -> IO ()
forall a. Maybe String -> String -> SBVCodeGen a -> IO a
compileToC Maybe String
forall a. Maybe a
Nothing String
"enc" (SBVCodeGen () -> IO ()) -> SBVCodeGen () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
               input <- String -> SBVCodeGen (SWord 64)
forall a. SymVal a => String -> SBVCodeGen (SBV a)
cgInput String
"inp"
               k0    <- cgInput "k0"
               k1    <- cgInput "k1"
               cgOverwriteFiles True
               cgOutput "ct"  $ encrypt input k0 k1