mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
775 lines
33 KiB
TeX
775 lines
33 KiB
TeX
\chapter{The Enigma machine}
|
|
\label{chapter:enigma}
|
|
|
|
The Enigma machine is probably the most famous of all cryptographic
|
|
devices in history, due to the prominent role it played in
|
|
WWII~\cite{wiki:enigma}.\indEnigma The first Enigma machines were
|
|
available around 1920s, with various models in the market for
|
|
commercial use. When Germans used the Enigma during WWII, they were
|
|
using a particular model referred to as the {\em Wehrmacht Enigma}, a
|
|
fairly advanced model available at the time.
|
|
|
|
The most important role of Enigma\indEnigma is in its role in the use
|
|
of automated machines to aid in secret communication, or what is known
|
|
as \emph{mechanizing secrecy}. One has to understand that computers
|
|
as we understand them today were not available when Enigma was in
|
|
operation. Thus, the Enigma employed a combination of mechanical
|
|
(keyboard, rotors, etc.) and electrical parts (lamps, wirings, etc.)
|
|
to implement its functionality. However, our focus in this chapter
|
|
will not be on the mechanical aspects of Enigma at all. For a highly
|
|
readable account of that, we refer the reader to Singh's excellent
|
|
book on cryptography~\cite{Singh:1999:CBE}. Instead, we will model
|
|
Enigma in Cryptol in an algorithmic sense, implementing Enigma's
|
|
operations without any reference to the underlying mechanics. More
|
|
precisely, we will model an Enigma machine that has a plugboard, three
|
|
interchangeable scramblers, and a fixed reflector.
|
|
|
|
\todo[inline]{Add a photo or two of some Enigmas here. Look into the
|
|
WikiCommons.}
|
|
|
|
\todo[inline]{Provide an architectural diagram of this Cryptol
|
|
construction somewhere reasonable and refer to it regularly to give
|
|
the reader a better big-picture of how the spec hangs together
|
|
vs.~the actual machine.}
|
|
|
|
%=====================================================================
|
|
% \section{The plugboard}
|
|
% \label{sec:enigma:plugboard}
|
|
\sectionWithAnswers{The plugboard}{sec:enigma:plugboard}
|
|
|
|
Enigma essentially implements a polyalphabetic substitution cipher
|
|
(\autoref{section:subst})\indPolyAlphSubst, consisting of a number
|
|
of rotating units that jumble up the alphabet. The first component is
|
|
the so called plugboard (\textit{Steckerbrett} in
|
|
German)\indEnigmaPlugboard. In the original Enigma, the plugboard
|
|
provided a means of interchanging 6 pairs of letters. For instance,
|
|
the plugboard could be set-up so that pressing the {\tt B} key would
|
|
actually engage the {\tt Q} key, etc. We will slightly generalize and
|
|
allow any number of pairings, as we are not limited by the
|
|
availability of cables or actual space to put them in a box! Viewed in
|
|
this sense, the plugboard is merely a permutation of the alphabet. In
|
|
Cryptol, we can represent the plugboard combination by a string of 26
|
|
characters, corresponding to the pairings for each letter in the
|
|
alphabet from {\tt A} to {\tt Z}:
|
|
|
|
\begin{code}
|
|
type Permutation = String 26
|
|
type Plugboard = Permutation
|
|
\end{code}
|
|
For instance, the plugboard matching the pairs {\tt A}-{\tt H}, {\tt
|
|
C}-{\tt G}, {\tt Q}-{\tt X}, {\tt T}-{\tt V}, {\tt U}-{\tt Y}, {\tt
|
|
W}-{\tt M}, and {\tt O}-{\tt L} can be created as follows:
|
|
\begin{code}
|
|
plugboard : Plugboard
|
|
plugboard = "HBGDEFCAIJKOWNLPXRSVYTMQUZ"
|
|
\end{code}
|
|
Note that if a letter is not paired through the plugboard, then it
|
|
goes untouched, i.e., it is paired with itself.
|
|
|
|
\begin{Exercise}\label{ex:enigma:1}
|
|
Use Cryptol to verify that the above plugboard definition indeed
|
|
implements the pairings we wanted.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:enigma:1}
|
|
We can simply ask Cryptol what the implied mappings are:
|
|
\begin{Verbatim}
|
|
Cryptol> [ plugboard @ (c - 'A') | c <- "ACQTUWO" ]
|
|
"HGXVYML"
|
|
\end{Verbatim}
|
|
Why do we subtract the {\tt 'A'} when indexing?
|
|
\end{Answer}
|
|
|
|
\note{In Enigma, the plugboard pairings are symmetric; if {\tt A} maps
|
|
to {\tt H}, then {\tt H} must map to {\tt A}.}
|
|
|
|
%=====================================================================
|
|
% \section{Scrambler rotors}
|
|
% \label{sec:enigma:scramblerrotors}
|
|
\sectionWithAnswers{Scrambler rotors}{sec:enigma:scramblerrotors}
|
|
|
|
The next component of the Enigma are the rotors that scramble the
|
|
letters. Rotors (\textit{walzen} in German)\indEnigmaRotor are
|
|
essentially permutations, with one little twist: as their name
|
|
implies, they rotate. This rotation ensures that the next character
|
|
the rotor will process will be encrypted using a different alphabet,
|
|
thus giving Enigma its polyalphabetic nature.\indPolyAlphSubst
|
|
|
|
The other trick employed by Enigma is how the rotations are done. In a
|
|
typical setup, the rotors are arranged so that the first rotor rotates
|
|
at every character, while the second rotates at every 26th, the third
|
|
at every 676th ($=26*26$), etc. In a sense, the rotors work like the
|
|
odometer in your car, one full rotation of the first rotor triggers
|
|
the second, whose one full rotation triggers the third, and so on. In
|
|
fact, more advanced models of Enigma allowed for two notches per
|
|
rotor, i.e., two distinct positions on the rotor that will allow the
|
|
next rotor in sequence to rotate itself. We will allow ourselves to
|
|
have any number of notches, by simply pairing each substituted letter
|
|
with a bit value saying whether it has an associated
|
|
notch:\footnote{The type definition for {\tt Char} was given in
|
|
Example~\ref{section:subst}-\ref{ex:subst:1}.}
|
|
|
|
\begin{code}
|
|
type Rotor = [26](Char, Bit)
|
|
\end{code}
|
|
The function {\tt mkRotor} will create a rotor for us from a given permutation of the letters and the notch
|
|
locations:\footnote{The function {\tt elem} was defined in \exerciseref{ex:recfun:4:1}.\indElem}
|
|
\begin{code}
|
|
mkRotor : {n} (fin n) => (Permutation, String n) -> Rotor
|
|
mkRotor (perm, notchLocations) = [ (p, elem (p, notchLocations))
|
|
| p <- perm
|
|
]
|
|
\end{code}
|
|
\todo[inline]{A diagram here would be really useful, especially one
|
|
that captures the location and use of notches and the state of these
|
|
rotors before and after rotations.}
|
|
Let us create a couple of rotors with notches:
|
|
\begin{code}
|
|
rotor1, rotor2, rotor3 : Rotor
|
|
rotor1 = mkRotor ("RJICAWVQZODLUPYFEHXSMTKNGB", "IO")
|
|
rotor2 = mkRotor ("DWYOLETKNVQPHURZJMSFIGXCBA", "B")
|
|
rotor3 = mkRotor ("FGKMAJWUOVNRYIZETDPSHBLCQX", "CK")
|
|
\end{code}
|
|
For instance, {\tt rotor1} maps {\tt A} to {\tt R}, {\tt B} to {\tt J},
|
|
$\ldots$, and {\tt Z} to {\tt B} in its initial position. It will engage its
|
|
notch if one of the permuted letters {\tt I} or {\tt O} appear in its first
|
|
position.
|
|
|
|
\begin{Exercise}\label{ex:enigma:2}
|
|
Write out the encrypted letters for the sequence of 5 {\tt C}'s for
|
|
{\tt rotor1}, assuming it rotates in each step. At what points does
|
|
it engage its own notch to signal the next rotor to rotate?
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:enigma:2}
|
|
Recall that {\tt rotor1} was defined as:
|
|
\begin{Verbatim}
|
|
rotor1 = mkRotor ("RJICAWVQZODLUPYFEHXSMTKNGB", "IO")
|
|
\end{Verbatim}
|
|
Here is a listing of the new mappings and the characters we will get
|
|
at the output for each successive {\tt C}:
|
|
\begin{Verbatim}
|
|
starting map output notch engaged?
|
|
RJICAWVQZODLUPYFEHXSMTKNGB I no
|
|
JICAWVQZODLUPYFEHXSMTKNGBR C no
|
|
ICAWVQZODLUPYFEHXSMTKNGBRJ A yes
|
|
CAWVQZODLUPYFEHXSMTKNGBRJI W no
|
|
AWVQZODLUPYFEHXSMTKNGBRJIC V no
|
|
\end{Verbatim}
|
|
Note how we get different letters as output, even though we are
|
|
providing the same input (all {\tt C}'s.) This is the essence of the
|
|
Enigma: the same input will not cause the same output necessarily,
|
|
making it a polyalphabetic substitution cipher.\indPolyAlphSubst
|
|
\end{Answer}
|
|
|
|
%=====================================================================
|
|
% \section{Connecting the rotors: notches in action}
|
|
% \label{sec:enigma:notches}
|
|
\sectionWithAnswers{Connecting the rotors: notches in action}{sec:enigma:notches}
|
|
|
|
\todo[inline]{A diagram here depicting rotor interchangeability and
|
|
the relationship between \texttt{scramble} and rotors in the above
|
|
figure.}
|
|
|
|
The original Enigma had three interchangeable rotors. The operator
|
|
chose the order they were placed in the machine. In our model, we will
|
|
allow for an arbitrary number of rotors. The tricky part of connecting
|
|
the rotors is ensuring that the rotations of each are done properly.
|
|
|
|
Let us start with a simpler problem. If we are given a rotor and a
|
|
particular letter to encrypt, how can we compute the output letter and
|
|
the new rotor position? First of all, we will need to know if the
|
|
rotor should rotate itself, that is if the notch between this rotor
|
|
and the previous one was activated. Also, we need to find out if the
|
|
act of rotation in this rotor is going to cause the next rotor to
|
|
rotate. We will model this action using the Cryptol function {\tt
|
|
scramble}:
|
|
\begin{code}
|
|
scramble : (Bit, Char, Rotor) -> (Bit, Char, Rotor)
|
|
\end{code}
|
|
The function {\tt scramble} takes a triple \texttt{(rotate, c, rotor)}:
|
|
\begin{itemize}
|
|
\item {\tt rotate}: if {\tt True}, this rotor will rotate after
|
|
encryption. Indicates that the notch between this rotor and the
|
|
previous one was engaged,
|
|
\item {\tt c}: the character to encrypt, and
|
|
\item {\tt rotor}: the current state of the rotor.
|
|
\end{itemize}
|
|
Similarly, the output will also be a triple:
|
|
\begin{itemize}
|
|
\item {\tt notch}: {\tt True} if the notch on this rotor engages,
|
|
i.e., if the next rotor should rotate itself,
|
|
\item {\tt c'}: the result of encrypting (substituting) for {\tt c}
|
|
with the current state of the rotor.
|
|
\item {\tt rotor'}: the new state of the rotor. If no rotation was
|
|
done this will be the same as {\tt rotor}. Otherwise it will be the
|
|
new substitution map obtained by rotating the old one to the left by
|
|
one.
|
|
\end{itemize}
|
|
Coding {\tt scramble} is straightforward:
|
|
\begin{code}
|
|
scramble (rotate, c, rotor) = (notch, c', rotor')
|
|
where
|
|
(c', _) = rotor @ (c - 'A')
|
|
(_, notch) = rotor @ 0
|
|
rotor' = if rotate then rotor <<< 1 else rotor
|
|
\end{code}
|
|
To determine {\tt c'}, we use the substitution map to find out what
|
|
this rotor maps the given character to, with respect to its current
|
|
state. Note how Cryptol's pattern matching notation\indPatMatch helps
|
|
with extraction of {\tt c'}, as we only need the character, not
|
|
whether there is a notch at that location. (The underscore character
|
|
use, `\texttt{\_}',\indUnderscore means that we do not need the value
|
|
at the position, and hence we do not give it an explicit name.) To
|
|
determine if we have our notch engaged, all we need to do is to look
|
|
at the first elements notch value, using Cryptol's selection operator
|
|
({\tt @ 0}\indIndex), and we ignore the permutation value there this
|
|
time, again using pattern matching. Finally, to determine {\tt
|
|
rotor'} we merely rotate left by 1\indRotLeft if the {\tt rotate}
|
|
signal was received. Otherwise, we leave the {\tt rotor} unchanged.
|
|
|
|
\begin{Exercise}\label{ex:enigma:3}
|
|
Redo \exerciseref{ex:enigma:2}, this time using Cryptol and the
|
|
{\tt scramble} function.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:enigma:3}
|
|
We can define the following value to simulate the operation of
|
|
always telling {\tt scramble} to rotate the rotor and providing it
|
|
with the input {\tt C}.
|
|
\begin{Verbatim}
|
|
rotor1CCCCC = [(c1, n1), (c2, n2), (c3, n3), (c4, n4), (c5, n5)]
|
|
where (n1, c1, r1) = scramble (True, 'C', rotor1)
|
|
(n2, c2, r2) = scramble (True, 'C', r1)
|
|
(n3, c3, r3) = scramble (True, 'C', r2)
|
|
(n4, c4, r4) = scramble (True, 'C', r3)
|
|
(n5, c5, r5) = scramble (True, 'C', r4)
|
|
\end{Verbatim}
|
|
\todo[inline]{Remind reader of simultaneity of \texttt{where}
|
|
clauses.} Note how we chained the output rotor values in the calls,
|
|
through the values {\tt r1}-{\tt r2}-{\tt r3} and {\tt r4}. We have:
|
|
\begin{Verbatim}
|
|
Cryptol> rotor1CCCCC
|
|
[(I, False), (C, False), (A, True), (W, False), (V, False)]
|
|
\end{Verbatim}
|
|
Note that we get precisely the same results from Cryptol as we
|
|
predicted in the previous exercise.
|
|
\end{Answer}
|
|
|
|
\note{The actual mechanics of the Enigma machine were slightly more
|
|
complicated: due to the keyboard mechanism and the way notches were
|
|
mechanically built, the first rotor was actually rotating before the
|
|
encryption took place. Also, the middle rotor could double-step if
|
|
it engages its notch right after the third rotor
|
|
does~\cite{enigmaAnomaly}.
|
|
|
|
We will take the simpler view here and assume that each key press
|
|
causes an encryption to take place, {\em after} which the rotors do
|
|
their rotation, getting ready for the next input. The mechanical
|
|
details, while historically important, are not essential for our
|
|
modeling purposes here. Also, the original Enigma had {\em rings}, a
|
|
relatively insignificant part of the whole machine, that we ignore
|
|
here.}
|
|
|
|
\paragraph*{Sequencing the rotors} Now that we have the rotors modeled,
|
|
the next task is to figure out how to connect them in a sequence. As
|
|
we mentioned, Enigma had 3 rotors originally (later versions allowing
|
|
4). The three rotors each had a single notch (later versions allowing
|
|
double notches). Our model allows for arbitrary number of rotors and
|
|
arbitrary number of notches on each. The question we now tackle is
|
|
the following: Given a sequence of rotors, how do we run them one
|
|
after the other? We are looking for a function with the following
|
|
signature:
|
|
\begin{code}
|
|
joinRotors : {n} (fin n) => ([n]Rotor, Char) -> ([n]Rotor, Char)
|
|
\end{code}
|
|
That is, we receive {\tt n} rotors and the character to be encrypted,
|
|
and return the updated rotors (accounting for their rotations) and the
|
|
final character. The implementation is an instance of the
|
|
fold\indFold pattern (\autoref{sec:recandrec}), using the {\tt
|
|
scramble} function we have just defined:
|
|
\begin{code}
|
|
joinRotors (rotors, inputChar) = (rotors', outputChar)
|
|
where
|
|
initRotor = mkRotor (['A' .. 'Z'], [])
|
|
ncrs : [n+1](Bit, [8], Rotor)
|
|
ncrs = [(True, inputChar, initRotor)]
|
|
# [ scramble (notch, char, r)
|
|
| r <- rotors
|
|
| (notch, char, rotor') <- ncrs
|
|
]
|
|
rotors' = tail [ r | (_, _, r) <- ncrs ]
|
|
(_, outputChar, _) = ncrs ! 0
|
|
\end{code}
|
|
The workhorse in {\tt joinRotors} is the definition of {\tt ncrs}, a
|
|
mnemonic for {\em notches-chars-rotors}. The idea is fairly simple.
|
|
We simply iterate over all the given rotors ({\tt r <- rotors}), and
|
|
{\tt scramble} the current character {\tt char}, using the rotor {\tt
|
|
r} and the notch value {\tt notch}. These values come from {\tt
|
|
ncrs} itself, using the fold pattern\indFold encoded by the
|
|
comprehension\indComp. The only question is what is the seed value
|
|
for this fold?
|
|
|
|
The seed used in {\tt ncrs} is {\tt (True, inputChar, initRotor)}. The
|
|
first component is {\tt True}, indicating that the very first rotor
|
|
should always rotate itself at every step. The second element is {\tt
|
|
inputChar}, which is the input to the whole sequence of rotors. The
|
|
only mysterious element is the last one, which we have specified as
|
|
{\tt initRotor}. This rotor is defined so that it simply maps the
|
|
letters to themselves with no notches on it, by a call to the {\tt
|
|
mkRotor} function we have previously defined. This rotor is merely a
|
|
place holder to kick off the computation of {\tt ncrs}, it acts as the
|
|
identity element in a sequence of rotors. To compute {\tt rotors'},
|
|
we merely project the third component of {\tt ncrs}, being careful
|
|
about skipping the first element using {\tt tail}\indTail. Finally,
|
|
{\tt outputChar} is merely the output coming out of the final rotor,
|
|
extracted using {\tt !0}\indRIndex. Note how we use Cryptol's pattern
|
|
matching to get the second component out of the triple in the last
|
|
line.\indPatMatch
|
|
|
|
\begin{Exercise}\label{ex:enigma:4}
|
|
Is the action of {\tt initRotor} ever used in the definition of {\tt
|
|
joinRotors}?
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:enigma:4}
|
|
Not unless we receive an empty sequence of rotors, i.e., a call of
|
|
the form: {\tt joinRotors ([], c)} for some character {\tt c}. In
|
|
this case, it does make sense to return {\tt c} directly, which is
|
|
what {\tt initRotor} will do. Note that unless we do receive an
|
|
empty sequence of rotors, the value of {\tt initRotor} will not be
|
|
used when computing the {\tt joinRotors} function.
|
|
\end{Answer}
|
|
|
|
\begin{Exercise}\label{ex:enigma:5}
|
|
What is the final character returned by the expression:
|
|
\begin{Verbatim}
|
|
joinRotors ([rotor1 rotor2 rotor3], 'F')
|
|
\end{Verbatim}
|
|
Use paper and pencil to figure out the answer by tracing the execution
|
|
of {\tt joinRotors} before running it in Cryptol!
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:enigma:5}
|
|
The crucial part is the value of {\tt ncrs}. Let us write it out by
|
|
substituting the values of {\tt rotors} and {\tt inputChar}:
|
|
\begin{Verbatim}
|
|
ncrs = [(True, 'F', initRotor)]
|
|
# [ scramble (notch, char, r)
|
|
| r <- [rotor1, rotor2, rotor3]
|
|
| (notch, char, rotor') <- ncrs
|
|
]
|
|
\end{Verbatim}
|
|
Clearly, the first element of {\tt ncrs} will be:
|
|
\begin{Verbatim}
|
|
(True, 'F', initRotor)
|
|
\end{Verbatim}
|
|
Therefore, the second element will be the result of the call:
|
|
\begin{Verbatim}
|
|
scramble (True, 'F', rotor1)
|
|
\end{Verbatim}
|
|
Recall that {\tt rotor1} was defined as:
|
|
\begin{Verbatim}
|
|
rotor1 = mkRotor ("RJICAWVQZODLUPYFEHXSMTKNGB", "IO")
|
|
\end{Verbatim}
|
|
What letter does {\tt rotor1} map {\tt F} to? Since {\tt F} is the 5th
|
|
character (counting from 0), {\tt rotor1} maps it to the 5th element
|
|
of its permutation, i.e., {\tt W}, remembering to count from 0! The
|
|
topmost element in {\tt rotor1} is {\tt R}, which is not its
|
|
notch-list, hence it will {\em not} tell the next rotor to rotate. But
|
|
it will rotate itself, since it received the {\tt True} signal. Thus,
|
|
the second element of {\tt ncrs} will be:
|
|
\begin{Verbatim}
|
|
(False, 'W', ...)
|
|
\end{Verbatim}
|
|
where we used {\tt ...} to denote the one left-rotation of {\tt
|
|
rotor1}. (Note that we do not need to know the precise arrangement
|
|
of {\tt rotor1} now for the purposes of this exercise.) Now we move to
|
|
{\tt rotor2}, we have to compute the result of the call:
|
|
\begin{Verbatim}
|
|
scramble (False, 'W', rotor2)
|
|
\end{Verbatim}
|
|
Recall that {\tt rotor2} was defined as:
|
|
\begin{Verbatim}
|
|
rotor2 = mkRotor ("DWYOLETKNVQPHURZJMSFIGXCBA", "B")
|
|
\end{Verbatim}
|
|
So, it maps {\tt W} to {\tt X}. (The fourth letter from the end.) It
|
|
will not rotate itself, and it will not tell {\tt rotor3} to rotate
|
|
itself either since the topmost element is {\tt D} in its current
|
|
configuration, and {\tt D} which is not in the notch-list {\tt
|
|
"B"}. Thus, the final {\tt scramble} call will be:
|
|
\begin{Verbatim}
|
|
scramble (False, 'X', rotor3)
|
|
\end{Verbatim}
|
|
where
|
|
\begin{Verbatim}
|
|
rotor3 = mkRotor ("FGKMAJWUOVNRYIZETDPSHBLCQX", "CK")
|
|
\end{Verbatim}
|
|
It is easy to see that {\tt rotor3} will map {\tt X} to {\tt C}. Thus
|
|
the final value coming out of this expression must be {\tt C}. Indeed,
|
|
we have:\indTupleProj
|
|
\begin{Verbatim}
|
|
Cryptol> project(2, 2, joinRotors ([rotor1 rotor2 rotor3], 'F'))
|
|
C
|
|
\end{Verbatim}
|
|
Of course, Cryptol also keeps track of the new rotor positions as
|
|
well, which we have glossed over in this discussion.
|
|
\end{Answer}
|
|
|
|
%=====================================================================
|
|
% \section{The reflector}
|
|
% \label{sec:enigma:reflector}
|
|
\sectionWithAnswers{The reflector}{sec:enigma:reflector}
|
|
|
|
The final piece of the Enigma machine is the
|
|
reflector\indEnigmaReflector ({\em umkehrwalze} in German). The
|
|
reflector is another substitution map. Unlike the rotors, however, the
|
|
reflector did not rotate. Its main function was ensuring that the
|
|
process of encryption was reversible: The reflector did one final
|
|
jumbling of the letters and then sent the signal back through the
|
|
rotors in the {\em reverse} order, thus completing the loop and
|
|
allowing the signal to reach back to the lamps that would light up.
|
|
For our purposes, it suffices to model it just like any other
|
|
permutation:
|
|
\begin{code}
|
|
type Reflector = Permutation
|
|
\end{code}
|
|
Here is one example:
|
|
\begin{code}
|
|
reflector : Reflector
|
|
reflector = "FEIPBATSCYVUWZQDOXHGLKMRJN"
|
|
\end{code}
|
|
Like the plugboard, the reflector is symmetric: If it maps {\tt B} to
|
|
{\tt E}, it should map {\tt E} to {\tt B}, as in the above
|
|
example. Furthermore, the Enigma reflectors were designed so that they
|
|
never mapped any character to themselves, which is true for the above
|
|
permutation as well. Interestingly, this idea of a non-identity
|
|
reflector (i.e., never mapping any character to itself) turned out to
|
|
be a weakness in the design, which the allies exploited in breaking
|
|
the Enigma during WWII~\cite{Singh:1999:CBE}.
|
|
|
|
\begin{Exercise}\label{ex:enigma:6}
|
|
Write a function {\tt checkReflector} with the signature:
|
|
\begin{Verbatim}
|
|
checkReflector : Reflector -> Bit
|
|
\end{Verbatim}
|
|
such that it returns {\tt True} if a given reflector is good (i.e.,
|
|
symmetric and non-self mapping) and {\tt False} otherwise. Check that
|
|
our definition of {\tt reflector} above is a good one. \lhint{Use the
|
|
{\tt all} function you have defined in
|
|
\exerciseref{ex:zero:1}.}
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:enigma:6}
|
|
%% if this is {code} we have two all's
|
|
\begin{Verbatim}
|
|
all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
|
|
all f xs = [ f x | x <- xs ] == ~zero
|
|
|
|
checkReflector refl = all check ['A' .. 'Z']
|
|
where check c = (c != m) && (c == c')
|
|
where m = refl @ (c - 'A')
|
|
c' = refl @ (m - 'A')
|
|
\end{Verbatim}
|
|
For each character in the alphabet, we first figure out what it maps
|
|
to using the reflector, named {\tt m} above. We also find out what
|
|
{\tt m} gets mapped to, named {\tt c'} above. To be a valid reflector
|
|
it must hold that {\tt c} is not {\tt m} (no character maps to
|
|
itself), and {\tt c} must be {\tt c'}. We have:
|
|
\begin{Verbatim}
|
|
Cryptol> checkReflector reflector
|
|
True
|
|
\end{Verbatim}
|
|
Note how we used {\tt all}\indAll to make sure {\tt check} holds for
|
|
all the elements of the alphabet.
|
|
\end{Answer}
|
|
|
|
%=====================================================================
|
|
% \section{Putting the pieces together}
|
|
% \label{sec:enigma:puttingittogether}
|
|
\sectionWithAnswers{Putting the pieces together}{sec:enigma:puttingittogether}
|
|
|
|
We now have all the components of the Enigma: the plugboard, rotors,
|
|
and the reflector. The final task is to implement the full loop. The
|
|
Enigma ran all the rotors in sequence, then passed the signal through
|
|
the reflector, and ran the rotors in reverse one more time before
|
|
delivering the signal to the lamps.
|
|
|
|
Before proceeding, we will define the following two helper functions:
|
|
\begin{code}
|
|
substFwd, substBwd : (Permutation, Char) -> Char
|
|
substFwd (perm, c) = perm @ (c - 'A')
|
|
substBwd (perm, c) = invSubst (perm, c)
|
|
\end{code}
|
|
(You have defined the {\tt invSubst} function in
|
|
\exerciseref{ex:subst:1}.) The {\tt substFwd}
|
|
function simply returns the character that the given permutation,
|
|
whether from the plugboard, a rotor, or the reflector. Conversely,
|
|
{\tt substBwd} returns the character that the given permutation maps
|
|
{\em from}, i.e., the character that will be mapped to {\tt c} using
|
|
the permutation.
|
|
|
|
\begin{Exercise}\label{ex:enigma:7}
|
|
Using Cryptol, verify that {\tt substFwd} and {\tt substBwd} return
|
|
the same elements for each letter in the alphabet for {\tt rotor1}.
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:enigma:7}
|
|
We can define the following helper function, using the function {\tt
|
|
all} you have defined in
|
|
\exerciseref{ex:zero:1}:\indAll
|
|
\begin{code}
|
|
checkPermutation : Permutation -> Bit
|
|
checkPermutation perm = all check ['A' .. 'Z']
|
|
where check c = (c == substBwd(perm, substFwd (perm, c)))
|
|
&& (c == substFwd(perm, substBwd (perm, c)))
|
|
\end{code}
|
|
Note that we have to check both ways (first {\tt substFwd} then {\tt
|
|
substBwd}, and also the other way around) in case the substitution
|
|
is badly formed, for instance if it is mapping the same character
|
|
twice. We have:
|
|
\begin{Verbatim}
|
|
Cryptol> checkPermutation [ c | (c, _) <- rotor1 ]
|
|
True
|
|
\end{Verbatim}
|
|
For a bad permutation we would get {\tt False}:
|
|
\begin{Verbatim}
|
|
Cryptol> checkPermutation (['A' .. 'Y'] # ['A'])
|
|
False
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\begin{Exercise}\label{ex:enigma:8}
|
|
Show that {\tt substFwd} and {\tt substBwd} are exactly the same
|
|
operations for the reflector. Why?
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:enigma:8}
|
|
Since the reflector is symmetric, substituting backwards or forwards
|
|
does not matter. We can verify this with the following helper
|
|
function:\indAll
|
|
\begin{code}
|
|
all : {a, b} (fin b) => (a -> Bit) -> [b]a -> Bit
|
|
all fn xs = folds ! 0 where
|
|
folds = [True] # [ fn x && p | x <- xs
|
|
| p <- folds]
|
|
checkReflectorFwdBwd : Reflector -> Bit
|
|
checkReflectorFwdBwd refl = all check ['A' .. 'Z']
|
|
where check c = substFwd (refl, c) == substBwd (refl, c)
|
|
\end{code}
|
|
We have:
|
|
\begin{Verbatim}
|
|
Cryptol> checkReflectorFwdBwd reflector
|
|
True
|
|
\end{Verbatim}
|
|
\end{Answer}
|
|
|
|
\paragraph*{The route back} One crucial part of the Enigma is the
|
|
running of the rotors in reverse after the reflector. Note that this
|
|
operation ignores the notches, i.e., the rotors do not turn while the
|
|
signal is passing the second time through the rotors. (In a sense, the
|
|
rotations happen after the signal completes its full loop, getting to
|
|
the reflector and back.) Consequently, it is much easer to code as
|
|
well (compare this code to {\tt joinRotors}, defined in
|
|
\autoref{sec:enigma:notches}):
|
|
|
|
\begin{code}
|
|
backSignal : {n} (fin n) => ([n]Rotor, Char) -> Char
|
|
backSignal (rotors, inputChar) = cs ! 0
|
|
where
|
|
cs = [inputChar] # [ substBwd ([ p | (p, _) <- r ], c)
|
|
| r <- reverse rotors
|
|
| c <- cs
|
|
]
|
|
\end{code}
|
|
Note that we explicitly reverse the rotors in the definition of {\tt
|
|
cs}.\indReverse (The definition of {\tt cs} is another typical
|
|
example of a fold. See page~\pageref{par:fold}.)\indFold
|
|
|
|
Given all this machinery, coding the entire Enigma loop is fairly
|
|
straightforward:
|
|
\begin{code}
|
|
//enigmaLoop : {n} (fin n) => (Plugboard, [n]Rotor, Reflector, Char)
|
|
// -> ([n]Rotor, Char)
|
|
enigmaLoop (pboard, rotors, refl, c0) = (rotors', c5)
|
|
where
|
|
// 1. First run through the plugboard
|
|
c1 = substFwd (pboard, c0)
|
|
// 2. Now run all the rotors forward
|
|
(rotors', c2) = joinRotors (rotors, c1)
|
|
// 3. Pass through the reflector
|
|
c3 = substFwd (refl, c2)
|
|
// 4. Run the rotors backward
|
|
c4 = backSignal(rotors, c3)
|
|
// 5. Finally, back through the plugboard
|
|
c5 = substBwd (pboard, c4)
|
|
\end{code}
|
|
|
|
%=====================================================================
|
|
\section{The state of the machine}
|
|
\label{sec:state-machine}
|
|
|
|
We are almost ready to construct our own Enigma machine in
|
|
Cryptol. Before doing so, we will take a moment to represent the state
|
|
of the Enigma machine as a Cryptol record\indTheRecordType, which will
|
|
simplify our final construction. At any stage, the state of an Enigma
|
|
machine is given by the status of its rotors. We will use the
|
|
following record to represent this state, for an Enigma machine
|
|
containing \texttt{n} rotors:
|
|
\begin{code}
|
|
type Enigma n = { plugboard : Plugboard,
|
|
rotors : [n]Rotor,
|
|
reflector : Reflector
|
|
}
|
|
\end{code}
|
|
To initialize an Enigma machine, the operator provides the plugboard
|
|
settings, rotors, the reflector. Furthermore, the operator also gives
|
|
the initial positions for the rotors. Rotors can be initially rotated
|
|
to any position before put together into the machine. We can capture
|
|
this operation with the function {\tt mkEnigma}:
|
|
\begin{code}
|
|
mkEnigma : {n} (Plugboard, [n]Rotor, Reflector, [n]Char)
|
|
-> Enigma n
|
|
mkEnigma (pboard, rs, refl, startingPositions) =
|
|
{ plugboard = pboard,
|
|
rotors = [ r <<< (s - 'A')
|
|
| r <- rs
|
|
| s <- startingPositions
|
|
],
|
|
reflector = refl
|
|
}
|
|
\end{code}
|
|
Note how we rotate each given rotor to the left by the amount given by
|
|
its starting position.
|
|
|
|
\todo[inline]{Connect ``left'' with up/down in the earlier
|
|
illustrations.}
|
|
|
|
Given this definition, let us construct an Enigma machine out of the
|
|
components we have created so far, using the starting positions {\tt
|
|
GCR} for the rotors respectively:\label{def:modelEnigma}
|
|
\begin{code}
|
|
modelEnigma : Enigma 3
|
|
modelEnigma = mkEnigma (plugboard, [rotor1, rotor2, rotor3],
|
|
reflector, "GCR")
|
|
\end{code}
|
|
We now have an operational Enigma machine coded up in Cryptol!
|
|
|
|
%=====================================================================
|
|
% \section{Encryption and decryption}
|
|
% \label{enigma:encdec}
|
|
\sectionWithAnswers{Encryption and decryption}{enigma:encdec}
|
|
|
|
Equipped with all the machinery we now have, coding Enigma encryption
|
|
is fairly straightforward:
|
|
\begin{code}
|
|
enigma : {n, m} (fin n, fin m) => (Enigma n, String m) -> String m
|
|
enigma (m, pt) = tail [ c | (_, c) <- rcs ]
|
|
where rcs = [(m.rotors, '*')] #
|
|
[ enigmaLoop (m.plugboard, r, m.reflector, c)
|
|
| c <- pt
|
|
| (r, _) <- rcs
|
|
]
|
|
\end{code}
|
|
The function {\tt enigma} takes a machine with {\tt n} rotors and a
|
|
plaintext of {\tt m} characters, returning a ciphertext of {\tt m}
|
|
characters back. It is yet another application of the fold pattern,
|
|
where we start with the initial set of rotors and the placeholder
|
|
character {\tt *} (which could be anything) to seed the fold.\indFold
|
|
Note how the change in rotors is reflected in each iteration of the
|
|
fold, through the {\tt enigmaLoop} function. At the end, we simply
|
|
drop the rotors from {\tt rcs}, and take the {\tt tail}\indTail to
|
|
skip over the seed character {\tt *}.
|
|
|
|
Here is our Enigma in operation:
|
|
\begin{Verbatim}
|
|
Cryptol> :set ascii=on
|
|
Cryptol> enigma (modelEnigma, "ENIGMAWASAREALLYCOOLMACHINE")
|
|
"UPEKTBSDROBVTUJGNCEHHGBXGTF"
|
|
\end{Verbatim}
|
|
|
|
\paragraph*{Decryption} As we mentioned before, Enigma was a
|
|
self-decrypting machine, that is, encryption and decryption are
|
|
precisely the same operations. Thus, we can define:
|
|
\begin{code}
|
|
dEnigma : {n, m} (fin n, fin m) => (Enigma n, String m) -> String m
|
|
dEnigma = enigma
|
|
\end{code}
|
|
And decrypt our above message back:
|
|
\begin{Verbatim}
|
|
Cryptol> dEnigma (modelEnigma, "UPEKTBSDROBVTUJGNCEHHGBXGTF")
|
|
"ENIGMAWASAREALLYCOOLMACHINE"
|
|
\end{Verbatim}
|
|
We have successfully performed our first Enigma encryption!
|
|
|
|
\begin{Exercise}\label{ex:enigma:9}
|
|
Different models of Enigma came with different sets of rotors. You
|
|
can find various rotor configurations on the
|
|
web~\cite{wiki:enigmarotors}. Create models of these rotors in
|
|
Cryptol, and run sample encryptions through them.
|
|
\end{Exercise}
|
|
|
|
\begin{Exercise}\label{ex:enigma:10}
|
|
As we have mentioned before, Enigma implements a polyalphabetic
|
|
substitution cipher\indPolyAlphSubst, where the same letter gets
|
|
mapped to different letters during encryption. The
|
|
period\indSubstPeriod of a cipher is the number of characters before
|
|
the encryption repeats itself, mapping the same sequence of letters
|
|
in the plaintext to the to the same sequence of letters in the
|
|
ciphertext. What is the period of an Enigma machine with $n$ rotors?
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:enigma:10}
|
|
Enigma will start repeating once the rotors go back to their
|
|
original position. With $n$ rotors, this will take $26^n$
|
|
characters. In the case of the traditional 3-rotor Enigma this
|
|
amounts to $26^3 = 17576$ characters. Note that we are assuming an
|
|
ideal Enigma here with no double-stepping~\cite{enigmaAnomaly}.
|
|
\end{Answer}
|
|
|
|
\begin{Exercise}\label{ex:enigma:11}
|
|
Construct a string of the form {\tt CRYPTOLXXX...XCRYPTOL}, where
|
|
...'s are filled with enough number of {\tt X}'s such that
|
|
encrypting it with our {\tt modelEnigma} machine will map the
|
|
instances of ``{\tt CRYPTOL}'' to the same ciphertext. How many {\tt
|
|
X}'s do you need? What is the corresponding ciphertext for ``{\tt
|
|
CRYPTOL}'' in this encryption?
|
|
\end{Exercise}
|
|
\begin{Answer}\ansref{ex:enigma:11}
|
|
Since the period\indSubstPeriod for the 3-rotor Enigma is 17576 (see
|
|
the previous exercise), we need to make sure two instances of {\tt
|
|
CRYPTOL} are 17576 characters apart. Since {\tt CRYPTOL} has 7
|
|
characters, we should have 17569 X's. The following Cryptol
|
|
definition would return the relevant pieces:
|
|
\begin{code}
|
|
enigmaCryptol = (take`{7} ct, drop`{17576} ct)
|
|
where str = "CRYPTOL" # [ 'X' | _ <- [1 .. 17569] ]
|
|
# "CRYPTOL"
|
|
ct = dEnigma(modelEnigma, str)
|
|
\end{code}
|
|
We have:
|
|
\begin{Verbatim}
|
|
Cryptol> enigmaCryptol
|
|
("KGSHMPK", "KGSHMPK")
|
|
\end{Verbatim}
|
|
As predicted, both instances of {\tt CRYPTOL} get encrypted as {\tt
|
|
KGSHMPK}.
|
|
\end{Answer}
|
|
|
|
\paragraph*{The code} You can see all the Cryptol code for our Enigma
|
|
simulator in Appendix~\ref{app:enigma}.
|
|
|
|
\commentout{
|
|
\begin{code}
|
|
invSubst : (Permutation, Char) -> Char
|
|
invSubst (key, c) = candidates ! 0
|
|
where candidates = [0] # [ if c == k then a else p
|
|
| k <- key
|
|
| a <- ['A' .. 'Z']
|
|
| p <- candidates
|
|
]
|
|
elem : {a, b} (fin 0, fin a, Cmp b) => (b, [a]b) -> Bit
|
|
elem (x, xs) = matches ! 0
|
|
where matches = [False] # [ m || (x == e) | e <- xs
|
|
| m <- matches
|
|
]
|
|
sanityCheck = enigma (modelEnigma, "ENIGMAWASAREALLYCOOLMACHINE") == "UPEKTBSDROBVTUJGNCEHHGBXGTF"
|
|
\end{code}
|
|
}
|
|
|
|
%%% Local Variables:
|
|
%%% mode: latex
|
|
%%% TeX-master: "../main/Cryptol"
|
|
%%% End:
|