From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Thu, 30 Mar 2017 15:15:59 +0000 (+0200)
Subject: Described Left to Right Exponentation
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=855c803a0ef097020f3f0d9c728a0fb0605d168c;p=cfuerst%2Fformal-numbers.git

Described Left to Right Exponentation
---

diff --git a/algorithmicnumbertheory.pdf b/algorithmicnumbertheory.pdf
new file mode 100644
index 0000000..b8bac40
Binary files /dev/null and b/algorithmicnumbertheory.pdf differ
diff --git a/report/formal.pdf b/report/formal.pdf
index a45345d..06923ca 100644
Binary files a/report/formal.pdf and b/report/formal.pdf differ
diff --git a/report/formal.tex b/report/formal.tex
index 9a46f32..72af0e3 100644
--- a/report/formal.tex
+++ b/report/formal.tex
@@ -6,6 +6,8 @@
 \usepackage{amsmath}
 \usepackage{amsthm}
 \usepackage{amssymb}
+\usepackage{algorithm}
+\usepackage[noend]{algpseudocode}
 \usepackage{listings}
 \usepackage{xcolor}
 \usepackage{textcomp}
@@ -36,7 +38,7 @@ 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. This mathematical preliminaries are then 
+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
@@ -224,7 +226,50 @@ to obtain the same key. The key $K$ can now be used by a 'simpler' crypto-system
 simple displacement chiffre.
 
 \section{The Formal Verification}
-TODO: Describe algorithm Left-To-Right Exponentation
+\subsection{Left-to-Right Exponentation}
+The first algorithm, we are going to formally verify is so called 'Left-to-Right Exponentation'.
+In the RSA-algorithm, we encounter the problem of computing powers (where, for the moment, we
+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.
+$$
+This 'naive algorithm' requires $d$ multiplications of $c$. The Left-to-Right Exponentation proceeds
+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 
+$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:
+\begin{algorithm}[H]
+        \caption{Left-to-Right Exponentation}
+\begin{algorithmic}
+\Require{$c\in\mathbb{Z}$, $d\in\mathbb{N}$}
+\Ensure{$c^d$}
+\State $y \leftarrow 1$;
+\While{$n > 0$}
+\If{$n$ is odd}
+\State $y\leftarrow x\cdot y$;
+\EndIf
+\State $x\leftarrow x^2$;
+\State $n \leftarrow \lfloor n/2\rfloor$;
+\EndWhile
+\Return $y$.
+\end{algorithmic}
+\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
+$$
+{\rm Exp}(x,n) = 
+\begin{cases}
+ 1,\qquad & n =0\\
+ {\rm Exp}(x^2,n/2),\qquad & n \text{ is even}\\
+ 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. 
 
 \appendix
 \section{Listing of the developed Theory}