\numberwithin{equation}{section}
-
+
\renewcommand{\thesection}{\arabic{section}}
-\renewcommand{\thealgorithm}{\arabic{section}.\arabic{algorithm}}
+\renewcommand{\thealgorithm}{\arabic{section}.\arabic{algorithm}}
%opening
\title{Formal Verification of Algorithms arising in Cryptography}
in applied Cryptography. Classic cryptographic algorithms rest
on the mathematical field of number theory, where abstract
mathematical problems are presented and algorithms to solve
-them are discussed. These mathematical preliminaries are then
-used to ensure secure encryption of secret messages. We prove
-formal correctness by considering concrete implementations and
+them are discussed. These mathematical preliminaries are then
+used to ensure secure encryption of secret messages. We prove
+formal correctness by considering concrete implementations and
use the recently developed verification system {\rm RISCAL} to
-prove exactness of the treated algorithms. We present the theories
+prove exactness of the treated algorithms. We present the theories
developed in RISCAL, and put them into context of formal verification
systems.
\end{abstract}
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{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
-$a,b\in\mathbb{N}$. Among all divisors of two numbers $a$,$b$ there is a
+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)$,
-that is computed by the \emph{Euclidean algorithm}. The \emph{extended Euclidean algorithm}
+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}$
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 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
+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$
+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
-1,\qquad & \text{if $a$ is quadratic nonresidue modulo $p$}
\end{cases}
$$
-Let $a$ be an integer and $n$ be a positive odd number such that $n = p_1^{\alpha_1}\ldots p_s^{\alpha_s}$.
+Let $a$ be an integer and $n$ be a positive odd number such that $n = p_1^{\alpha_1}\ldots p_s^{\alpha_s}$.
The \emph{Jacobi-Symbol} $\left(\frac{a}{n}\right)$ is defined as
$$
\left(\frac{a}{n}\right) = \left(\frac{a}{p_1}\right)^{\alpha_1}\ldots \left(\frac{a}{p_s}\right)^{\alpha_s}.
\end{lem}
-
+
\subsubsection*{The Discrete Logarithm problem}
-Consider an odd prime $p$. Let $b\in\mathbb{Z}_p$ and $0\leq x\leq p-1$.
+Consider an odd prime $p$. Let $b\in\mathbb{Z}_p$ and $0\leq x\leq p-1$.
We consider the equality $a\equiv b^x\pmod p$, and call $x$ the \emph{discrete
logarithm} (or \emph{index}) of $a$ with respect to the basis $b$.\\
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 B now wants to transmit a secret message to A, B uses the public key $(n,e)$
+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, B transmits the encrypted message $c$ to A.\\
$$
d = \sum_{i=0}^m a_i\cdot 2^i,\qquad a_i \in \{0,1\}.
$$
-With that representation of $d$, we immediately obtain
+With that representation of $d$, we immediately obtain
$c^d \equiv c^{a_0}\cdot (c^{2})^{a_1} \cdot \ldots (c^{2^m})^{a_m}$.
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:
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) =
+{\rm Exp}(x,n) =
\begin{cases}
1,\qquad & n =0\\
{\rm Exp}(x^2,n/2),\qquad & n \text{ is even}\\
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.
+y \leq y' \text{ and }
+\begin{cases}
+ n \text{ is odd } &\Rightarrow y < y',\\
+ n \text{ is even }&\Rightarrow y = y',
+\end{cases}
+\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$.
showstringspaces=false, % underline spaces within strings only
showtabs=false, % show tabs within strings adding particular underscores
stepnumber=1, % the step between two line-numbers. If it's 1, each line will be numbered
- tabsize=2, % sets default tabsize to 2 spaces
+ tabsize=2, % sets default tabsize to 2 spaces
}
{\tiny \lstinputlisting{../src/primefactors.cpp}}
projects / cfuerst / formal-numbers.git / commitdiff