\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{listings}
+
+%
+ \newtheorem{thm}{Theorem}[section]
+ \newtheorem{cor}[thm]{Corollary}
+ \newtheorem{lem}[thm]{Lemma}
+ \newtheorem{prop}[thm]{Proposition}
+ \theoremstyle{definition}
+ \newtheorem{defn}[thm]{Definition}
+ \newtheorem{ex}[thm]{Example}
+ \theoremstyle{remark}
+ \newtheorem{rem}[thm]{Remark}
+
+ \numberwithin{equation}{section}
+
+
%opening
\title{Formal Verification of Algorithms arising in Cryptography}
\author{Christoph F\"urst\qquad Wolfgang Schreiner\\ Research Institute for Symbolic Computation (RISC) Linz}
unique \emph{greatest} common divisor of $a$ and $b$, denoted by $\gcd(a,b)$,
that is computed by the \emph{Euclidean algorithm}. The \emph{extended Euclidean algorithm}
allows to compute integers $s,t\in\mathbb{Z}$ such that $a\cdot s + b\cdot t = \gcd(a,b)$.
+Two numbers $a,b$ with $\gcd(a,b)=1$ are sometimes called \emph{relative prime}.
In particular, if $p$ is prime and $a\in\mathbb{N}$, there are integers $s,t\in\mathbb{Z}$
such that
$$
which carry equivalent information. We focus on the second representation, i.e.
we demand the result of the operation modulo $p$ to be in $\mathbb{Z}_p = \{0,\ldots,p-1\}$.
+\subsection{Elementary Number Theory}
+With the preliminaries introduced in the last subsection, we can already formulate the
+first non-trivial Theorems in number theory.
+
+\begin{thm}[Fundamental Theorem of Arithmetic]
+ Every natural number can be written as product of primes uniquely up to order.
+\end{thm}
+
+TODO: Describe algorithms for computing prime decomposition
+
+\subsubsection*{Euler's totient Function}
+A fundamental notion for a natural number $n$ is the set of elements relatively prime
+to $n$. The cardinality of this set is referred in literature as \emph{Euler's $\phi$-function}
+(sometimes also as \emph{Euler's totient}-function) $\phi(n)$, i.e.
+$$
+\phi(n) := |\{a\in\mathbb{N}: 1\leq a\leq n \gcd(a,n) = 1\}|.
+$$
+Let us characterize $\phi(n)$.
+\begin{lem}
+ Let $m,n\in\mathbb{N}$, $p,p_1,p_2$ be prime, $k\in\mathbb{N}$.
+ \begin{itemize}
+ \item $\phi(p) = p-1$;
+ \item $\phi(p^k) = p^{k}-p^{k-1} = p^k \left(1-\frac{1}{p}\right)$;
+ \item $\phi(m\cdot n) = \phi(m)\cdot\phi(n)\cdot \frac{\gcd(m,n)}{\phi(\gcd(m,n))}$ in particular $\phi(p_1\cdot p_2) = \phi(p_1)\cdot\phi(p_2)$;
+ \item $\phi(n) = n\cdot \prod_{p|n}\limits\left(1-\frac{1}{p}\right)$ ;
+ \item $\sum_{d|n}\limits \phi(d) = n$.
+ \end{itemize}
+ \subsubsection*{The Legendre/Jacobi Symbol}
+ TODO
+ \subsubsection*{The discrete Logarithm problem}
+ TODO
+ \subsection{The RSA cryptosystem}
+ TODO
+
+\end{lem}
+
+
\section{The Formal Verification}