mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 21:11:35 +03:00
1525 lines
60 KiB
TeX
1525 lines
60 KiB
TeX
\commentout{
|
|
\begin{code}
|
|
module AES where
|
|
|
|
import Enigma
|
|
// import Classic
|
|
\end{code}
|
|
}
|
|
|
|
%#####################################################################
|
|
\chapter{AES: The Advanced Encryption Standard}
|
|
\label{chapter:aes}
|
|
|
|
AES\indAES is a symmetric key encryption algorithm (a symmetric
|
|
cipher, per the discussion in~\autoref{chapter:classic}), based on the
|
|
Rijndael algorithm designed by Joan Daemen and Vincent
|
|
Rijmen~\cite{DaemenR02}\glosAES. (The term {\em symmetric key} means
|
|
that the algorithm uses the same key for encryption and
|
|
decryption.\indSymKey) AES was adopted in 2001 by the US government,
|
|
deemed suitable for protecting classified information up to {\em
|
|
secret} level for the key size 128, and up to the {\em top-secret}
|
|
level for key sizes 192 and 256.
|
|
|
|
In this chapter, we will program AES in Cryptol. Our emphasis will be
|
|
on clarity, as opposed to efficiency, and we shall follow the NIST
|
|
standard description of AES\indAES fairly closely~\cite{aes}\glosNIST.
|
|
Referring to the standard as you work your way through this chapter is
|
|
recommended.
|
|
|
|
Some surprises may be at hand for the reader who has never deeply
|
|
examined a modern cryptography algorithm before.
|
|
|
|
First, algorithms like AES are typically composed of many smaller
|
|
units of varying kinds. Consequently, the entire algorithm is
|
|
constructed bottom-up by specifying and verifying each of its
|
|
component pieces. It is wise to handle smaller and simpler components
|
|
first. It is also a good practice, though hard to accomplish the
|
|
first one or two times you write such a specification, to write
|
|
specifications with an eye toward reuse in multiple instantiations of
|
|
the same algorithm (e.g., different key sizes or configurations). The
|
|
choice between encoding configurations at the type level or the value
|
|
level is aesthetic and practical: some verification is only possible
|
|
when one encodes information at the type level.
|
|
|
|
Second, algorithms frequently depend upon interesting data structures
|
|
and mathematical constructs, the latter of which can be though of as
|
|
data structures in a pure mathematics sense. The definition, shape,
|
|
form, and subtleties of these data structures are critical to the
|
|
\emph{correct definition} of the crypto algorithm \emph{as well as its
|
|
security properties}. Implementing an algorithm using an
|
|
alternative datatype construction that you believe has the same
|
|
properties as that which is stipulated in a standard is nearly always
|
|
the wrong thing to do. Also, the subtleties of these constructions
|
|
usually boils down to what an engineer might think of as ``magic
|
|
numbers''---strange initial values or specific polynomials that appear
|
|
out of thin air. Just remind yourself that the discovery and analysis
|
|
of those magic values was, in general, the joint hard work of a
|
|
community of cryptographers.
|
|
|
|
%=====================================================================
|
|
\section{Parameters}
|
|
\label{sec:aesparams}
|
|
|
|
The AES algorithm always takes 128 bits of input, and always produces
|
|
128 bits of output, regardless of the key size. The key-size can be
|
|
one of 128 (AES128), 192 (AES192), or 256 (AES256). Following the
|
|
standard, we define the following three parameters~\cite[section
|
|
2.2]{aes}:
|
|
\begin{itemize}
|
|
\item {\tt Nb}: Number of columns, always set to 4 by the standard.
|
|
\item {\tt Nk}: Number of key-blocks, which is the number of 32-bit
|
|
words in the key: 4 for AES128, 6 for AES192, and 8 for AES256;
|
|
\item {\tt Nr}: Number of rounds, which {\tt Nr} is always $6 +
|
|
\mbox{\tt Nk}$, according to the standard. Thus, 10 for AES128, 12
|
|
for AES192, and 14 for AES256.
|
|
\end{itemize}
|
|
The Cryptol definitions follow the above descriptions verbatim:
|
|
\begin{code}
|
|
type AES128 = 4
|
|
type AES192 = 6
|
|
type AES256 = 8
|
|
|
|
type Nk = AES128
|
|
type Nb = 4
|
|
type Nr = 6 + Nk
|
|
\end{code}
|
|
The following derived type is helpful in signatures:
|
|
\begin{code}
|
|
type AESKeySize = (Nk*32)
|
|
\end{code}
|
|
|
|
%=====================================================================
|
|
% \section{Polynomials in \texorpdfstring{GF($2^8$)}{GF(2,8)}}
|
|
% \label{sec:polynomials}
|
|
\sectionWithAnswers{Polynomials in \texorpdfstring{GF($2^8$)}{GF(2,8)}}{sec:polynomials}
|
|
|
|
AES\indAES works on a two-dimensional representation of the input
|
|
arranged into bytes, called the {\em state}.\indAESState For a
|
|
128-bit input, we have precisely 4 rows, each containing {\tt Nb}
|
|
(i.e., 4) bytes, each of which is 8 bits wide, totaling
|
|
$4\times4\times8 = 128$ bits. The bytes themselves are treated as
|
|
finite field elements in the Galois field
|
|
GF($2^8$)~\cite{wiki:galoisfield}\indGF, giving rise to the following
|
|
declarations:
|
|
\begin{code}
|
|
type GF28 = [8]
|
|
type State = [4][Nb]GF28
|
|
\end{code}
|
|
|
|
The hard-encoding of \texttt{GF28} in this specification is completely
|
|
appropriate because the construction of AES depends entirely upon the
|
|
Galois field GF($2^8$). It is conceivable that other algorithms might
|
|
be parameterized across GF($2^k$) for some $k$, in which case the
|
|
underlying type declaration would also be parameterized.
|
|
|
|
While a basic understanding Galois field operations is helpful, the
|
|
details are not essential for our modeling purposes. It suffices to
|
|
note that GF($2^8$) has precisely 256 elements, each of which is a
|
|
polynomial\indPoly of maximum degree 7, where the coefficients are
|
|
either 0 or 1. The numbers from 0 to 255 (i.e., all possible 8-bit
|
|
values) are in one-to-one correspondence with these polynomials. The
|
|
coefficients of the polynomial come from the successive bits of the
|
|
number, and vice versa. For instance the 8-bit number 87 can be
|
|
written as {\tt 0b01010111} in binary, and hence corresponds to the
|
|
polynomial $x^6 + x^4 + x^2 + x^1 + 1$. Similarly, the polynomial $x^4
|
|
+ x^3 + x$ corresponds to the number {\tt 0b00011010}, i.e., 26. We
|
|
can also compute this value by evaluating the polynomial for $x=2$,
|
|
obtaining $2^4+2^3+2 = 16+8+2 = 26$.
|
|
|
|
Cryptol allows you to write polynomials in GF($2^n$), for arbitrary
|
|
$n$, using the following notation:
|
|
\begin{Verbatim}
|
|
Cryptol> <| x^^6 + x^^4 + x^^2 + x^^1 + 1 |>
|
|
87
|
|
Cryptol> 0b1010111
|
|
87
|
|
Cryptol> <| x^^4 + x^^3 + x |>
|
|
26
|
|
Cryptol> 0b11010
|
|
26
|
|
\end{Verbatim}
|
|
|
|
A polynomial is similar to a decimal representation of a number,
|
|
albeit in a more suggestive syntax. Like with a decimal, the Cryptol
|
|
type system will default the type to be the smallest number of bits
|
|
required to represent the polynomial, but it may be expanded to more
|
|
bits if an expression requires it.
|
|
|
|
\paragraph*{Addition and Subtraction} Given two polynomials,
|
|
adding\indAddPoly and subtracting\indSubPoly them in a Galois field
|
|
GF($2^n$) results in a new polynomial where terms with the same power
|
|
cancel each other out. When interpreted as a word, both addition and
|
|
subtraction amount to a simple exclusive-or operation. Cryptol's
|
|
\Verb|^|\indXOr operator captures this idiom concisely:
|
|
\begin{Verbatim}
|
|
Cryptol> <| x^^4 + x^^2 |> ^ <| x^^5 + x^^2 + 1 |> == \
|
|
<| x^^5 + x^^4 + 1 |>
|
|
True
|
|
\end{Verbatim}
|
|
Note that the term $x^2$ cancels since it appears in both polynomials.
|
|
\begin{Exercise}\label{ex:gf:0}
|
|
Adding a polynomial to itself in GF($2^n$) will always yield {\tt 0}
|
|
since all the terms will cancel each other. Write and prove a
|
|
theorem {\tt polySelfAdd} over {\tt GF28} to state this fact.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:gf:0}
|
|
\todo[inline]{Recheck use of parentheses in property after \ticket{208}
|
|
is closed.}
|
|
\begin{code}
|
|
polySelfAdd: GF28 -> Bit
|
|
property polySelfAdd x = (x ^ x) == zero
|
|
\end{code}
|
|
We have:\indSBV
|
|
\begin{Verbatim}
|
|
Cryptol> :prove polySelfAdd
|
|
Q.E.D.
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
\unparagraph While adding two polynomials does not warrant a separate
|
|
function, we will need a version that can add a sequence of
|
|
polynomials:
|
|
\begin{Exercise}\label{ex:gf:add0}
|
|
Define a function
|
|
\begin{code}
|
|
gf28Add : {n} (fin n) => [n]GF28 -> GF28
|
|
\end{code}
|
|
that adds all the elements given.
|
|
\lhint{Use a fold, see page~\pageref{par:fold}.}\indFold
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:gf:add0}
|
|
\begin{code}
|
|
gf28Add ps = sums ! 0
|
|
where sums = [zero] # [ p ^ s | p <- ps
|
|
| s <- sums
|
|
]
|
|
\end{code}
|
|
\end{Answer}
|
|
|
|
\paragraph*{Multiplication} Multiplication in GF($2^n$) follows the usual
|
|
polynomial multiplication algorithm, where we multiply the first
|
|
polynomial with each term of the second, and add all the partial sums
|
|
(i.e., compute their exclusive-or). While this operation can be
|
|
programmed explicitly, Cryptol does provide the primitive {\tt
|
|
pmult}\indMulPoly for this purpose:
|
|
\begin{Verbatim}
|
|
Cryptol> pmult <| x^^3 + x^^2 + x + 1 |> <| x^^2 + x + 1 |>
|
|
45
|
|
Cryptol> <| x^^5 + x^^3 + x^^2 + 1 |>
|
|
45
|
|
\end{Verbatim}
|
|
|
|
\begin{Exercise}\label{ex:gf:1}
|
|
Multiply the polynomials $x^3 +x^2+x+1$ and $x^2+x+1$ by hand in
|
|
GF($2^8$) and show that the result is indeed $x^5+x^3+x^2+1$, (i.e.,
|
|
$45$), justifying Cryptol's result above.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:gf:1}
|
|
\todo[inline]{Figure out outdent on this answer if this todo note is
|
|
removed.} We first compute the results of multiplying our first
|
|
polynomial ($x^3 +x^2+x+1$) with each term in the second polynomial
|
|
($x^2+x+1$) separately:
|
|
\begin{eqnarray*}
|
|
(x^3 + x^2 + x + 1) \times x^2 &=& x^5 + x^4 + x^3 + x^2 \\
|
|
(x^3 + x^2 + x + 1) \times x\;\; &=& x^4 + x^3 + x^2 + x \\
|
|
(x^3 + x^2 + x + 1) \times 1\;\; &=& x^3 + x^2 + x\;\; + 1
|
|
\end{eqnarray*}
|
|
We now add the resulting polynomials, remembering the adding the same
|
|
powered terms cancel each other out. For instance, we have two
|
|
instances each of $x^4$, $x^2$, and $x$, which all get canceled. We
|
|
have three instances each of $x^3$ and $x^2$, so they survive the
|
|
addition, etc. After the addition, we are left with the polynomial
|
|
$x^5 + x^3 + x^2 + 1$, which can be interpreted as {\tt 0b00101101},
|
|
i.e., $45$.
|
|
\end{Answer}
|
|
|
|
\paragraph*{Reduction} If you multiply two polynomials with degrees $m$
|
|
and $n$, you will get a new polynomial of degree $m+n$. As we
|
|
mentioned before, the polynomials in GF($2^8$)\indGF have degree at
|
|
most 7. Obviously, $m+n$ can be larger than $7$ when we multiply to
|
|
elements of GF($2^8$). So we have to find a way to map the resulting
|
|
larger-degree polynomial back to an element of GF($2^8$). This is done
|
|
by reduction, or modulus, with respect to an {\em irreducible
|
|
polynomial}\indIrredPoly. The AES algorithm uses the following
|
|
polynomial for this purpose:
|
|
\begin{code}
|
|
irreducible = <| x^^8 + x^^4 + x^^3 + x + 1 |>
|
|
\end{code}
|
|
(Recall in the introduction of this chapter our warning about magic!)
|
|
|
|
Note that {\tt irreducible} is {\em not} an element of GF($2^8$),
|
|
since it has degree 8. However we can use this polynomial to define
|
|
the multiplication routine itself, which uses Cryptol's {\tt
|
|
pmod}\indModPoly (polynomial modulus) function, as follows:
|
|
\begin{code}
|
|
gf28Mult : (GF28, GF28) -> GF28
|
|
gf28Mult (x, y) = pmod (pmult x y) irreducible
|
|
\end{code}
|
|
Polynomial modulus and division operations follow the usual schoolbook
|
|
algorithm for long-division---a fairly laborious process in itself,
|
|
but it is well studied in mathematics~\cite{wiki:polydiv}. Luckily for
|
|
us, Cryptol's {\tt pdiv}\indDivPoly and {\tt pmod}\indModPoly
|
|
functions implement these operations, saving us the programming task.
|
|
|
|
\begin{Exercise}\label{ex:pdivmod}
|
|
Divide $x^5 + x^3 + 1$ by $x^3 + x^2 + 1$ by hand, finding the
|
|
quotient and the remainder. Check your answer with Cryptol's {\tt
|
|
pmod} and {\tt pdiv} functions.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:pdivmod}
|
|
The long division algorithm is laborious, but not particularly hard:
|
|
\[
|
|
\renewcommand\arraystretch{1.2}
|
|
\begin{array}{*1r @{\hskip\arraycolsep}c@{\hskip\arraycolsep} *6r}
|
|
% & && & 1 & 1 & 0 \\
|
|
& & & & & x^2 &+ x & \\
|
|
\cline{2-8}
|
|
x^3 + x^2 + 1 &\big)& x^5 & & + x^3 & & & + 1\\
|
|
& & x^5 & + x^4 & & + x^2 & & \\
|
|
\cline{3-6}
|
|
& & & x^4 & + x^3 & + x^2 & & + 1 \\
|
|
& & & x^4 & + x^3 & & + x& \\
|
|
\cline{4-8}
|
|
& & & & & x^2 & + x & + 1 \\
|
|
\end{array}
|
|
\]
|
|
Therefore, the quotient is $x^2+x$ and the remainder is $x^2+x+1$. We
|
|
can verify this easily with Cryptol:
|
|
\begin{Verbatim}
|
|
Cryptol> pdiv <| x^^5 + x^^3 + 1 |> <| x^^3 + x^^2 + 1 |> == \
|
|
<| x^^2 + x |>
|
|
True
|
|
Cryptol> pmod <| x^^5 + x^^3 + 1 |> <| x^^3 + x^^2 + 1 |> == \
|
|
<| x^^2 + x + 1 |>
|
|
True
|
|
\end{Verbatim}
|
|
Another way to check your result would be to multiply the quotient by
|
|
the divisor and add the remainder, and check that it gives us
|
|
precisely the polynomial we started with:
|
|
\begin{Verbatim}
|
|
Cryptol> pmult <| x^^2 + x |> <| x^^3 + x^^2 + 1 |> \
|
|
^ <| x^^2 + x + 1 |>
|
|
0x29
|
|
Cryptol> <| x^^5 + x^^3 + 1 |>
|
|
0x29
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\begin{Exercise}\label{ex:gf:2}
|
|
Write and prove theorems showing that {\tt gf28Mult} (i) has the
|
|
polynomial 1 as its unit, (ii) is commutative, and (iii) is
|
|
associative.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:gf:2}
|
|
\fvset{fontsize=\footnotesize}
|
|
\begin{code}
|
|
property gf28MultUnit x = gf28Mult(x, 1) == x
|
|
property gf28MultCommutative x y = gf28Mult(x, y) == gf28Mult(y, x)
|
|
property gf28MultAssociative x y z = gf28Mult(x, gf28Mult(y, z))
|
|
== gf28Mult(gf28Mult(x, y), z)
|
|
\end{code}
|
|
It turns out that proving the unit and commutativity are fairly
|
|
trivial:\indCmdProve
|
|
\begin{Verbatim}
|
|
Cryptol> :prove gf28MultUnit
|
|
Q.E.D.
|
|
Cryptol> :prove gf28MultCommutative
|
|
Q.E.D.
|
|
\end{Verbatim}
|
|
But {\tt aesMultAssociative} takes much longer! We show the results of
|
|
{\tt :check} below:\indCmdCheck
|
|
\begin{Verbatim}
|
|
Cryptol> :check gf28MultAssociative
|
|
Checking case 1000 of 1000 (100.00%)
|
|
1000 tests passed OK
|
|
\end{Verbatim}
|
|
%% [Coverage: 5.96e-3%. (1000/16777216)]
|
|
Note that the coverage is pretty small (on the order of $0.006\%$)
|
|
in this case. Proving associativity of multiplication algorithms using
|
|
SAT/SMT based technologies is a notoriously hard task~\cite[section
|
|
6.3.1]{DecisionProcedures2008}. If you have the time, you can let
|
|
Cryptol run long enough to complete the {\tt :prove
|
|
gf28MultAssociative} command, however.
|
|
\end{Answer}
|
|
|
|
%=====================================================================
|
|
% \section{The {\ttfamily{\textbf SubBytes}} transformation}
|
|
% \label{aes:subbytes}
|
|
\sectionWithAnswers{The {\ttfamily{\textbf SubBytes}} transformation}{aes:subbytes}
|
|
|
|
\todo[inline]{Introduce a figure here, perhaps lifted from the
|
|
standard, to better explain this stage of the algorithm.}
|
|
|
|
Recall that the state in AES\indAES is a $4\times4$ matrix of
|
|
bytes. As part of its operation, AES\indAES performs the so called
|
|
{\tt SubBytes} transformation\indAESSbox~\cite[section 5.1.1]{aes},
|
|
substituting each byte in the state with another element. Given an $x
|
|
\in \mbox{GF}(2^8)$,\indGF the substitution for $x$ is computed as
|
|
follows:
|
|
\begin{enumerate}
|
|
\item Compute the multiplicative inverse of $x$ in GF$(2^8)$\indGF,
|
|
call it $b$. If $x$ is 0, then take 0 as the result.
|
|
\item Replace bits in $b$ as follows: Each bit $b_i$ becomes $b_i
|
|
\oplus b_{i+4\imod{8}} \oplus b_{i+5\imod{8}} \oplus
|
|
b_{i+6\imod{8}} \oplus b_{i+7\imod{8}} \oplus c_i$. Here $\oplus$
|
|
is exclusive-or and $c$ is {\tt 0x63}.
|
|
\end{enumerate}
|
|
|
|
\paragraph*{Computing the multiplicative inverse} It turns out that the
|
|
inverse of any non-zero $x$ in GF$(2^8)$ can be computed by raising
|
|
$x$ to the power 254, i.e., multiplying $x$ by itself 254
|
|
times. (Mathematically, GF$(2^8)$\indGF is a cyclic group such that
|
|
$x^{255}$ is always $1$ for any $x$, making $x^{254}$ the
|
|
multiplicative inverse of $x$.)
|
|
|
|
\begin{Exercise}\label{ex:gfmi:0}
|
|
Write a function
|
|
\begin{code}
|
|
gf28Pow : (GF28, [8]) -> GF28
|
|
\end{code}
|
|
such that the call {\tt gf28Pow (n, k)} returns $n^k$ using {\tt
|
|
gf28Mult} as the multiplication operator. \lhint{Use the fact that
|
|
$x^0 = 1$, $x^{2n} = (x^n)^2$, and $x^{2n+1} = x \times (x^n)^2$ to
|
|
speed up the exponentiation.}
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:gfmi:0}
|
|
\begin{code}
|
|
gf28Pow (n, k) = pow k
|
|
where sq x = gf28Mult (x, x)
|
|
odd x = x ! 0
|
|
pow i = if i == 0 then 1
|
|
else if odd i
|
|
then gf28Mult (n, sq (pow (i >> 1)))
|
|
else sq (pow (i >> 1))
|
|
\end{code}
|
|
Here is a version that follows the stream-recursion pattern:
|
|
\begin{code}
|
|
gf28Pow' : (GF28, [8]) -> GF28
|
|
gf28Pow' (n, k) = pows ! 0
|
|
where pows = [1] # [ if bit then gf28Mult (n, sq x)
|
|
else sq x
|
|
| x <- pows
|
|
| bit <- k
|
|
]
|
|
sq x = gf28Mult (x, x)
|
|
\end{code}
|
|
\end{Answer}
|
|
|
|
\begin{Exercise}\label{ex:gfmi:01}
|
|
Write a function
|
|
\begin{code}
|
|
gf28Inverse : GF28 -> GF28
|
|
\end{code}
|
|
to compute the multiplicative inverse of a given element by raising it
|
|
to the power $254$. Note that {\tt gf28Inverse} must map $0$ to
|
|
$0$. Do you have to do anything special to make sure this happens?
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:gfmi:01}
|
|
\begin{code}
|
|
gf28Inverse x = gf28Pow (x, 254)
|
|
\end{code}
|
|
We do not have to do anything special about $0$, since our {\tt
|
|
gf28Inverse} function yields $0$ in that case:
|
|
\begin{Verbatim}
|
|
Cryptol> gf28Inverse 0
|
|
0x00
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\begin{Exercise}\label{ex:gfmi:1}
|
|
Write and prove a property {\tt gf28InverseCorrect}, ensuring that
|
|
{\tt gf28Inverse x} does indeed return the multiplicative inverse of
|
|
{\tt x}. Do you have to do anything special when {\tt x} is $0$?
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:gfmi:1}
|
|
Since $0$ does not have a multiplicative inverse, we have to write a
|
|
conditional property:
|
|
\begin{code}
|
|
property gf28InverseCorrect x =
|
|
if x == 0 then x' == 0 else gf28Mult(x, x') == 1
|
|
where x' = gf28Inverse x
|
|
\end{code}
|
|
We have:
|
|
\begin{Verbatim}
|
|
Cryptol> :prove gf28InverseCorrect
|
|
Q.E.D.
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\paragraph*{Transforming the result} As we mentioned above, the
|
|
AES\indAES specification asks us to transform each bit $b_i$ according
|
|
to the following transformation:
|
|
$$
|
|
b_i \oplus b_{i+4\imod{8}} \oplus b_{i+5\imod{8}} \oplus b_{i+6\imod{8}} \oplus b_{i+7\imod{8}} \oplus c_i
|
|
$$
|
|
For instance, bit $b_5$ becomes $b_5 \oplus b_1 \oplus b_2 \oplus b_3
|
|
\oplus c_5$. When interpreted at the word level, this basically
|
|
amounts to computing:
|
|
$$
|
|
b \oplus (b \ggg 4) \oplus (b \ggg 5) \oplus (b \ggg 6) \oplus (b \ggg 7) \oplus c
|
|
$$
|
|
by aligning the corresponding bits in the word representation.
|
|
|
|
\todo[inline]{Justify/prove the equivalence of these two terms.
|
|
Perhaps add a property to prove it in Cryptol?}
|
|
|
|
\begin{Exercise}\label{ex:aessbytes:0}
|
|
Write a function
|
|
\begin{code}
|
|
xformByte : GF28 -> GF28
|
|
\end{code}
|
|
that computes the above described transformation.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aessbytes:0}
|
|
\begin{code}
|
|
xformByte b = gf28Add [b, (b >>> 4), (b >>> 5),
|
|
(b >>> 6), (b >>> 7), c]
|
|
where c = 0x63
|
|
\end{code}
|
|
\end{Answer}
|
|
|
|
\todo[inline]{Remind the reader of the context again before putting
|
|
everything together.}
|
|
|
|
\paragraph*{Putting it together} Armed with {\tt gf28Inverse} and {\tt
|
|
xformByte}, we can easily code the function that transforms a single
|
|
byte as follows:
|
|
\begin{code}
|
|
SubByte : GF28 -> GF28
|
|
SubByte b = xformByte (gf28Inverse b)
|
|
\end{code}
|
|
AES's {\tt SubBytes}\indAES transformation merely applies this
|
|
function to each byte of the state:
|
|
\begin{code}
|
|
SubBytes : State -> State
|
|
SubBytes state = [ [ SubByte b | b <- row ] | row <- state ]
|
|
\end{code}
|
|
|
|
\paragraph*{Table lookup} Our definition of the {\tt SubByte} function
|
|
above follows how the designers of AES came up with the substitution
|
|
maps, i.e., it is a {\em reference} implementation. For efficiency
|
|
purposes, however, we might prefer a version that simply performs a
|
|
look-up in a table. Notice that the type of {\tt SubByte} is {\tt GF28
|
|
-> GF28}, i.e., it takes a value between 0 and 255. Therefore, we
|
|
can make a table containing the precomputed values for all possible
|
|
256 inputs, and simply perform a table look-up instead of computing
|
|
these values each time we need it. In fact, Figure~7 on page 16 of
|
|
the AES\indAES standard lists these precomputed values for
|
|
us~\cite[section 5.1.1]{aes}. We capture this table below in Cryptol:
|
|
\todo[inline]{We should consistently use either ``look-up'' or ``lookup''.}
|
|
|
|
\vspace{0.25cm}
|
|
\begin{minipage}{\textwidth}
|
|
{\footnotesize
|
|
\begin{code}
|
|
sbox : [256]GF28
|
|
sbox = [
|
|
0x63, 0x7c, 0x77, 0x7b, 0xf2, 0x6b, 0x6f, 0xc5, 0x30, 0x01, 0x67,
|
|
0x2b, 0xfe, 0xd7, 0xab, 0x76, 0xca, 0x82, 0xc9, 0x7d, 0xfa, 0x59,
|
|
0x47, 0xf0, 0xad, 0xd4, 0xa2, 0xaf, 0x9c, 0xa4, 0x72, 0xc0, 0xb7,
|
|
0xfd, 0x93, 0x26, 0x36, 0x3f, 0xf7, 0xcc, 0x34, 0xa5, 0xe5, 0xf1,
|
|
0x71, 0xd8, 0x31, 0x15, 0x04, 0xc7, 0x23, 0xc3, 0x18, 0x96, 0x05,
|
|
0x9a, 0x07, 0x12, 0x80, 0xe2, 0xeb, 0x27, 0xb2, 0x75, 0x09, 0x83,
|
|
0x2c, 0x1a, 0x1b, 0x6e, 0x5a, 0xa0, 0x52, 0x3b, 0xd6, 0xb3, 0x29,
|
|
0xe3, 0x2f, 0x84, 0x53, 0xd1, 0x00, 0xed, 0x20, 0xfc, 0xb1, 0x5b,
|
|
0x6a, 0xcb, 0xbe, 0x39, 0x4a, 0x4c, 0x58, 0xcf, 0xd0, 0xef, 0xaa,
|
|
0xfb, 0x43, 0x4d, 0x33, 0x85, 0x45, 0xf9, 0x02, 0x7f, 0x50, 0x3c,
|
|
0x9f, 0xa8, 0x51, 0xa3, 0x40, 0x8f, 0x92, 0x9d, 0x38, 0xf5, 0xbc,
|
|
0xb6, 0xda, 0x21, 0x10, 0xff, 0xf3, 0xd2, 0xcd, 0x0c, 0x13, 0xec,
|
|
0x5f, 0x97, 0x44, 0x17, 0xc4, 0xa7, 0x7e, 0x3d, 0x64, 0x5d, 0x19,
|
|
0x73, 0x60, 0x81, 0x4f, 0xdc, 0x22, 0x2a, 0x90, 0x88, 0x46, 0xee,
|
|
0xb8, 0x14, 0xde, 0x5e, 0x0b, 0xdb, 0xe0, 0x32, 0x3a, 0x0a, 0x49,
|
|
0x06, 0x24, 0x5c, 0xc2, 0xd3, 0xac, 0x62, 0x91, 0x95, 0xe4, 0x79,
|
|
0xe7, 0xc8, 0x37, 0x6d, 0x8d, 0xd5, 0x4e, 0xa9, 0x6c, 0x56, 0xf4,
|
|
0xea, 0x65, 0x7a, 0xae, 0x08, 0xba, 0x78, 0x25, 0x2e, 0x1c, 0xa6,
|
|
0xb4, 0xc6, 0xe8, 0xdd, 0x74, 0x1f, 0x4b, 0xbd, 0x8b, 0x8a, 0x70,
|
|
0x3e, 0xb5, 0x66, 0x48, 0x03, 0xf6, 0x0e, 0x61, 0x35, 0x57, 0xb9,
|
|
0x86, 0xc1, 0x1d, 0x9e, 0xe1, 0xf8, 0x98, 0x11, 0x69, 0xd9, 0x8e,
|
|
0x94, 0x9b, 0x1e, 0x87, 0xe9, 0xce, 0x55, 0x28, 0xdf, 0x8c, 0xa1,
|
|
0x89, 0x0d, 0xbf, 0xe6, 0x42, 0x68, 0x41, 0x99, 0x2d, 0x0f, 0xb0,
|
|
0x54, 0xbb, 0x16]
|
|
\end{code}
|
|
}
|
|
\end{minipage}
|
|
\vspace{0.25cm}
|
|
|
|
\noindent With this definition of {\tt sbox}, the look-up variants of
|
|
{\tt SubByte} and {\tt SubBytes} becomes:\label{aes:subbytetl}
|
|
\begin{code}
|
|
SubByte' : GF28 -> GF28
|
|
SubByte' x = sbox @ x
|
|
|
|
SubBytes' : State -> State
|
|
SubBytes' state = [ [ SubByte' b | b <- row ] | row <- state ]
|
|
\end{code}
|
|
|
|
\begin{Exercise}\label{ex:sbox}
|
|
Write and prove a property stating that {\tt SubByte} and
|
|
{\tt SubByte'} are equivalent.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:sbox}
|
|
\begin{code}
|
|
property SubByteCorrect x = SubByte x == SubByte' x
|
|
\end{code}
|
|
We have:
|
|
\begin{Verbatim}
|
|
Cryptol> :prove SubByteCorrect
|
|
Q.E.D.
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\note{The {\tt SubByte'} and {\tt SubBytes'} versions are going to be
|
|
more efficient for execution, naturally. We should emphasize that
|
|
this mode of development is quite common in modern cryptography.
|
|
Ciphers are typically designed using ideas from mathematics, often
|
|
requiring complicated algorithms. To speed things up, however,
|
|
implementors use clever optimization tricks, convert functions to
|
|
look-up tables using precomputed values, etc.
|
|
|
|
What Cryptol allows us to do is to write the algorithms using both
|
|
styles, and then formally show that they are indeed equivalent, as
|
|
you did in Exercise~\ref{ex:sbox} above. This mode of
|
|
high-assurance development makes sure that we have not made any
|
|
cut-and-paste errors when we wrote down the numbers in our {\tt
|
|
sbox} table. Equivalently, our proof also establishes that the
|
|
official specification~\cite[section 5.1.1]{aes} got its own table
|
|
correct!}
|
|
|
|
\todo[inline]{Revisit a commented-out exercise here after \ticket{210}
|
|
on \texttt{:safe} is addressed.}
|
|
% \begin{Exercise}\label{ex:sbox:safe}
|
|
% The implementation of {\tt SubByte'} uses indexing ({\tt
|
|
% @})\indIndex, and hence we might be worried about
|
|
% index-out-of-bounds errors. In this case the table has precisely
|
|
% 256 elements and we are indexing with a byte, so the indexing must
|
|
% be safe. Use Cryptol's {\tt :safe} command\indCmdSafe to verify
|
|
% this claim.
|
|
% \end{Exercise}
|
|
% \begin{Answer}\ansref{ex:sbox:safe}
|
|
% \begin{Verbatim}
|
|
% Cryptol> :safe SubByte'
|
|
% "SubByte'" is safe; no safety violations exist.
|
|
% \end{Verbatim}
|
|
% \end{Answer}
|
|
|
|
%=====================================================================
|
|
% \section{The {\ttfamily{\textbf ShiftRows}} transformation}
|
|
% \label{aes:shiftrows}
|
|
\sectionWithAnswers{The {\ttfamily{\textbf ShiftRows}} transformation}{aes:shiftrows}
|
|
|
|
\todo[inline]{Need a figure here to get reader in the right frame of
|
|
mind.}
|
|
|
|
The second transformation AES\indAES utilizes is the {\tt
|
|
ShiftRows}\indAESShiftRows operation~\cite[section 5.1.2]{aes}. This
|
|
operation treats the {\tt State} as a $4\times4$ matrix, and rotates
|
|
the last three row to the left by the amounts 1, 2, and 3;
|
|
respectively. Implementing {\tt ShiftRows} in Cryptol is trivial,
|
|
using the \verb+<<<+\indRotLeft operator:
|
|
\begin{code}
|
|
ShiftRows : State -> State
|
|
ShiftRows state = [ row <<< shiftAmount | row <- state
|
|
| shiftAmount <- [0 .. 3]
|
|
]
|
|
\end{code}
|
|
|
|
\begin{Exercise}\label{ex:aesshiftrows:0}
|
|
Can you transform a state back into itself by repeated applications
|
|
of {\tt ShiftRows}? How many times would you need to shift? Verify
|
|
your answer by writing and proving a corresponding Cryptol property.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aesshiftrows:0}
|
|
Consider what happens after 4 calls to {\tt ShiftRows}. The first
|
|
row will stay the same, since it never moves. The second row moves
|
|
one position each time, and hence it will move 4 positions at the
|
|
end, restoring it back to its original starting
|
|
configuration. Similarly, row 3 will rotate $2\times4=8$ times,
|
|
again restoring it. Finally, row 4 rotates 3 times each for a total
|
|
of $3\times4 = 12$ times, cycling back to its starting
|
|
position. Hence, every 4th rotation will restore the entire state
|
|
back. We can verify this in Cryptol by the following property:
|
|
\begin{code}
|
|
shiftRow4RestoresBack : State -> Bit
|
|
property shiftRow4RestoresBack state = states @ 4 == state
|
|
where states = [state] # [ ShiftRows s | s <- states ]
|
|
\end{code}
|
|
We have:
|
|
\begin{Verbatim}
|
|
Cryptol> :prove shiftRow4RestoresBack
|
|
Q.E.D.
|
|
\end{Verbatim}
|
|
Of course, any multiple of 4 would have the same effect.
|
|
\end{Answer}
|
|
|
|
%=====================================================================
|
|
% \section{The {\ttfamily{\textbf MixColumns}} transformation}
|
|
% \label{sec:aesmixcolumns}
|
|
\sectionWithAnswers{The {\ttfamily{\textbf MixColumns}} transformation}{sec:aesmixcolumns}
|
|
|
|
The third major transformation AES\indAES performs is the {\tt
|
|
MixColumns}\indAESMixColumns operation~\cite[section 5.1.3]{aes}.
|
|
In this transformation, the {\tt State} is viewed as a $4\times4$
|
|
matrix, and each successive column of it is replaced by the result of
|
|
multiplying it by the matrix:
|
|
$$
|
|
\left[ \begin{array}{cccc} 2 & 3 & 1 & 1 \\ 1 & 2 & 3 & 1 \\ 1 & 1 & 2 & 3 \\ 3 & 1 & 1 & 2 \end{array} \right]
|
|
$$
|
|
|
|
As you might recall from linear algebra, given two \emph{compatible}
|
|
matrices $A$ and $B$, the $ij$th element of $A\times B$ is the
|
|
dot-product of the $i$th row of $A$ and the $j$th column of $B$.
|
|
(By \emph{compatible} we mean the number of columns of $A$ must be the
|
|
same as the number of rows of $B$. All our matrices are $4\times 4$,
|
|
so they are always compatible.) The dot-product is defined as
|
|
multiplying the corresponding elements of two same-length vectors and
|
|
adding the results together. The only difference here is that we use
|
|
the functions {\tt gf28Add} and {\tt gf28Mult} for addition and
|
|
multiplication respectively. We will develop this algorithm in the
|
|
following sequence of exercises.
|
|
|
|
\begin{Exercise}\label{ex:aesmc:0}
|
|
Write a function {\tt gf28DotProduct} with the signature:
|
|
\begin{code}
|
|
gf28DotProduct : {n} (fin n) => ([n]GF28, [n]GF28) -> GF28
|
|
\end{code}
|
|
such that {\tt gf28DotProduct} returns the dot-product of two length $n$ vectors of GF($2^8$) elements.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aesmc:0}
|
|
\begin{code}
|
|
gf28DotProduct (xs, ys) = gf28Add [ gf28Mult (x, y) | x <- xs
|
|
| y <- ys
|
|
]
|
|
\end{code}
|
|
\end{Answer}
|
|
|
|
\todo[inline]{Check correct with theorem support.}
|
|
|
|
\begin{Exercise}\label{ex:aesmc:1}
|
|
Write properties stating that the vector operation
|
|
\texttt{gf28DotProduct} is commutative and distributive over vector
|
|
addition:
|
|
\begin{eqnarray*}
|
|
a \cdot b &=& b \cdot a \\
|
|
a \cdot (b + c) &=& a\cdot b + a\cdot b
|
|
\end{eqnarray*}
|
|
Addition over vectors is defined element-wise. Prove the commutativity
|
|
property for vectors of length 10. Distributivity will take much
|
|
longer, so you might want to do a \texttt{:check} on it.\indCmdCheck
|
|
\todo[inline]{Explain why distributivity is so much harder to prove.}
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aesmc:1}
|
|
\fvset{fontsize=\small}
|
|
\begin{code}
|
|
property DPComm a b = gf28DotProduct (a, b) == gf28DotProduct (b, a)
|
|
property DPDist a b c = gf28DotProduct (a, vectorAdd(b, c)) ==
|
|
gf28Add [ab, ac]
|
|
where ab = gf28DotProduct (a, b)
|
|
ac = gf28DotProduct (a, c)
|
|
vectorAdd (xs, ys) = [ gf28Add [x, y] | x <- xs
|
|
| y <- ys
|
|
]
|
|
\end{code}
|
|
We have:
|
|
\fvset{fontsize=\normalsize}
|
|
\begin{Verbatim}
|
|
AES> :prove DPComm : [10]GF28 -> [10]GF28 -> Bit
|
|
Q.E.D.
|
|
AES> :check DPDist : [10]GF28 -> [10]GF28 -> [10]GF28 -> Bit
|
|
Using random testing.
|
|
passed 1000 tests.
|
|
\end{Verbatim}
|
|
\todo[inline]{Revisit after \ticket{207} is addressed.}
|
|
% \verb+[Coverage: 0.00%. (1000/17668470647783843295832975007429185158274838968756189 ...58121606201292619776)]+
|
|
% The coverage number on {\tt DPDist} is a clear indication on how
|
|
% wild these property can get fairly quickly. (The total number of
|
|
% cases is $2^{3*10*8} = 2^{240}$, which is a truly enormous number!)
|
|
You might be surprised that the total number of cases for this
|
|
property is $2^{3*10*8} = 2^{240}$---a truly ginormous number!
|
|
\end{Answer}
|
|
|
|
\begin{Exercise}\label{ex:aesmc:2}
|
|
Write a function
|
|
\begin{code}
|
|
gf28VectorMult : {n, m, k} (fin n) => ([n]GF28, [m][n]GF28) ->
|
|
[m]GF28
|
|
\end{code}
|
|
computing the dot-product of its first argument with each of the $m$
|
|
rows of the second argument, returning the resulting values as a
|
|
vector of $m$ elements.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aesmc:2}
|
|
\begin{code}
|
|
gf28VectorMult (v, ms) = [ gf28DotProduct(v, m) | m <- ms ]
|
|
\end{code}
|
|
\end{Answer}
|
|
|
|
\begin{Exercise}\label{ex:aesmc:3}
|
|
Write a function
|
|
\begin{code}
|
|
gf28MatrixMult : {n, m, k} (fin m) => ([n][m]GF28, [m][k]GF28)
|
|
-> [n][k]GF28
|
|
\end{code}
|
|
which multiplies the given matrices in GF($2^8$)\indGF.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aesmc:3}
|
|
We simply need to call {\tt gfVectorMult} of the previous exercise
|
|
on every row of the first matrix, after transposing the second
|
|
matrix to make sure columns are properly aligned. We
|
|
have:\indTranspose
|
|
\begin{code}
|
|
gf28MatrixMult (xss, yss) = [ gf28VectorMult(xs, yss')
|
|
| xs <- xss ]
|
|
where yss' = transpose yss
|
|
\end{code}
|
|
\end{Answer}
|
|
|
|
\todo[inline]{Remind the reader of the context again before jumping
|
|
into \texttt{MixColumns}.}
|
|
|
|
\unparagraph Now that we have the matrix multiplication machinery
|
|
built, we can code {\tt MixColumns} fairly easily. Following the
|
|
description in the AES\indAES standard~\cite[section 5.3.1]{aes}, all
|
|
we have to do is to multiply the matrix we have seen at the beginning
|
|
of this section with the state:
|
|
|
|
\begin{code}
|
|
MixColumns : State -> State
|
|
MixColumns state = gf28MatrixMult (m, state)
|
|
where m = [[2, 3, 1, 1],
|
|
[1, 2, 3, 1],
|
|
[1, 1, 2, 3],
|
|
[3, 1, 1, 2]]
|
|
\end{code}
|
|
|
|
Note that Cryptol makes no built-in assumption about row- or
|
|
column-ordering of multidimensional matrices. Of course, given
|
|
Cryptol's concrete syntax, it makes little sense to do anything but
|
|
row-based ordering.
|
|
|
|
%=====================================================================
|
|
% \section{Key expansion}
|
|
% \label{aes:keyexpansion}
|
|
\sectionWithAnswers{Key expansion}{aes:keyexpansion}
|
|
|
|
\todo[inline]{Will we push the pipeline of verification all the way
|
|
through? In particular, I'm interested in the equivalence proofs
|
|
between the various ticked and unticked versions of functions and
|
|
their composition.}
|
|
|
|
Recall from \autoref{sec:aesparams} that AES takes 128, 192, or
|
|
256-bit keys. The key is not used as-is, however. Instead, AES\indAES
|
|
expands the key into a number of round keys, called the {\em key
|
|
schedule}. Construction of the key schedule relies on a number of
|
|
auxiliary definitions, as we shall see shortly.
|
|
|
|
\paragraph*{Round constants} The AES\indAES standard refers to the constant
|
|
array {\tt Rcon} used during key expansion. For each {\tt i}, {\tt
|
|
Rcon[i]} contains 4 words, the last three being 0~\cite[section
|
|
5.2]{aes}. The first element is given by $x^{i-1}$, where
|
|
exponentiation is done using the {\tt gf28Pow} function you have
|
|
defined in Exercise~\ref{aes:subbytes}-\ref{ex:gfmi:0}. In Cryptol,
|
|
it is easiest to define {\tt Rcon} as a function:
|
|
\begin{code}
|
|
Rcon : [8] -> [4]GF28
|
|
Rcon i = [(gf28Pow (<| x |>, i-1)), 0, 0, 0]
|
|
\end{code}
|
|
|
|
\begin{Exercise}\label{ex:aeskerc:0}
|
|
By definition, AES\indAES only calls {\tt Rcon} with the parameters
|
|
ranging from 1--10. Based on this, create a table-lookup version
|
|
\begin{code}
|
|
Rcon' : [8] -> [4]GF28
|
|
\end{code}
|
|
that simply performs a look-up instead. \lhint{Use Cryptol to find out
|
|
what the elements of your table should be.}
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aeskerc:0}
|
|
Finding out the elements is easy:
|
|
\begin{Verbatim}
|
|
Cryptol> [ (Rcon i)@0 | i <- [1 .. 10] ]
|
|
[1, 2, 4, 8, 16, 32, 64, 128, 27, 54]
|
|
\end{Verbatim}
|
|
Note that we only capture the first element in each {\tt Rcon} value,
|
|
since we know that the rest are 0. We can now use this table to define
|
|
{\tt Rcon'} as follows:
|
|
\begin{code}
|
|
Rcon' i = [(rcons @ (i-1)), 0, 0, 0]
|
|
where rcons : [10]GF28
|
|
rcons = [1, 2, 4, 8, 16, 32, 64, 128, 27, 54]
|
|
\end{code}
|
|
Note that we subtract 1 before indexing into the {\tt rcons} sequence
|
|
to get the indexing right.
|
|
\end{Answer}
|
|
|
|
\begin{Exercise}\label{ex:aeskerc:1}
|
|
Write and prove a property that {\tt Rcon} and {\tt Rcon'} are
|
|
equivalent when called with numbers in the range 1--10.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aeskerc:1}
|
|
We need to write a conditional property
|
|
(\autoref{sec:condproof})\indThmCond. Below, we use the function
|
|
{\tt elem} you have defined in
|
|
Exercise~\ref{sec:recandrec}-\ref{ex:recfun:4:1}:\indElem
|
|
\begin{code}
|
|
property RconCorrect x = if elem(x, [1..10])
|
|
then Rcon x == Rcon' x
|
|
else True
|
|
\end{code}
|
|
We have:
|
|
\begin{Verbatim}
|
|
Cryptol> :prove RconCorrect
|
|
Q.E.D.
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\todo[inline]{Will we support the \texttt{:safe} command again? See
|
|
\ticket{210}. There is a commented-out exercise here on the safety
|
|
of \texttt{Rcon'}.}
|
|
% \begin{Exercise}\label{ex:aeskerc:2}
|
|
% Is {\tt Rcon'} safe? Verify your answer using Cryptol.
|
|
% \end{Exercise}
|
|
% \begin{Answer}\ansref{ex:aeskerc:2}
|
|
% No, {\tt Rcon'} is {\em not} safe by itself:
|
|
% \begin{Verbatim}
|
|
% Cryptol> :safe Rcon'
|
|
% *** 1 safety condition to be checked.
|
|
% *** Checking for violations of: ``..: index of symbolic-value is out of bounds
|
|
% (valid range is 0 thru 9).''
|
|
% *** Violation detected:
|
|
% Rcon' 0x00
|
|
% = ..: index of 255 is out of bounds
|
|
% (valid range is 0 thru 9).
|
|
% *** 1 problem found.
|
|
% \end{Verbatim}
|
|
% The premise of {\tt Rcon'} is that it must be called with numbers in
|
|
% the range 1--10. So, all its uses are actually safe, as we shall
|
|
% explore in Exercise~\ref{aes:keyexpansion}~\ref{ex:rconsafety}.
|
|
% \end{Answer}
|
|
|
|
\paragraph*{The {\ttfamily{\textbf SubWord}} function} The AES\indAES
|
|
specification refers to a function named {\tt SubWord}~\cite[section
|
|
5.2]{aes}, that takes a 32-bit word and applies the {\tt SubByte}
|
|
transformation from \autoref{aes:subbytes}. This function is
|
|
trivial to code in Cryptol:
|
|
\begin{code}
|
|
SubWord : [4]GF28 -> [4]GF28
|
|
SubWord bs = [ SubByte' b | b <- bs ]
|
|
\end{code}
|
|
Note that we have used the table-lookup version ({\tt SubByte'},
|
|
page~\pageref{aes:subbytetl}) above.
|
|
|
|
\paragraph*{The {\ttfamily{\textbf RotWord}} function} The last
|
|
function we need for key expansion is named {\tt RotWord} by the
|
|
AES\indAES standard~\cite[section 5.2]{aes}. This function merely
|
|
rotates a given word cyclically to the left:
|
|
\begin{code}
|
|
RotWord : [4]GF28 -> [4]GF28
|
|
RotWord [a0, a1, a2, a3] = [a1, a2, a3, a0]
|
|
\end{code}
|
|
We could have used \verb+<<<+\indRotLeft to implement {\tt RotWord} as
|
|
well, but the above definition textually looks exactly the one given
|
|
in the standard specification, and hence is preferable for the
|
|
purposes of clarity.
|
|
|
|
\todo[inline]{Demonstrate the use of rotate and prove the
|
|
equivalence.}
|
|
|
|
\paragraph*{The key schedule} Recall that AES\indAES operates on 128,
|
|
192, or 256 bit keys. These keys are used to construct a sequence of
|
|
so-called \emph{round keys}, each of which is 128 bits wide, and is
|
|
viewed the same way as the {\tt State}:\todo[inline]{\emph{Viewed} or
|
|
\emph{used}? Isn't this type abuse?}
|
|
\begin{code}
|
|
type RoundKey = State
|
|
\end{code}
|
|
The expanded key schedule contains {\tt Nr}+1 round-keys. (Recall
|
|
from \autoref{sec:aesparams} that {\tt Nr} is the number of
|
|
rounds.) It also helps to separate out the first and the last keys,
|
|
as they are used in a slightly different fashion. Based on this
|
|
discussion, we use the following Cryptol type to capture the
|
|
key schedule:
|
|
\begin{code}
|
|
type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey)
|
|
\end{code}
|
|
|
|
The key schedule is computed by seeding it with the initial key and
|
|
computing the successive elements from the previous entries. In
|
|
particular, the $i$th element of the expanded key is determined as
|
|
follows, copied verbatim from the AES\indAES
|
|
specification~\cite[figure 11; section 5.2]{aes}:
|
|
\begin{Verbatim}
|
|
temp = w[i-1]
|
|
if (i mod Nk = 0)
|
|
temp = SubWord(RotWord(temp)) xor Rcon[i/Nk]
|
|
else if (Nk > 6 and i mod Nk = 4)
|
|
temp = SubWord(temp)
|
|
end if
|
|
w[i] = w[i-Nk] xor temp
|
|
\end{Verbatim}
|
|
In the pseudo-code, the {\tt w} array contains the expanded key. We
|
|
are computing {\tt w[i]}, using the values {\tt w[i-1]} and {\tt
|
|
w[i-Nk]}. The result is the exclusive-or of {\tt w[i-Nk]} and a
|
|
mask value, called {\tt temp} above. The mask is computed using {\tt
|
|
w[i-1]}, the {\tt Rcon} array we have seen before, the current index
|
|
{\tt i}, and {\tt Nk}. This computation is best expressed as a
|
|
function in Cryptol that we will call {\tt NextWord}. We will name
|
|
the {\tt w[i-1]} argument {\tt prev}, and the {\tt w[i-Nk]} argument
|
|
{\tt old}. Otherwise, the Cryptol code just follows the pseudo-code
|
|
above, written in a functional style to compute the mask:
|
|
\begin{code}
|
|
NextWord : ([8],[4][8],[4][8]) -> [4][8]
|
|
NextWord(i, prev, old) = old ^ mask
|
|
where mask = if i % `Nk == 0
|
|
then SubWord(RotWord(prev)) ^ Rcon' (i / `Nk)
|
|
else if (`Nk > 6) && (i % `Nk == 4)
|
|
then SubWord(prev)
|
|
else prev
|
|
\end{code}
|
|
\note{It is well worth studying the pseudo-code above and the Cryptol
|
|
equivalent to convince yourself they are expressing the same idea!}
|
|
|
|
To compute the key schedule we start with the initial key as the
|
|
seed. We then make calls to {\tt NextWord} with a sliding window of
|
|
{\tt Nk} elements, computing the subsequent elements. Let us first
|
|
write a function that will apply this algorithm to generate an
|
|
infinite regression of elements:\indDrop\indTranspose
|
|
\begin{code}
|
|
ExpandKeyForever : [Nk][4][8] -> [inf]RoundKey
|
|
ExpandKeyForever seed = [ transpose g | g <- groupBy`{4} keyWS ]
|
|
where keyWS = seed # [ NextWord(i, prev, old)
|
|
| i <- [`Nk ...]
|
|
| prev <- drop`{Nk-1} keyWS
|
|
| old <- keyWS
|
|
]
|
|
\end{code}
|
|
Note how {\tt prev} tracks the previous 32 bits of the expanded key
|
|
(by dropping the first {\tt Nk-1} elements), while {\tt old} tracks
|
|
the {\tt i-Nk}th recurrence for {\tt keyWS}. Once we have the
|
|
infinite expansion, it is easy to extract just the amount we need by
|
|
using number of rounds ({\tt Nr}) as our guide:\indIndex\indIndexs
|
|
\begin{code}
|
|
ExpandKey : [AESKeySize] -> KeySchedule
|
|
ExpandKey key = (keys @ 0, keys @@ [1 .. (Nr - 1)], keys @ `Nr)
|
|
where seed : [Nk][4][8]
|
|
seed = split (split key)
|
|
keys = ExpandKeyForever seed
|
|
\end{code}
|
|
The call {\tt split key} chops {\tt AESKey} into {\tt [Nk*4][8]}, and
|
|
the outer call to {\tt split} further constructs the {\tt [Nk][4][8]}
|
|
elements.
|
|
|
|
\paragraph*{Testing {\ttfamily{\textbf ExpandKey}}} The completion of
|
|
{\tt ExpandKey} is an important milestone in our AES\indAES
|
|
development, and it is worth testing it before we proceed. The AES
|
|
specification has example key expansions that we can use. The
|
|
following function will be handy in viewing the output correctly
|
|
aligned:
|
|
\begin{code}
|
|
fromKS : KeySchedule -> [Nr+1][4][32]
|
|
fromKS (f, ms, l) = [ formKeyWords (transpose k)
|
|
| k <- [f] # ms # [l]
|
|
]
|
|
where formKeyWords bbs = [ join bs | bs <- bbs ]
|
|
\end{code}
|
|
Here is the example from Appendix~A.1 of the AES\indAES
|
|
specification~\cite{aes}:
|
|
\begin{Verbatim}
|
|
Cryptol> fromKS (ExpandKey 0x2b7e151628aed2a6abf7158809cf4f3c)
|
|
[[0x2b7e1516, 0x28aed2a6, 0xabf71588, 0x09cf4f3c],
|
|
[0xa0fafe17, 0x88542cb1, 0x23a33939, 0x2a6c7605],
|
|
[0xf2c295f2, 0x7a96b943, 0x5935807a, 0x7359f67f],
|
|
[0x3d80477d, 0x4716fe3e, 0x1e237e44, 0x6d7a883b],
|
|
[0xef44a541, 0xa8525b7f, 0xb671253b, 0xdb0bad00],
|
|
[0xd4d1c6f8, 0x7c839d87, 0xcaf2b8bc, 0x11f915bc],
|
|
[0x6d88a37a, 0x110b3efd, 0xdbf98641, 0xca0093fd],
|
|
[0x4e54f70e, 0x5f5fc9f3, 0x84a64fb2, 0x4ea6dc4f],
|
|
[0xead27321, 0xb58dbad2, 0x312bf560, 0x7f8d292f],
|
|
[0xac7766f3, 0x19fadc21, 0x28d12941, 0x575c006e],
|
|
[0xd014f9a8, 0xc9ee2589, 0xe13f0cc8, 0xb6630ca6]]
|
|
\end{Verbatim}
|
|
As you can verify this output matches the last column of the table in
|
|
Appendix~A.1 of the reference specification for AES.\indAES
|
|
|
|
\todo[inline]{A theorem for safety follows that we can re-introduce
|
|
after \ticket{210} is closed.}
|
|
% \begin{Exercise}\label{ex:rconsafety}
|
|
% Let us revisit Exercise~\ref{aes:keyexpansion}~\ref{ex:aeskerc:2},
|
|
% where we have seen that {\tt Rcon'} is not safe. However, the
|
|
% promise was that it would only be called with numbers ranging
|
|
% 1--10, thus all its uses would be fine. Verify this claim by
|
|
% proving {\tt ExpandKey} itself is safe. How about {\tt NextWord}?
|
|
% Is it safe?
|
|
% \end{Exercise}
|
|
% \begin{Answer}\ansref{ex:rconsafety}
|
|
% Let us first check {\tt NextWord}. We have:
|
|
% \begin{Verbatim}
|
|
% Cryptol> :safe NextWord
|
|
% *** 1 safety condition to be checked.
|
|
% *** Checking for violations of: ``..: index of symbolic-value is out of bounds
|
|
% (valid range is 0 thru 9).''
|
|
% *** Violation detected:
|
|
% NextWord (0x00, [0x00 0x00 0x00 0x00], [0x00 0x00 0x00 0x00])
|
|
% = ..: index of 255 is out of bounds
|
|
% (valid range is 0 thru 9).
|
|
% *** 1 problem found.
|
|
% \end{Verbatim}
|
|
% This is indeed to be expected, since {\tt NextWord} simply uses its
|
|
% {\tt i} argument in the call to {\tt Rcon' (i/Nk)}, and there is no
|
|
% guarantee that this {\tt i} will not be 0. However, the use from
|
|
% within {\tt ExpandKey} is perfectly fine:
|
|
% \begin{Verbatim}
|
|
% Cryptol> :safe ExpandKey
|
|
% "ExpandKey" is safe; no safety violations exist.
|
|
% \end{Verbatim}
|
|
% formally ensuring that the use of {\tt Rcon'} via {\tt NextWord} in
|
|
% {\tt ExpandKey} is indeed safe.
|
|
% \end{Answer}
|
|
|
|
%=====================================================================
|
|
\section{The {\ttfamily{\textbf AddRoundKey}} transformation}
|
|
\label{sec:ttfam-addr-transf}
|
|
|
|
{\tt AddRoundKey} is the simplest of all the transformations in
|
|
AES~\cite[section 5.1.4]{aes}.\indAES It merely amounts to the
|
|
exclusive-or of the state and the current round key:\indXOr
|
|
\begin{code}
|
|
AddRoundKey : (RoundKey, State) -> State
|
|
AddRoundKey (rk, s) = rk ^ s
|
|
\end{code}
|
|
Notice that Cryptol's {\tt \Verb|^|} operator applies structurally to
|
|
arbitrary shapes, computing the exclusive-or element-wise.
|
|
|
|
%=====================================================================
|
|
% \section{AES encryption}
|
|
% \label{sec:aes:encryption}
|
|
\sectionWithAnswers{AES encryption}{sec:aes:encryption}
|
|
|
|
We now have all the necessary machinery to perform AES\indAES
|
|
encryption.
|
|
|
|
\paragraph*{AES rounds} As mentioned before, AES performs encryption in
|
|
rounds. Each round consists of performing {\tt SubBytes}
|
|
(\autoref{aes:subbytes}), {\tt ShiftRows}
|
|
(\autoref{aes:shiftrows}), and {\tt MixColumns}
|
|
(\autoref{sec:aesmixcolumns}). Before finishing up, each round
|
|
also adds the current round key to the state~\cite[section
|
|
5.1]{aes}. The Cryptol code for the rounds is fairly trivial:
|
|
\begin{code}
|
|
AESRound : (RoundKey, State) -> State
|
|
AESRound (rk, s) = AddRoundKey (rk,
|
|
MixColumns (ShiftRows (SubBytes s)))
|
|
\end{code}
|
|
|
|
\paragraph*{The final round} The last round of AES is slightly
|
|
different than the others. It omits the {\tt MixColumns}
|
|
transformation:
|
|
\begin{code}
|
|
AESFinalRound : (RoundKey, State) -> State
|
|
AESFinalRound (rk, s) = AddRoundKey (rk, ShiftRows (SubBytes s))
|
|
\end{code}
|
|
|
|
\paragraph*{Forming the input/output blocks} Recall that AES processes
|
|
input in blocks of 128 bits, producing 128 bits of output, regardless
|
|
of the key size. We will need two helper functions to convert 128-bit
|
|
messages to and from AES states. Conversion from a message to a state
|
|
is easy to define:
|
|
\begin{code}
|
|
msgToState : [128] -> State
|
|
msgToState msg = transpose (split (split msg))
|
|
\end{code}
|
|
The first call to \texttt{split} gives us four 32-bit words, which we again
|
|
split into bytes. We then form the AES state by transposing the
|
|
resulting matrix. In the other direction, we simply transpose the
|
|
state and perform the necessary
|
|
\texttt{join}s:\indTranspose\indJoin\indReverse\indSplit
|
|
\begin{code}
|
|
stateToMsg : State -> [128]
|
|
stateToMsg st = join (join (transpose st))
|
|
\end{code}
|
|
|
|
\begin{Exercise}\label{ex:aes:enc0}
|
|
Write and prove a pair of properties stating that {\tt msgToState}
|
|
and {\tt stateToMsg} are inverses of each other.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aes:enc0}
|
|
\begin{code}
|
|
property msgToStateToMsg msg = stateToMsg(msgToState(msg)) == msg
|
|
property stToMsgToSt s = msgToState(stateToMsg s) == s
|
|
\end{code}
|
|
We have:
|
|
\begin{Verbatim}
|
|
Cryptol> :prove msgToStateToMsg
|
|
Q.E.D.
|
|
Cryptol> :prove stToMsgToSt
|
|
Q.E.D.
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\paragraph*{Putting it together} To encrypt, AES merely expands the
|
|
given key and calls the round functions. The starting state (\texttt{state0}
|
|
below) is constructed by adding the first round key to the
|
|
input. We then run all the middle rounds using a simple comprehension,
|
|
and finish up by applying the last round~\cite[figure 5, section
|
|
5.1]{aes}:\indRIndex
|
|
\begin{code}
|
|
aesEncrypt : ([128], [AESKeySize]) -> [128]
|
|
aesEncrypt (pt, key) = stateToMsg (AESFinalRound (kFinal, rounds ! 0))
|
|
where (kInit, ks, kFinal) = ExpandKey key
|
|
state0 = AddRoundKey(kInit, msgToState pt)
|
|
rounds = [state0] # [ AESRound (rk, s) | rk <- ks
|
|
| s <- rounds
|
|
]
|
|
\end{code}
|
|
|
|
\paragraph*{Testing} We can now run some test vectors. Note that, just
|
|
because a handful of test vectors pass, we cannot claim that our
|
|
implementation of AES is correct.
|
|
|
|
The first example comes from Appendix~B of the AES\indAES
|
|
standard~\cite{aes}:
|
|
\begin{Verbatim}
|
|
Cryptol> aesEncrypt (0x3243f6a8885a308d313198a2e0370734, \
|
|
0x2b7e151628aed2a6abf7158809cf4f3c)
|
|
0x3925841d02dc09fbdc118597196a0b32
|
|
\end{Verbatim}
|
|
which is what the standard asserts to be the answer. (Note that you
|
|
have to read the final box in Appendix~B column-wise!) The second
|
|
example comes from Appendix~C.1:
|
|
\begin{Verbatim}
|
|
Cryptol> aesEncrypt (0x00112233445566778899aabbccddeeff, \
|
|
0x000102030405060708090a0b0c0d0e0f)
|
|
0x69c4e0d86a7b0430d8cdb78070b4c55a
|
|
\end{Verbatim}
|
|
Again, the result agrees with the standard.
|
|
|
|
\commentout{
|
|
\begin{code}
|
|
aesEncSanityCheck = (aesEncrypt(0x3243f6a8885a308d313198a2e0370734, 0x2b7e151628aed2a6abf7158809cf4f3c) == 0x3925841d02dc09fbdc118597196a0b32) && (aesEncrypt(0x00112233445566778899aabbccddeeff, 0x000102030405060708090a0b0c0d0e0f) == 0x69c4e0d86a7b0430d8cdb78070b4c55a)
|
|
\end{code}
|
|
}
|
|
|
|
\commentout{
|
|
192 and 256 bit tests:
|
|
\begin{Verbatim}
|
|
aesEncrypt(0x00112233445566778899aabbccddeeff, 0x000102030405060708090a0b0c0d0e0f1011121314151617) == 0xdda97ca4864cdfe06eaf70a0ec0d7191
|
|
aesEncrypt(0x00112233445566778899aabbccddeeff, 0x000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f) == 0x8ea2b7ca516745bfeafc49904b496089
|
|
\end{Verbatim}
|
|
}
|
|
|
|
\paragraph*{Other key sizes} Our development of AES has been key-size
|
|
agnostic, relying on the definition of the parameter \texttt{Nk}. (See
|
|
\autoref{sec:aesparams}.) To obtain AES192, all we need is to set
|
|
\texttt{Nk} to be 6, no additional code change is needed. Similarly, we
|
|
merely need to set \texttt{Nk} to be 8 for AES256.
|
|
|
|
\begin{Exercise}\label{ex:aes192}
|
|
By setting \texttt{Nk} to be 6 and 8 respectively, try the test vectors
|
|
given in Appendices C.2 and C.3 of the AES\indAES
|
|
standard~\cite{aes}.
|
|
\end{Exercise}
|
|
|
|
%=====================================================================
|
|
% \section{Decryption}
|
|
% \label{sec:aesdecryption}
|
|
\sectionWithAnswers{Decryption}{sec:aesdecryption}
|
|
|
|
AES decryption is fairly similar to encryption, except it uses inverse
|
|
transformations~\cite[figure 12, section 5.3]{aes}. Armed with all the
|
|
machinery we have built so far, the inverse transformations are
|
|
relatively easy to define.
|
|
|
|
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
\subsection{The {\ttfamily{\textbf InvSubBytes}} transformation}
|
|
\label{sec:ttfam-invs-transf}
|
|
|
|
The {\tt InvSubBytes} transformation reverses the {\tt SubBytes}
|
|
transformation of \autoref{aes:subbytes}. As with {\tt SubBytes},
|
|
we have a choice to either do a table lookup implementation, or follow
|
|
the mathematical description. We will do the former in these examples;
|
|
you are welcome to do the latter on your own and prove the equivalence
|
|
of the two versions. To do so, we need to invert the transformation
|
|
given by:
|
|
$$
|
|
b \oplus b \ggg 4 \oplus b \ggg 5 \oplus b \ggg 6 \oplus b \ggg 7 \oplus c
|
|
$$
|
|
where $c$ is {\tt 0x63}. It turns out that the inverse of this
|
|
transformation can be computed by
|
|
$$
|
|
b \ggg 2 \oplus b \ggg 5 \oplus b \ggg 7 \oplus d
|
|
$$
|
|
where $d$ is {\tt 0x05}. It is easy to code this inverse transform in
|
|
Cryptol:
|
|
|
|
\begin{code}
|
|
xformByte' : GF28 -> GF28
|
|
xformByte' b = gf28Add [(b >>> 2), (b >>> 5), (b >>> 7), d]
|
|
where d = 0x05
|
|
\end{code}
|
|
|
|
\begin{Exercise}\label{ex:invsb:1}
|
|
Write and prove a Cryptol property stating that {\tt xformByte'} is
|
|
the inverse of the function {\tt xformByte} that you have defined in
|
|
Exercise~\ref{aes:subbytes}~\ref{ex:aessbytes:0}.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:invsb:1}
|
|
\begin{code}
|
|
property xformByteInverse x = xformByte' (xformByte x) == x
|
|
\end{code}
|
|
We have:
|
|
\begin{Verbatim}
|
|
Cryptol> :prove xformByteInverse
|
|
Q.E.D.
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\unparagraph We can now define the inverse S-box
|
|
transform,\indAESInvSbox using the multiplicative inverse function
|
|
{\tt gf28Inverse} you have defined in
|
|
Exercise~\ref{aes:subbytes}~\ref{ex:gfmi:01}:
|
|
\begin{code}
|
|
InvSubByte : GF28 -> GF28
|
|
InvSubByte b = gf28Inverse (xformByte' b)
|
|
|
|
InvSubBytes : State -> State
|
|
InvSubBytes state = [ [ InvSubByte b | b <- row ]
|
|
| row <- state
|
|
]
|
|
\end{code}
|
|
|
|
\begin{Exercise}\label{ex:invsb:2}
|
|
Write and prove a Cryptol property showing that {\tt InvSubByte}
|
|
reverses {\tt SubByte}.\indAESSbox
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:invsb:2}
|
|
\begin{code}
|
|
property sboxInverse s = InvSubBytes (SubBytes s) == s
|
|
\end{code}
|
|
We have:
|
|
\begin{Verbatim}
|
|
Cryptol> :prove xformByteInverse
|
|
Q.E.D.
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\begin{Exercise}\label{ex:invsb:3}
|
|
The AES specification provides an inverse S-box table~\cite[figure
|
|
14, section 5.3.2]{aes}. Write a Cryptol function {\tt InvSubBytes'}
|
|
using the table lookup technique. Make sure your implementation is
|
|
correct (i.e., equivalent to {\tt InvSubBytes}) by writing and
|
|
proving a corresponding property.
|
|
\end{Exercise}
|
|
|
|
\subsection{The {\ttfamily{\textbf InvShiftRows}} transformation}
|
|
\label{sec:ttfam-invsh-transf}
|
|
|
|
The {\tt InvShiftRows} transformation\indAESInvShiftRows simply
|
|
reverses the {\tt ShiftRows}\indAESShiftRows transformation from
|
|
\autoref{aes:shiftrows}:
|
|
|
|
\begin{code}
|
|
InvShiftRows : State -> State
|
|
InvShiftRows state = [ row >>> shiftAmount
|
|
| row <- state
|
|
| shiftAmount <- [0 .. 3]
|
|
]
|
|
\end{code}
|
|
|
|
\begin{Exercise}\label{ex:aesisr:0}
|
|
Write and prove a property stating that {\tt InvShiftRows} is the
|
|
inverse of {\tt ShiftRows}.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aesisr:0}
|
|
\begin{code}
|
|
property shiftRowsInverse s = InvShiftRows (ShiftRows s) == s
|
|
\end{code}
|
|
We have:
|
|
\begin{Verbatim}
|
|
Cryptol> :prove shiftRowsInverse
|
|
Q.E.D.
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\subsection{The {\ttfamily{\textbf InvMixColumns}} transformation}
|
|
\label{sec:ttfam-invm-transf}
|
|
|
|
Recall from \autoref{sec:aesmixcolumns} that {\tt
|
|
MixColumns}\indAESMixColumns amounts to matrix multiplication in
|
|
GF($2^8$).\indGF The inverse transform turns out to be the same,
|
|
except with a different matrix:\indAESInvMixColumns
|
|
|
|
\begin{code}
|
|
InvMixColumns : State -> State
|
|
InvMixColumns state = gf28MatrixMult (m, state)
|
|
where m = [[0x0e, 0x0b, 0x0d, 0x09],
|
|
[0x09, 0x0e, 0x0b, 0x0d],
|
|
[0x0d, 0x09, 0x0e, 0x0b],
|
|
[0x0b, 0x0d, 0x09, 0x0e]]
|
|
\end{code}
|
|
|
|
\begin{Exercise}\label{ex:aesimc:0}
|
|
Write and prove a property stating that {\tt InvMixColumns} is the
|
|
inverse of {\tt MixColumns}.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:aesimc:0}
|
|
\begin{code}
|
|
property mixColumnsInverse s = InvMixColumns (MixColumns s) == s
|
|
\end{code}
|
|
Unlike others, this property is harder to prove automatically and will
|
|
take much longer. Below we show the {\tt :check} results instead:
|
|
\begin{Verbatim}
|
|
Cryptol> :check mixColumnsInverse
|
|
Checking case 1000 of 1000 (100.00%)
|
|
1000 tests passed OK
|
|
\end{Verbatim}
|
|
|
|
\todo[inline]{Reflect upon coverage, in relation to \ticket{207}.}
|
|
% \verb+[Coverage: 0.00%. (1000/340282366920938463463374607431768211456)]+.
|
|
% The coverage information is an indication of the magnitude of the
|
|
% problem we are dealing with.}
|
|
\end{Answer}
|
|
|
|
%=====================================================================
|
|
\section{The inverse cipher}
|
|
\label{sec:inverse-cipher}
|
|
|
|
We now also have all the ingredients to encode AES decryption.
|
|
Following figure~12 (section 5.3) of the AES\indAES
|
|
standard~\cite{aes}: {\small
|
|
\begin{code}
|
|
AESInvRound : (RoundKey, State) -> State
|
|
AESInvRound (rk, s) =
|
|
InvMixColumns (AddRoundKey (rk, InvSubBytes (InvShiftRows s)))
|
|
|
|
AESFinalInvRound : (RoundKey, State) -> State
|
|
AESFinalInvRound (rk, s) = AddRoundKey (rk, InvSubBytes (InvShiftRows s))
|
|
|
|
aesDecrypt : ([128], [AESKeySize]) -> [128]
|
|
aesDecrypt (ct, key) = stateToMsg (AESFinalInvRound (kFinal, rounds ! 0))
|
|
where
|
|
(kFinal, ks, kInit) = ExpandKey key
|
|
state0 = AddRoundKey(kInit, msgToState ct)
|
|
rounds = [state0] # [ AESInvRound (rk, s)
|
|
| rk <- reverse ks
|
|
| s <- rounds
|
|
]
|
|
\end{code}
|
|
}
|
|
|
|
Note how we use the results of {\tt ExpandedKey}, by carefully naming
|
|
the first and last round keys and using the middle keys in reverse.
|
|
|
|
\paragraph*{Testing} Let us repeat the tests for AES encryption. Again,
|
|
the first example comes from Appendix~B of the AES\indAES
|
|
standard~\cite{aes}:
|
|
\begin{Verbatim}
|
|
Cryptol> aesDecrypt (0x3925841d02dc09fbdc118597196a0b32, \
|
|
0x2b7e151628aed2a6abf7158809cf4f3c)
|
|
0x3243f6a8885a308d313198a2e0370734
|
|
\end{Verbatim}
|
|
which agrees with the original value. The second example comes from
|
|
Appendix~C.1:
|
|
\begin{Verbatim}
|
|
Cryptol> aesDecrypt (0x69c4e0d86a7b0430d8cdb78070b4c55a, \
|
|
0x000102030405060708090a0b0c0d0e0f)
|
|
0x00112233445566778899aabbccddeeff
|
|
\end{Verbatim}
|
|
Again, the result agrees with the standard.
|
|
|
|
\commentout{
|
|
\begin{code}
|
|
aesDecSanityCheck = (aesDecrypt(0x3925841d02dc09fbdc118597196a0b32, 0x2b7e151628aed2a6abf7158809cf4f3c) == 0x3243f6a8885a308d313198a2e0370734) && (aesDecrypt(0x69c4e0d86a7b0430d8cdb78070b4c55a, 0x000102030405060708090a0b0c0d0e0f) == 0x00112233445566778899aabbccddeeff)
|
|
\end{code}
|
|
}
|
|
|
|
\commentout{
|
|
192 and 256 bit tests:
|
|
\begin{Verbatim}
|
|
aesDecrypt(0xdda97ca4864cdfe06eaf70a0ec0d7191, 0x000102030405060708090a0b0c0d0e0f1011121314151617) == 0x00112233445566778899aabbccddeeff
|
|
aesDecrypt(0x8ea2b7ca516745bfeafc49904b496089, 0x000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f) == 0x00112233445566778899aabbccddeeff
|
|
\end{Verbatim}
|
|
}
|
|
|
|
\paragraph*{Other key sizes} Similar to encryption, all we need to
|
|
obtain AES192 decryption is to set {\tt Nk} to be 6 in
|
|
section~\ref{sec:aesparams}. Setting {\tt Nk} to 8 will
|
|
correspondingly give us AES256.
|
|
|
|
\paragraph*{The code} You can see all the Cryptol code for AES in
|
|
Appendix~\ref{app:aes}.
|
|
|
|
%=====================================================================
|
|
\section{Correctness}
|
|
\label{sec:aescorrectattempt}
|
|
|
|
While test vectors do provide good evidence of AES\indAES working
|
|
correctly, they do not provide a proof that we have implemented the
|
|
standard faithfully. In fact, for a block cipher like AES, it is not
|
|
possible to state what correctness would mean. Tweaking some
|
|
parameters, or changing the S-box appropriately can give us a brand
|
|
new cipher. And it would be impossible to tell this new cipher apart
|
|
from AES aside from running it against published test vectors.
|
|
|
|
\todo[inline]{Is this claim about correctness really true?!}
|
|
|
|
What we can do, however, is gain assurance that our implementation
|
|
demonstrably has the desired properties. We have done this throughout
|
|
this chapter by stating and proving a number of properties about AES
|
|
and its constituent parts. The Cryptol methodology allows us to
|
|
construct the code together with expected properties, allowing
|
|
high-assurance development. We conclude this chapter with one final
|
|
property, stating that {\tt aesEncrypt} and {\tt aesDecrypt} do indeed
|
|
form an encryption-decryption pair:
|
|
|
|
\begin{code}
|
|
property AESCorrect msg key = aesDecrypt (aesEncrypt (msg, key), key) == msg
|
|
\end{code}
|
|
|
|
Can we hope to automatically prove this theorem? For 128-bit AES, the
|
|
state space for this theorem has $2^{256}$ elements. It would be
|
|
naive to expect that we can prove this theorem by a push-button tool
|
|
very quickly.\footnote{Note that, for a general algorithm with this
|
|
large a state space, it is entirely possible to perform automatic
|
|
verification using modern solvers, but if one carefully reflects
|
|
upon the nature of cryptographic functions, it becomes clear why it
|
|
should \emph{not} be the case here.} We can however, gain some
|
|
assurance by running it through the {\tt :check} command:\indCmdCheck
|
|
|
|
\begin{Verbatim}
|
|
Checking case 1000 of 1000 (100.00%)
|
|
1000 tests passed OK
|
|
\end{Verbatim}
|
|
\todo[inline]{The \texttt{:check} output here is out of date.}
|
|
% [Coverage: 0.00%. (1000/11579208923731619542357098500868790785326998466564
|
|
% ...0564039457584007913129639936)]
|
|
You will notice that even running quick-check will take a while for
|
|
the above theorem, and the total state space for this function means
|
|
that we have not even scratched the surface! That said, being able to
|
|
specify these properties together with very high level code is what
|
|
distinguishes Cryptol from other languages when it comes to
|
|
cryptographic algorithm programming.
|
|
|
|
\todo[inline]{This is highly dissatisfying!}
|
|
|
|
\todo[inline]{Add some text here back when we improve proof
|
|
capabilities?}
|
|
%% Furthermore, Cryptol has some further proof tools in its arsenal
|
|
%% that will actually let us complete this proof in a reasonable
|
|
%% amount of time, as we shall see in \autoref{sec:proveaes}.
|
|
\commentout{
|
|
\begin{code}
|
|
sanityCheck = (aesEncrypt (0x3243f6a8885a308d313198a2e0370734, 0x2b7e151628aed2a6abf7158809cf4f3c)
|
|
== 0x3925841d02dc09fbdc118597196a0b32)
|
|
&&
|
|
(aesEncrypt (0x00112233445566778899aabbccddeeff, 0x000102030405060708090a0b0c0d0e0f)
|
|
== 0x69c4e0d86a7b0430d8cdb78070b4c55a)
|
|
\end{code}
|
|
}
|
|
|
|
\todo[inline]{Need a punchier conclusion to the chapter, since it ends
|
|
the book, or add a new conclusion.}
|
|
|
|
%%% Local Variables:
|
|
%%% mode: latex
|
|
%%% TeX-master: "../main/Cryptol"
|
|
%%% End:
|