« Tech Talk: SMACCMPilot: flying quadcopters using new techniques for embedded programming | Main | Tech Talk: The Constrained-Monad Problem »

SIMON and SPECK in Cryptol

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


We've formally specified both ciphers in Cryptol:


The following sections explore some applications of our specifications.


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])


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

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!

Reader Comments (2)

> The proof completes in less than 30 seconds!

So what are we missing here?

June 25, 2013 | Unregistered CommenterAnonymous

I've edited the post to explain how Cryptol's :prove command works. I hope that helps.


June 26, 2013 | Registered CommenterDavid Lazar

PostPost a New Comment

Enter your information below to add a new comment.

My response is on my own website »
Author Email (optional):
Author URL (optional):
Some HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>