two possible implementations of the Sieve of Erathostenes, and view the difference in the formalization.
\subsection{(Slightly more) Advanced Number Theory}
-Describe the algorithm for discrete logarithm here
+In this section, we describe a cryptographic algorithm, the \emph{Diffie-Hellmann key exchange} that has its origins
+in computational number theory. Within the description of the algorithm, we will pose question \eqref{eq:q2} that we
+will answer and formalize in section \ref{sec:formal}. The Diffie-Hellmann key exchange is used, when two parties, say
+\textbf{A}lice and \textbf{B}ob want to exchange secret messages. \textbf{A} and \textbf{B} agree on
+a (large) prime $p$ and an element $a\in\mathbb{Z}_p$ (of high order, i.e. $a^m\pmod p \equiv 1$ implies that
+$m$ is large). The pair $(a,p)$ is called the \emph{public key}. Then, both \textbf{A} and \textbf{B}, choose their private key $x$ and
+$y$ respectively, and publish as a public key $a^x\pmod p$ and $a^y\pmod p$ respectively. \textbf{A} takes the published key
+$a^y\pmod p$ from Bob and computes the key $M\equiv (a^y)^x \equiv a^{xy}\pmod p$. Similar, \textbf{B}
+takes the published key $a^x\pmod p$ from \textbf{A} and computes $M \equiv (a^x)^y \equiv a^{xy}\pmod p$,
+to obtain the same key. The key $M$ can now be used by a ``simpler'' crypto-system, such as a
+simple displacement chiffre.\\
+
+Why is this algorithm useful? The overall concept of the Diffie-Hellmann key exchange rests on the \emph{discrete logarithm problem}.
+Let us describe this problem in more detail: Suppose we are given
+\begin{itemize}
+ \item an odd (very large) prime $p$;
+ \item an element $b\in \mathbb{Z}_p$;
+\end{itemize}
+If we now have an element $a$ such that $0\leq a\leq p-1$, such that
+$$
+a \equiv b^x \pmod p,\qquad 0\leq x\leq p-1,
+$$
+then $x$ is called \emph{the discrete logarithm} of $a$ to basis $b$. The assumption of the Diffie-Hellmann algorithm
+might now be formulated as follows: Given $a^x\pmod p$ and $a^y\pmod p$ without knowing $x,y$, the expression $a^{xy}\pmod p$
+is not efficiently solvable.\\
+
+We are now ready formulate \eqref{eq:q2}:
+\begin{itemize}
+ \item Let $p$ be a large (odd) prime;
+ \item An element $g$ such that $2\leq g\leq p-1$ of order $p-1$;
+ \item An element $a\in\mathbb{Z}_p\backslash\{0\}$;
+\end{itemize}
+\begin{equation}\label{eq:q2}
+\text{Find }x\in \mathbb{Z}_p \text{ such that }\, g^x\equiv a\pmod p.\tag{{\rm Q2}}
+\end{equation}
\section{Analysis of the Algorithms}
The first step in formalization is to do the necessary paper-work. We start by analyzing the expected input and output
considered, no further numbers greater $\lfloor \sqrt{n}\rfloor$ need to be considered and hence the algorithm terminates in
a finite number of steps.
-\subsection{Discrete Logarithm - Algorithm of Tonelli}
+\subsection{Discrete Logarithm - The Baby Step Giant Step Algorithm}
-\section{The RISCAL Formalization}
+\section{The RISCAL Formalization}\label{sec:formal}
\section{Outlook}