/*
 * Copyright (c) 2013-2016 Galois, Inc.
 * Distributed under the terms of the BSD3 license (see LICENSE file)
 */

/* Cryptol specification of the Simon block cipher
 * Author: David Lazar
 */

///////////////////////////////////////////////////////////////////////
// parameters
///////////////////////////////////////////////////////////////////////
module simon where

Simon32_64    = encrypt `{n=16,m=4,T=32,j=0}
Simon48_72    = encrypt `{n=24,m=3,T=36,j=0}
Simon48_96    = encrypt `{n=24,m=4,T=36,j=1}
Simon64_96    = encrypt `{n=32,m=3,T=42,j=2}
Simon64_128   = encrypt `{n=32,m=4,T=44,j=3}
Simon96_96    = encrypt `{n=48,m=2,T=52,j=2}
Simon96_144   = encrypt `{n=48,m=3,T=54,j=3}
Simon128_128  = encrypt `{n=64,m=2,T=68,j=2}
Simon128_192  = encrypt `{n=64,m=3,T=69,j=3}
Simon128_256  = encrypt `{n=64,m=4,T=72,j=4}

Simon32_64'   = decrypt `{n=16,m=4,T=32,j=0}
Simon48_72'   = decrypt `{n=24,m=3,T=36,j=0}
Simon48_96'   = decrypt `{n=24,m=4,T=36,j=1}
Simon64_96'   = decrypt `{n=32,m=3,T=42,j=2}
Simon64_128'  = decrypt `{n=32,m=4,T=44,j=3}
Simon96_96'   = decrypt `{n=48,m=2,T=52,j=2}
Simon96_144'  = decrypt `{n=48,m=3,T=54,j=3}
Simon128_128' = decrypt `{n=64,m=2,T=68,j=2}
Simon128_192' = decrypt `{n=64,m=3,T=69,j=3}
Simon128_256' = decrypt `{n=64,m=4,T=72,j=4}

// check only a few of them for now
property correctSimon32_64 k b   = Simon32_64' k (Simon32_64 k b) == b
property correctSimon64_96 k b   = Simon64_96' k (Simon64_96 k b) == b
property correctSimon96_144 k b  = Simon96_144' k (Simon96_144 k b) == b
property correctSimon128_128 k b = Simon128_128' k (Simon128_128 k b) == b
property correctSimon128_256 k b = Simon128_256' k (Simon128_256 k b) == b

property uniqueExpandSimon32_64 k1 k2 = (k1 == k2) || (expandKey `{n=16,m=4,T=32,j=0} k1 != expandKey `{n=16,m=4,T=32,j=0} k2)
property uniqueExpandSimon48_72 k1 k2 = (k1 == k2) || (expandKey `{n=24,m=3,T=36,j=0} k1 != expandKey `{n=24,m=3,T=36,j=0} k2)
property uniqueExpandSimon48_96 k1 k2 = (k1 == k2) || (expandKey `{n=24,m=4,T=36,j=1} k1 != expandKey `{n=24,m=4,T=36,j=1} k2)
property uniqueExpandSimon64_96 k1 k2 = (k1 == k2) || (expandKey `{n=32,m=3,T=42,j=2} k1 != expandKey `{n=32,m=3,T=42,j=2} k2)
property uniqueExpandSimon64_128 k1 k2 = (k1 == k2) || (expandKey `{n=32,m=4,T=44,j=3} k1 != expandKey `{n=32,m=4,T=44,j=3} k2)
property uniqueExpandSimon96_96 k1 k2 = (k1 == k2) || (expandKey `{n=48,m=2,T=52,j=2} k1 != expandKey `{n=48,m=2,T=52,j=2} k2)
property uniqueExpandSimon96_144 k1 k2 = (k1 == k2) || (expandKey `{n=48,m=3,T=54,j=3} k1 != expandKey `{n=48,m=3,T=54,j=3} k2)
property uniqueExpandSimon128_128 k1 k2 = (k1 == k2) || (expandKey `{n=64,m=2,T=68,j=2} k1 != expandKey `{n=64,m=2,T=68,j=2} k2)
property uniqueExpandSimon128_192 k1 k2 = (k1 == k2) || (expandKey `{n=64,m=3,T=69,j=3} k1 != expandKey `{n=64,m=3,T=69,j=3} k2)
property uniqueExpandSimon128_256 k1 k2 = (k1 == k2) || (expandKey `{n=64,m=4,T=72,j=4} k1 != expandKey `{n=64,m=4,T=72,j=4} k2)

// A weak key theorem would look something like:
// :prove exists (\k1 -> exists (\k2 -> forall (\x -> Simon32_64 k1 (Simon32_64 k2 x) != x)))


///////////////////////////////////////////////////////////////////////
// round function
///////////////////////////////////////////////////////////////////////

R k (x, y) = (y ^ f x ^ k, x)

// inverse
R' k (x, y) = (y, x ^ f y ^ k)

f x = ((x <<< 1) && (x <<< 8)) ^ (x <<< 2)


///////////////////////////////////////////////////////////////////////
// encryption / decryption
///////////////////////////////////////////////////////////////////////

