mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 13:01:31 +03:00
30 lines
856 B
TeX
30 lines
856 B
TeX
\chapter{AES in Cryptol}\label{app:aes}
|
|
|
|
In this appendix we present the Cryptol code for the AES\indAES in its
|
|
entirety for reference purposes.
|
|
\hyperref[chapter:aes]{Chapter~\ref*{chapter:aes}} has a detailed
|
|
discussion on how AES works, and the construction of the Cryptol model
|
|
below.
|
|
|
|
In the below code, simply set {\tt Nk} to be 4 for AES128, 6 for
|
|
AES192, and 8 for AES256 on line 19. No other modifications are
|
|
required for obtaining these AES variants. Note that we have
|
|
rearranged the code given in \autoref{chapter:aes} below for ease
|
|
of reading.
|
|
%% and eliminated the theorem declarations for simplicity.
|
|
|
|
\fvset{fontsize=\footnotesize}
|
|
\VerbatimInput[numbers=left]{aes/AES.cry}
|
|
\commentout{
|
|
\begin{code}
|
|
AESEncapsulated = {
|
|
include "AES.cry";
|
|
};
|
|
\end{code}
|
|
}
|
|
|
|
%%% Local Variables:
|
|
%%% mode: latex
|
|
%%% TeX-master: "../main/Cryptol"
|
|
%%% End:
|