\section{Introduction}
\section{Mathematical and Cryptographic Preliminaries}
+Throughout this paper, let $\mathbb{N}$ denote the non-negative
+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 that \emph{$a$ divides $c$} if there is a number $b$
-such that $c = a\cdot b$. 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 Euclidean algorithm. The extended Euclidean algorithm
-allows to compute numbers $s$ and $t$ such that $a\cdot s + b\cdot t = \gcd(a,b)$.
+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$
+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}
+allows to compute integers $s,t\in\mathbb{Z}$ such that $a\cdot s + b\cdot t = \gcd(a,b)$.
+In particular, if $p$ is prime and $a\in\mathbb{N}$, there are integers $s,t\in\mathbb{Z}$
+such that
+$$
+p\cdot s + a\cdot t = 1 \Longleftrightarrow a\cdot t\equiv 1\pmod p \Longleftrightarrow p|(a\cdot t-1).
+$$
+The last equivalence introduces the notion of 'multiplicative inverse mod $p$', i.e.
+$a\cdot t \equiv 1\pmod p$ means that $t = a^{-1}$ if we consider the integers modulo
+a prime number $p$. The integers modulo a prime $p$ form a field, as introduced in the
+next subsection.
+
\subsection{Finite Fields}
An elementary notion in cryptographic mathematical theories, is the notion
of a finite field. A field is a set $K$ where the elementary mathematical
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.
+\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
+$$
+[a]_p \pm [b]_p := [a\pm b]_p,\qquad [a]_p\cdot [b]_p := [ab]_p.
+$$
+For division in a finite field, we recall that $a/b = a\cdot b^{-1}$ where $b^{-1}$ is
+the multiplicative inverse of $b$ modulo $p$, i.e. $[b]_p\cdot [b^{-1}]_p = [b\cdot b^{-1}]_p = [1]_p$.
+The multiplicative inverse can be computed by the extended Euclidean algorithm. Hence, we we define
+$$
+[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.\\
+
+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\}$.
+
\section{The Formal Verification}
projects / cfuerst / formal-numbers.git / commitdiff