SIMON and SPECK in Cryptol

Last week, the NSA published two families of lightweight block ciphers, SIMON and SPECK:

http://eprint.iacr.org/2013/404

We’ve formally specified both ciphers in Cryptol:

https://github.com/GaloisInc/cryptol/blob/master/examples/contrib/simon.cry

https://github.com/GaloisInc/cryptol/blob/master/examples/contrib/speck.cry

Parameters

SIMON and SPECK are cipher families: each algorithm in the family offers different security and performance based on parameters such as block size, key size, and number of rounds. In Cryptol, we can use type variables to represent these parameters. For example, consider the type signature of SIMON’s encrypt function:

encrypt : {n m T j} (...) => [m][n] -> ([n], [n]) -> ([n], [n]);

Each type variable corresponds to a parameter in the cipher:

• n is the word size (the block size is 2n)
• m is the number of key words
• T is the number of rounds
• j specifies which round constant to use

The encrypt function can be instantiated with almost any values for its parameters (subject to some constraints not shown here). This gives us an elegant way to construct the variants of SIMON:

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};
...

We can also experiment with stronger or weaker variants of the cipher:

simon> :let weakSimon = encrypt `{n=8, m=4, T=16, j=0}
simon> :type weakSimon
weakSimon : [4][8] -> ([8],[8]) -> ([8],[8])

Verification

An important property of block ciphers is that decryption is the inverse operation of encryption. We can state this property in Cryptol for the Speck64_96 encryption function (and its corresponding Speck64_96' decryption function) as follows:

theorem correctSpeck64_96: {k b}. Speck64_96' k (Speck64_96 k b) == b;

The theorem is universally quantified over all keys k and all blocks b.

We can use Cryptol’s :check command to test whether the theorem holds for several randomly generated inputs:

speck> :check correctSpeck64_96
Checking case 1000 of 1000 (100.00%)
1000 tests passed OK
[Coverage: 0.00%. (1000/1461501637330902918203684832716283019655932542976)]

However this did not give us good coverage of the state space. Instead, we can use Cryptol’s :prove command to show the theorem holds for every possible input:

speck> :prove correctSpeck64_96
Q.E.D.

Cryptol proves the theorem by asking a SAT solver whether the negation of the theorem is satisfiable. If the negation is satisfiable, Cryptol returns the satisfying assignment as a counterexample to the theorem. In this case, the SAT solver says the negation is unsatisfiable so the theorem holds. The proof completes in less than 30 seconds!