encrypt : {n, m, T, j}
    ( fin n, fin m, fin T, fin j
    , n >= 2, 4 >= m, T >= 4, T-1 >= m
    ) => [m][n] -> ([n], [n]) -> ([n], [n])
encrypt k0 b0 = bs ! 0
  where
    bs = [b0] # [ R k b | b <- bs | k <- ks ]
    ks = expandKey `{n=n,m=m,T=T,j=j} (reverse k0)

decrypt : {n, m, T, j}
    ( fin n, fin m, fin T, fin j
    , n >= 2, 4 >= m, T >= 4, T-1 >= m
    ) => [m][n] -> ([n], [n]) -> ([n], [n])
decrypt k0 b0 = bs ! 0
  where
    bs = [b0] # [ R' k b | b <- bs | k <- reverse ks ]
    ks = expandKey `{n=n,m=m,T=T,j=j} (reverse k0)


///////////////////////////////////////////////////////////////////////
// key expansion
///////////////////////////////////////////////////////////////////////

expandKey : {n, m, T, j}
    ( fin n, fin m, fin T, fin j
    , n >= 2, 4 >= m, T >= 4, T-1 >= m
    ) => [m][n] -> [T][n]
expandKey k0 = k
  where
    k = k0 # [ r where
                    o = k @ (i - 1) >>> 3
                    p = if `m == 4 then o ^ k @ (i - 3) else o
                    q = p ^ p >>> 1
                    r = ~ k @ (i - `m) ^ q ^ z ^ 3
                    z = Z @ `j @ ((i - `m) % 62)
             | i <- [m .. T - 1]
             ]

// TODO specify how Z is constructed
Z = [[1, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 0, 0, 1, 0, 1, 0, 1, 1, 0,
      0, 0, 0, 1, 1, 1, 0, 0, 1, 1, 0, 1, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1,
      0, 0, 1, 0, 1, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 0, 0, 1, 1, 0],
     [1, 0, 0, 0, 1, 1, 1, 0, 1, 1, 1, 1, 1, 0, 0, 1, 0, 0, 1, 1, 0, 0,
      0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 0, 1, 1, 1, 1, 1,
      0, 0, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 0, 1, 1, 0, 1, 0],
     [1, 0, 1, 0, 1, 1, 1, 1, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 1,
      0, 0, 1, 0, 0, 1, 1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 1,
      1, 1, 1, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 1, 0, 0, 1, 1],
     [1, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1,
      0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0,
      0, 1, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0, 0, 0, 1, 1, 1, 1],
     [1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1,
      1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 1, 1, 1, 0, 0, 0, 0, 1, 1,
      0, 0, 1, 0, 1, 0, 0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 1, 1]]

///////////////////////////////////////////////////////////////////////
// tests
///////////////////////////////////////////////////////////////////////

tests = [t01,t02,t03,t04,t05,t06,t07,t08,t09]
property testsPass = tests == ~zero

t00 = Simon32_64   [0x1918, 0x1110, 0x0908, 0x0100] (0x6565, 0x6877) == (0xc69b, 0xe9bb)
t01 = Simon48_72   [0x121110, 0x0a0908, 0x020100] (0x612067, 0x6e696c) == (0xdae5ac, 0x292cac)
t02 = Simon48_96   [0x1a1918, 0x121110, 0x0a0908, 0x020100] (0x726963, 0x20646e) == (0x6e06a5, 0xacf156)
t03 = Simon64_96   [0x13121110, 0x0b0a0908, 0x03020100] (0x6f722067, 0x6e696c63) == (0x5ca2e27f, 0x111a8fc8)
t04 = Simon64_128  [0x1b1a1918, 0x13121110, 0x0b0a0908, 0x03020100] (0x656b696c, 0x20646e75) == (0x44c8fc20, 0xb9dfa07a)
t05 = Simon96_96   [0x0d0c0b0a0908, 0x050403020100] (0x2072616c6c69, 0x702065687420) == (0x602807a462b4, 0x69063d8ff082)
t06 = Simon96_144  [0x151413121110, 0x0d0c0b0a0908, 0x050403020100] (0x746168742074, 0x73756420666f) == (0xecad1c6c451e, 0x3f59c5db1ae9)
t07 = Simon128_128 [0x0f0e0d0c0b0a0908, 0x0706050403020100] (0x6373656420737265, 0x6c6c657661727420) == (0x49681b1e1e54fe3f, 0x65aa832af84e0bbc)
t08 = Simon128_192 [0x1716151413121110, 0x0f0e0d0c0b0a0908, 0x0706050403020100] (0x206572656874206e, 0x6568772065626972) == (0xc4ac61effcdc0d4f, 0x6c9c8d6e2597b85b)
t09 = Simon128_256 [0x1f1e1d1c1b1a1918, 0x1716151413121110, 0x0f0e0d0c0b0a0908, 0x0706050403020100] (0x74206e69206d6f6f, 0x6d69732061207369) == (0x8d2b5579afc8a3a0, 0x3bf72a87efe7b868)