From: Christoph Fuerst Date: Fri, 31 Mar 2017 17:20:40 +0000 (+0200) Subject: Added cases X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=5c314d6bf2e252ffee8075075c035cda897b6360;p=cfuerst%2Fformal-numbers.git Added cases --- diff --git a/report/formal.pdf b/report/formal.pdf index aae5a1f..90947c5 100644 Binary files a/report/formal.pdf and b/report/formal.pdf differ diff --git a/report/formal.tex b/report/formal.tex index 59cdcb0..a487560 100644 --- a/report/formal.tex +++ b/report/formal.tex @@ -24,9 +24,9 @@ \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} @@ -41,11 +41,11 @@ We present a formal verification of algorithms that are used 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} @@ -61,11 +61,11 @@ 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{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}$ @@ -87,18 +87,18 @@ 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 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 @@ -165,7 +165,7 @@ $$ -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}. @@ -183,9 +183,9 @@ $$ \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$.\\ @@ -209,7 +209,7 @@ $$ 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.\\ @@ -245,7 +245,7 @@ by first representing $d$ in its binary representation, i.e. $$ 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: @@ -271,7 +271,7 @@ Let us analyze this in more detail. To gain insight, we might consider some conc 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}\\ @@ -295,7 +295,12 @@ 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'