mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
349 lines
10 KiB
TeX
349 lines
10 KiB
TeX
%
|
|
% Programming in Cryptol
|
|
% Galois, Inc.
|
|
% Levent Erkok, Dylan McNamee, Joseph Kiniry, and others
|
|
%
|
|
|
|
\documentclass[twoside]{book}
|
|
\usepackage{amsfonts}
|
|
\usepackage{xspace}
|
|
\usepackage{url}
|
|
\usepackage{subfigure}
|
|
\usepackage{graphicx}
|
|
\usepackage{lastpage}
|
|
\usepackage{makeidx}
|
|
\usepackage[myheadings]{fullpage}
|
|
\usepackage{verbatim}
|
|
\usepackage{fancyvrb}
|
|
\usepackage{booktabs}
|
|
\usepackage{amsmath, amsthm, amssymb}
|
|
\usepackage{fancyhdr}
|
|
\usepackage{xcolor}
|
|
\usepackage{pdfpages}
|
|
\usepackage[answerdelayed,lastexercise]{utils/exercise}
|
|
\usepackage[xetex,bookmarks=true,pagebackref=true,linktocpage=false]{hyperref}
|
|
\usepackage[style=list]{utils/glossary}
|
|
\usepackage{adjustbox}
|
|
\usepackage{xparse}
|
|
|
|
%% choose output pagesize. Here are two options:
|
|
%% Half of a US Letter sheet, (or A5 paper)
|
|
%% intended to be folded in half and bound in a book
|
|
% for half-letter:
|
|
%\usepackage[paperwidth=5.5in,paperheight=8.5in,inner=62pt,outer=34pt]{geometry}
|
|
%\setlength{\textheight}{502pt}
|
|
|
|
% for full-letter
|
|
\usepackage[paperwidth=8.5in,paperheight=11in,inner=62pt,outer=34pt]{geometry}
|
|
\setlength{\textheight}{652pt}
|
|
|
|
\newcommand{\titleline}{Programming in Cryptol}
|
|
|
|
\hypersetup{%
|
|
pdftitle = \titleline,
|
|
pdfkeywords = {Cryptol, Cryptography, Programming},
|
|
pdfauthor = {Levent Erk\"{o}k and others at Galois},
|
|
pdfpagemode = UseOutlines
|
|
}
|
|
|
|
\RequirePackage[12tabu,orthodox]{nag}
|
|
\input{utils/Indexes.tex}
|
|
\input{utils/GlossaryItems.tex}
|
|
\input{utils/trickery.tex}
|
|
|
|
% fonts
|
|
\usepackage[TS1,T1]{fontenc}
|
|
\usepackage{microtype}
|
|
\usepackage[osf]{mathpazo}
|
|
\usepackage{fontspec}
|
|
\usepackage{xunicode}
|
|
\usepackage{xltxtra}
|
|
\defaultfontfeatures{Mapping=tex-text}
|
|
%\setmainfont[]{Times}
|
|
%\setsansfont[]{Helvetica}
|
|
%\setmonofont[Scale=0.85]{Courier}
|
|
\usepackage{sectsty}
|
|
\usepackage[disable]{todonotes}
|
|
\allsectionsfont{\sffamily}
|
|
|
|
%% Commands for checking REPL
|
|
\DefineVerbatimEnvironment
|
|
{replinVerb}{Verbatim}
|
|
{}
|
|
\DefineVerbatimEnvironment
|
|
{reploutVerb}{Verbatim}
|
|
{}
|
|
\DefineVerbatimEnvironment
|
|
{replPrompt}{Verbatim}
|
|
{}
|
|
\CustomVerbatimCommand{\replin}{Verb}{}
|
|
\CustomVerbatimCommand{\replout}{Verb}{}
|
|
\NewDocumentCommand{\hidereplin}{r||}{}
|
|
\NewDocumentCommand{\hidereplout}{r||}{}
|
|
\newcommand{\restartrepl}[0]{}{}
|
|
|
|
% \newcommand{\todo}[1]{\begin{center}\framebox{\begin{minipage}{0.8\textwidth}{{\bf TODO:} #1}\end{minipage}}\end{center}}
|
|
\newcommand{\lamex}{\ensuremath{\lambda}-expression\indLamExp}
|
|
\newcommand{\lamexs}{\ensuremath{\lambda}-expressions\indLamExp}
|
|
\makeatletter
|
|
\def\imod#1{\allowbreak\mkern10mu({\operator@font mod}\,\,#1)}
|
|
\makeatother
|
|
\newcommand{\advanced}{\begin{center}\framebox{\begin{minipage}{0.95\textwidth}{{\bf Note:} The material in this section
|
|
is aimed for the more advanced reader. It can be skipped on a first reading without loss of continuity.}\end{minipage}}\end{center}}
|
|
|
|
\newcommand{\sectionWithAnswers}[2]{%
|
|
\section{#1}\label{#2}%
|
|
\AnswerBoxSectionMark{Section \arabic{chapter}.\arabic{section} #1 (p.~\pageref{#2})}%
|
|
\AnswerBoxExecute{\addcontentsline{toc}{section}{\texorpdfstring{\parbox{2.3em}{\arabic{chapter}.\arabic{section}\ }}{(\arabic{chapter}.\arabic{section})\ }#1}}%
|
|
}
|
|
|
|
\newcommand{\commentout}[1]{}
|
|
\DefineVerbatimEnvironment{code}{Verbatim}{}
|
|
\renewcommand{\ExerciseHeaderTitle}{\ExerciseTitle}
|
|
\renewcommand{\theExercise}{\thechapter.\arabic{Exercise}}
|
|
%\renewcommand{\theExercise}{\thesection--\arabic{Exercise}}
|
|
\renewcommand{\ExerciseHeader}{\textbf{\hspace*{-\parindent}\ExerciseName\ \theExercise.\ }}
|
|
\renewcommand{\AnswerHeader}{\textbf{\hspace*{-\parindent}\ExerciseName\ \theExercise.\ }}
|
|
%\renewcounter{Exercise}[section]
|
|
\renewcounter{Exercise}[chapter]
|
|
\newcommand{\unparagraph}{\paragraph{$\,\,\,$\hspace*{-\parindent}}}
|
|
\newcommand{\exerciseref}[1]{\hyperref[#1]{exercise~\ref*{#1}}}
|
|
|
|
% various little text sections:
|
|
\newtheorem*{hint}{Hint}
|
|
\newcommand{\note}[1]{\vspace{5mm}{\setlength{\parindent}{0pt}{\bf Note:~}{#1}}}
|
|
\newcommand{\tip}[1]{\vspace{5mm}{\setlength{\parindent}{0pt}{\bf Tip:~}{#1}}}
|
|
\newcommand{\lhint}[1]{({\bf Hint}\ #1)}
|
|
\newcommand{\ansref}[1]{{\bf (p.~\pageref{#1})}}
|
|
%% not needed:?
|
|
\setlength{\voffset}{-1cm}
|
|
|
|
\setlength{\headsep}{2cm}
|
|
\setlength{\headheight}{15.2pt}
|
|
\renewcommand{\headrulewidth}{0pt} % no line on top
|
|
\renewcommand{\footrulewidth}{.5pt} % line on bottom
|
|
\renewcommand{\chaptermark}[1]{\markboth{#1}{}}
|
|
\renewcommand{\sectionmark}[1]{\markright{#1}{}}
|
|
\cfoot{}
|
|
\fancyfoot[LE,RO]{\fancyplain{}{\textsf{\thepage}}}
|
|
\fancyfoot[LO,RE]{\fancyplain{}{\textsf{\copyright\ 2010--2018, Galois, Inc.}}}
|
|
%% \fancyhead[LE]{\fancyplain{}{\textsf{\draftdate}}}
|
|
%% \fancyhead[RO]{\fancyplain{}{\textsf{DO NOT DISTRIBUTE!}}}
|
|
\fancyhead[RO,LE]{\fancyplain{}{}} %% outer
|
|
%\fancyhead[LO,RE]{\fancyplain{}{\textsf{\nouppercase{\rightmark}}}}
|
|
\fancyhead[LO,RE]{\fancyplain{}{\textsf{\nouppercase{\rightmark}}}} %% inner
|
|
\pagestyle{fancyplain}
|
|
|
|
\makeglossary
|
|
\makeindex
|
|
|
|
\begin{document}
|
|
|
|
\title{\Huge{\bf \titleline}}
|
|
\author{\\$ $\\$ $\\
|
|
Levent Erk\"{o}k\\
|
|
%\url{levent.erkok@galois.com}
|
|
\\$ $\\
|
|
Galois, Inc.\\
|
|
421 SW 6th Ave., Suite 300\\Portland, OR 97204}
|
|
\date{
|
|
\vspace*{2cm}$ $\\
|
|
\includegraphics{utils/galois.jpg}
|
|
}
|
|
|
|
\pagenumbering{roman}
|
|
|
|
%% for full-size papersize:
|
|
\includepdf[offset=0 -28]{cover/CryptolCover.pdf}
|
|
|
|
%% for A5 / half-letter papersize:
|
|
% \includepdf[offset=0 -28]{cover/CryptolSmallCover.pdf}
|
|
|
|
|
|
% \maketitle
|
|
|
|
\index{inference|see{type, inference}}
|
|
\index{signature|see{type, signature}}
|
|
\index{polymorphism|see{type, polymorphism}}
|
|
\index{monomorphism|see{type, monomorphism}}
|
|
\index{overloading|see{type, overloading}}
|
|
\index{undecidable|see{type, undecidable}}
|
|
\index{predicates|see{type, predicates}}
|
|
\index{defaulting|see{type, defaulting}}
|
|
\index{fin@\texttt{fin}|see{type, fin}}
|
|
\index{ambiguous constraints|see{type, ambiguous}}
|
|
\index{wildcard|see{\texttt{\_} (underscore)}}
|
|
\index{lambda expression|see{\ensuremath{\lambda}-expression}}
|
|
\index{pdiv@\texttt{pdiv}|see{polynomial, division}}
|
|
\index{pmod@\texttt{pmod}|see{polynomial, modulus}}
|
|
\index{pmult@\texttt{pmult}|see{polynomial, multiplication}}
|
|
\index{000GF28@GF($2^8$)|see{galois field}}
|
|
|
|
\setlength{\headsep}{24pt}
|
|
% \layout
|
|
|
|
%%%%%% PREFACE
|
|
%\input{preface/Preface.tex}
|
|
\input{preface/Notice.tex}
|
|
|
|
%%%%%% TOC
|
|
\tableofcontents
|
|
|
|
\includepdf[pages={1}]{cover/Blank.pdf}
|
|
\newpage
|
|
|
|
\setcounter{page}{1}
|
|
\pagenumbering{arabic}
|
|
%%%%%% Crash Course
|
|
\input{crashCourse/CrashCourse.tex}
|
|
\commentout{
|
|
\begin{code}
|
|
include "../crashCourse/CrashCourse.tex";
|
|
\end{code}
|
|
}
|
|
|
|
%%%%%% Transposition ciphers
|
|
\input{classic/Classic.tex}
|
|
\commentout{
|
|
\begin{code}
|
|
include "../classic/Classic.tex";
|
|
\end{code}
|
|
}
|
|
|
|
%%%%%% Enigma
|
|
\input{enigma/Enigma.tex}
|
|
\commentout{
|
|
\begin{code}
|
|
include "../enigma/Enigma.tex";
|
|
\end{code}
|
|
}
|
|
|
|
%%%%%% High assurance
|
|
\input{highAssurance/HighAssurance.tex}
|
|
\commentout{
|
|
\begin{code}
|
|
include "../highAssurance/HighAssurance.tex";
|
|
\end{code}
|
|
}
|
|
|
|
%%%%%% DES
|
|
% \chapter{DES: The Data Encryption Standard}
|
|
|
|
%%%%%% AES
|
|
\input{aes/AES.tex}
|
|
\commentout{
|
|
\begin{code}
|
|
include "../aes/AES.tex";
|
|
\end{code}
|
|
}
|
|
|
|
%%%%%% SHA
|
|
% \chapter{SHA: The Secure Hash Algorithm}
|
|
|
|
%\chapter{Advanced proof techniques}
|
|
%\section{Assumed equality}
|
|
%\section{Uninterpreted functions}
|
|
%\section{Proving AES correct}\label{sec:proveaes}
|
|
%In \autoref{sec:aescorrectattempt}, we wrote down the below Cryptol theorem stating that our AES\indAES encryption/decryption functions work correctly:
|
|
%\begin{Verbatim}
|
|
% theorem AESCorrect: {msg key}. aesDecrypt (aesEncrypt (msg, key), key) == msg;
|
|
%\end{Verbatim}
|
|
|
|
% However, we were not able to do an automated proof of this fact, as it is beyond the scope of what SAT-based equivalence checkers can handle. In this
|
|
% section we will use our new tools to attack this problem and actually complete the proof in a reasonable amount of time.
|
|
|
|
%%%%%% SAT solving
|
|
% \chapter{Using satisfiability solvers: Solving Sudoku and N-Queens in Cryptol}\label{chap:usingsat}
|
|
|
|
%%%%%% Hardware
|
|
% \chapter{Generating and proving hardware correct}
|
|
|
|
%%%%%% Pitfalls
|
|
% \chapter{Pitfalls}
|
|
% \section{Defaulting}\label{sec:pitfall:defaulting}
|
|
% \todo{Talk about defaulting gotchas}
|
|
% \section{Evaluation order}\label{sec:pitfall:evorder}
|
|
% \todo{Talk about there's no short-circuit except for if-then-else, although models might differ.}
|
|
% \section{Theorems and safety checking}\label{sec:pitfall:thmexceptions}
|
|
% \todo{Talk about safety failures and theorems}
|
|
% \todo{Talk about why {\tt implies (x, y) = if x then y else False} is not a substitute for {\tt if-then-else}}
|
|
% \todo{Talk about assumeSafe}
|
|
|
|
%%%%%% Toolbox
|
|
% \chapter{Programmer's toolbox}
|
|
% \section{Pretty printing using {\tt format}}
|
|
% \section{Debugging code using {\tt trace}}
|
|
|
|
%%%%%% Miscallaneous
|
|
% \input{misc/Misc.tex}
|
|
% \commentout{
|
|
% \begin{code}
|
|
% include "../misc/Misc.tex";
|
|
% \end{code}
|
|
% }
|
|
|
|
\appendix
|
|
% \fancyhead[LO,RE]{\fancyplain{}{\textsf{\nouppercase{\leftmark}}}}
|
|
\fancyhead[LO,RE]{\fancyplain{}{}}
|
|
|
|
%%%% Solutions
|
|
\chapter{Solutions to selected exercises}
|
|
As with any language, there are usually multiple ways to write the same
|
|
function in Cryptol. We have tried to use the most idiomatic
|
|
Cryptol code segments in our solutions. Note that Cryptol prints
|
|
numbers out in hexadecimal by default. In most of the answers below, we
|
|
have implicitly used the command {\tt :set base=10} to print numbers
|
|
out in decimal for readability.\indSettingBase
|
|
\shipoutAnswer
|
|
|
|
%%%% Cryptol primitives
|
|
\input{prims/Primitives.tex}
|
|
\commentout{
|
|
\begin{code}
|
|
include "../prims/Primitives.tex";
|
|
\end{code}
|
|
}
|
|
|
|
%%%% Enigma code
|
|
\input{enigma/EnigmaCode.tex}
|
|
\commentout{
|
|
\begin{code}
|
|
include "../enigma/EnigmaCode.tex";
|
|
\end{code}
|
|
}
|
|
|
|
%%%% AES code
|
|
\input{aes/AESCode.tex}
|
|
\commentout{
|
|
\begin{code}
|
|
include "../aes/AESCode.tex";
|
|
\end{code}
|
|
}
|
|
|
|
%%%% Language description & REPL commands
|
|
\input{technicalities/TechAppendix.tex}
|
|
|
|
%%%% Syntax (& Grammar someday)
|
|
\input{appendices/grammar.tex}
|
|
|
|
%%%% Glossary
|
|
\printglossary
|
|
\addcontentsline{toc}{chapter}{Glossary}
|
|
|
|
%%%% Bibliography
|
|
\bibliography{bib/cryptol}
|
|
\bibliographystyle{plain}
|
|
|
|
%%%% Index
|
|
\printindex
|
|
|
|
%%%% sanity checks
|
|
% \commentout{
|
|
% \begin{code}
|
|
% isEverythingSane = ~zero == checks
|
|
% where checks = [aesEncSanityCheck aesDecSanityCheck];
|
|
% \end{code}
|
|
% }
|
|
|
|
\end{document}
|