\numberwithin{equation}{section}
+
+\renewcommand{\thesection}{\arabic{section}}
+\renewcommand{\thealgorithm}{\arabic{section}.\arabic{algorithm}}
%opening
\title{Formal Verification of Algorithms arising in Cryptography}
integers including zero, i.e. $\mathbb{N} = \{0,1,2,\ldots\}$.
One of the most fundamental notions in mathematics is without doubt
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}$
+that \emph{$a$ divides $c$}, and write $a|c$, if there is a number $b\in\mathbb{Z}$
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$
that has exactly two divisors, $1$ and $p$. Let now be given two numbers
complex numbers $\mathbb{C}$, are infinite fields, the focus in cryptographic
applications is on \emph{finite fields}. A finite field with $p$ elements, where
$p$ is prime, is usually written as $\mathbb{Z}_p = \mathbb{Z}/p\mathbb{Z}$,
-and consists of the elements $\{0,1,\ldots,p-1\}$. The number $p$ is called the
-\emph{characteristic} of $\mathbb{Z}_p$. In fact, the characteristic of every
-finite field is a prime power. Throughout this paper, we restrict our attention
-to the set $\mathbb{Z}_p$, i.e. the integers modulo a prime $p$ (rather than
-a prime power).\\
-
-Let $p$ be a prime. In finite sets of the form $\mathbb{Z}_p$, addition, subtraction
-and multiplication are performed modulo residue classes, i.e. if we denote the residue of
-$a\in\mathbb{Z}$ modulo a prime $p$ by $[a]_p$, then we have
+and consists of the elements $\{0,1,\ldots,p-1\}$. The classic operations are
+carried out modulo $p$, and hence, instead of $a\in\mathbb{Z}$,
+we consider the residue class, denoted by $[a]_p := \{a+k\cdot p: 0\leq a < p \wedge k\in\mathbb{Z}\}$.
+For residue classes, there are two representations available, either
+$$
+\left\{-\frac{p-1}{2},-\frac{p-3}{2}\ldots,\frac{p-3}{2},\frac{p-1}{2}\right\}\qquad \text{ or }\qquad \{0,\ldots,p-1\} = \mathbb{Z}_p,
+$$
+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\}$.\\
+
+The number $p$ is called the \emph{characteristic} of $\mathbb{Z}_p$. In fact,
+the characteristic of every finite field is a prime power. Throughout this paper,
+we restrict our attention to the set $\mathbb{Z}_p$, i.e. the integers modulo a prime $p$
+(rather than a prime power).\\
+
+Let $p$ be an odd prime. In finite sets of the form $\mathbb{Z}_p$, addition, subtraction
+and multiplication are performed modulo a prime $p$ by $[a]_p$, and we have
$$
[a]_p \pm [b]_p := [a\pm b]_p,\qquad [a]_p\cdot [b]_p := [ab]_p.
$$
[a\div b]_p := [a\cdot b^{-1}]_p.
$$
Hence, the finite set $\mathbb{Z}_p$ with the operations of addition, subtraction, multiplication
-and division as defined above, forms a finite field.\\
+and division as defined above, forms a finite field.
+
-For residue classes, there are two representations available, either
-$$
-\left\{-\frac{p-1}{2},\ldots,\frac{p-1}{2}\right\}\qquad \text{ or }\qquad \{0,\ldots,p-1\} = \mathbb{Z}_p,
-$$
-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
\subsection{The RSA cryptosystem}
At the RSA cryptosystem, named after its authors Rivest, Shamir and Adleman, the two
protagonists \textbf{A}lice and \textbf{B}ob want to exchange secret messages. To that
-end, Alice generates two primes $p$ and $q$ which are approximately of the same size.
-Then, Alice calculates the product $n=pq$ and $\phi(n) = (p-1)(q-1)$, and proceeds by
+end, A generates two primes $p$ and $q$ which are approximately of the same size.
+Then, A calculates the product $n=pq$ and $\phi(n) = (p-1)(q-1)$, and proceeds by
choosing $1<e<\phi(n)$ such that $\gcd(e,\phi(n)) = 1$. With the help of the Euclidean
-algorithm, Alice calculates $1<d<\phi(n)$ such that
+algorithm, A calculates $1<d<\phi(n)$ such that
$$
ed \equiv 1 \pmod {\phi(n)}.
$$
We call the pair $(n,e)$ the \emph{public key} of Alice and $d$ the \emph{private key}.
-If Bob now wants to transmit a secret message to Alice, Bob uses the public key $(n,e)$
-of Alice. He represents his (secret) message $m$ by digits $\{0,1,\ldots,n-1\}$, and
+If B now wants to transmit a secret message to A, B uses the public key $(n,e)$
+of A. He represents his (secret) message $m$ by digits $\{0,1,\ldots,n-1\}$, and
computes the encrypted message $c\equiv m^e\pmod n$ by repeated squaring. When he is
-finished, Bob transmits the encrypted message $c$ to Alice.\\
+finished, B transmits the encrypted message $c$ to A.\\
Alice, on her side, uses her private key $d$ to compute $c^d \pmod n$ which obviously gives
$$
forget that the powers are computed modulo $n$), which might be desribed recursive
by
$$
-c^d \equiv c\cdot c^{d-1}, \qquad c^0 \equiv 1.
+c^d = {\rm Pow}(c,d) \equiv c\cdot {\rm Pow}(c,d-1) = c\cdot c^{d-1}, \qquad c^0 = {\rm Pow}(c,0) \equiv 1.
$$
This 'naive algorithm' requires $d$ multiplications of $c$. The Left-to-Right Exponentation proceeds
by first representing $d$ in its binary representation, i.e.
But some of the coefficients $a_k$ might be zero, and hence contribute 1 to the
product. Hence, we are led to the following algorithm:
\begin{algorithm}[H]
- \caption{Left-to-Right Exponentation}
-\begin{algorithmic}
+
+\begin{algorithmic}[1]
\Require{$c\in\mathbb{Z}$, $d\in\mathbb{N}$}
\Ensure{$c^d$}
\State $y \leftarrow 1$;
\State $x\leftarrow x^2$;
\State $n \leftarrow \lfloor n/2\rfloor$;
\EndWhile
-\Return $y$.
+\State\Return $y$.
\end{algorithmic}
+ \caption{Left-to-Right Exponentation}
+ \label{alg:1}
\end{algorithm}
-Let us analyze this in more detail. Formulated as function ${\rm Exp}(x,n)$,
-it is obvious that the algorithm is equivalent to the recursive description
+Let us analyze this in more detail. To gain insight, we might consider some concrete examples.
+If we apply Algorithm \ref{alg:1} to a handful of numbers, we realize the following relationship:
+Formulated as function ${\rm Exp}(x,n)$, we find that algorithm is equivalent to the recursive description
$$
{\rm Exp}(x,n) =
\begin{cases}
x\cdot {\rm Exp}(x^2,(n-1)/2),\qquad & n \text{ is odd}.
\end{cases}
$$
-The binary representation of $d\in\mathbb{N}$ has at most $\lfloor \log_2(d)\rfloor +1$ digits.
+The binary representation of $d\in\mathbb{N}$ has at most $\lfloor \log_2(d)\rfloor +1$ digits.
+Let us consider two extreme cases: If $d$ is a power of 2, say $2^m$, then its binary representation
+equals
+$$
+2^m = (1\underbrace{0\ldots0}_{m \text{ zeros}})_2,
+$$
+and hence consists of exactly $\log_2(d) +1 = m+1$ positions. The If-condition is met only
+once, after $m$ divisions by 2, after which the remainder is one.\\
+
+The other extreme case is when $d$ is $2^m-1 = (1,\ldots,1)_2$ i.e. the binary representation
+consists of exactly $m$ ones. When this is the case, the If-condition \emph{always} evaluates
+to true, and hence we gain nothing compared to the classic algorithm.\\
+For the While-loop, we start with values $(x,y,n)$ and update them to $(x',y',n')$.
+We observe that regardless if $n$ is even or odd, that $n'<n$ at each stage.
+Further, we obviously we have
+$$
+y \leq y' \text{ and } n \text{ is odd }\Rightarrow y < y',\qquad \text{and further } x < x' = x^2.
+$$
+The termination of the loop is a consequence of $\lfloor n/2^k\rfloor \rightarrow 0$ after
+finitely many steps, i.e. there exists $k\in\mathbb{N}$ such that $\lfloor n/2^k\rfloor = 0$.
\appendix
\section{Listing of the developed Theory}
{\scriptsize \verbatiminput{../numbertheory.txt}}
projects / cfuerst / formal-numbers.git / commitdiff