the term \emph{divisor}, we say for $a,c\in\mathbb{N}$,
that \emph{$a$ divides $c$}, and write $a|c$, if there is a number $b\in\mathbb{N}$
such that $c = a\cdot b$. Every number $n\in\mathbb{N}$ has at least
-two divisors. A \emph{prime number} $p\in\mathbb{N}$ is a number $p$
+two divisors, a \emph{prime number} $p\in\mathbb{N}$ is a number $p$
that has exactly two divisors, $1$ and $p$. Let now be given two numbers
$a,b\in\mathbb{N}$. Among all divisors of two numbers $a$,$b$ there is a
unique \emph{greatest} common divisor of $a$ and $b$, denoted by $\gcd(a,b)$,
Alice, on her side, uses her private key $d$ to compute $c^d \pmod n$ which obviously gives
$$
-c^d \equiv (m^e)^d \equiv m^{(ed)} = m^1 \mod n,
+c^d \equiv (m^e)^d \equiv m^{(ed)} \equiv m^{1+k\cdot \phi(n)} \equiv m \mod n,
$$
by Euler-/Fermat's Theorem Lemma \ref{lem:eulerfermat},
and translates the message $m$ back into their agreed alphabet.
\subsection{The Diffie-Hellmann cryptosystem}
-TODO
+The Diffie-Hellmann cryptosystem, relies on the following idea. Alice and Bob agree on
+a (large) prime $p$ and an element $a\in\mathbb{Z}_p$ (of great order). The pair $(a,p)$
+is called the \emph{public key}. Then, both Alice and Bob, choose their private key $x$ and
+$y$ respectively, and publish $a^x\pmod p$ and $a^y\pmod p$. Alice takes the published key
+$a^y\pmod p$ from Bob and computes the key $K\equiv (a^y)^x \equiv a^{xy}\pmod p$. Similar, Bob
+takes the published key $a^x\pmod p$ from Alice and computes $K \equiv (a^x)^y \equiv a^{xy}\pmod p$,
+to obtain the same key. The key $K$ can now be used by a 'simpler' crypto-system, such as a
+simple displacement chiffre.
\section{The Formal Verification}
TODO: Describe algorithm Left-To-Right Exponentation
projects / cfuerst / formal-numbers.git / commitdiff