Cryptol

Cryptographic algorithms are typically very complicated, which means that it's hard to get them working correctly in either hardware or software. If you're implementing a new one, you often need to carefully step through your algorithm by hand to make sure that it's correct, a process that can be very time consuming.

To make this easier, a company called Galois has made Cryptol, a domain-specific language that's designed for the sole purpose of specifying cryptographic algorithms. From looking at the Cryptol Programming Guide, it looks like Cryptol is realy designed for specifying symmetric algoritms and hash functions instead of public-key algorithms. Once you develop and debug your algorithm in Cryptol, you can then create an implementation of your algorithm in C, VHDL or Haskell. From Example 8-1 in the Cryptol Programming Guide, here's what the high-level structure of DES looks like in Cryptol:

des : {a b} (a > = 7) = > ([2**(a- 1)],[b][48]) - > [64];
des (pt, keys) = permute (FP, swap (split last))
where { pt’ = permute (IP, pt);
   iv = [| round (k, split lr)
   | | k < - keys
   | | lr < - [pt’] # iv
   | ];
   last = iv @ (width keys - 1);
};
round (k, [l r]) = r # (l ^ f (r, k));
f (r, k) = permute(PP, SBox(k ^ permute(EP, r)));
swap [a b] = b # a;
permute : {a b} (b > = 1) = > ([a][b], [2**(b - 1)]) - > [a];
permute (p, m) = [| m @ (i - 1) | | i < - p | ];

Cryptol also provides a way to check an implementation of an algorithm against a reference specification that's written in Cryptol. That may be the best use of Cryptol; it's certainly more useful that the ability to implement your algorithm in Haskell. This means that organizations like the IEEE Security in Storage Working Group that are defining new modes of operation of AES can provide a reference specification in Cryptol and anyone implementing the new modes can use Cryptol to verify that their implementation is correct. That's a handy capability to have.