From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sun, 9 Apr 2017 07:02:13 +0000 (+0200)
Subject: Finalized formalization of discrete_log
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=2f878c8130646c1ad4cb0e8db76e68ab8fe95abf;p=cfuerst%2Fformal-numbers.git

Finalized formalization of discrete_log
---

diff --git a/discrete_log.txt b/discrete_log.txt
index 30b5143..c5c11a5 100644
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -88,6 +88,7 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
          {
             // result found
             ret = i*m + j;
+            print ret;
             // abort loop
             // Q: Is there a more comfortable way (e.g. break??)
             i = m-1; 
@@ -100,3 +101,4 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
    return ret;
 }
 
+
diff --git a/report/formal.pdf b/report/formal.pdf
index 55e74ad..600a46b 100644
Binary files a/report/formal.pdf and b/report/formal.pdf differ
diff --git a/report/formal.tex b/report/formal.tex
index 35e09c8..4bea1c0 100644
--- a/report/formal.tex
+++ b/report/formal.tex
@@ -428,9 +428,55 @@ hence we have shown $x^2\leq a < (x+1)^2$, and taking square roots shows the cla
 \subsection*{The RISCAL Formalization}
 %{\scriptsize \verbatiminput{../integerroot.txt}}
 {\scriptsize \verbatimboxed{../integerroot.txt}}
+
+\subsection{The Baby-Step Giant-Step Algorithm}
+At the Diffie-Hellmann Key-Exchange algorithm, we have encounterd the Discrete
+Logarithm problem. An algorithm to compute the discrete logarithm is the Baby-Step
+Giant-Step algorithm as sketeched before. A possible formalization might be formulated
+as follows:
+{\scriptsize \verbatimboxed{../discrete_log.txt}}
+Some comments on the formalization:
+\begin{itemize}
+ \item The first argument is the characteristic of the finite field, which is a prime.
+       Below 10, the primes are 2,3,5,7. Obviously, for $p=2$ we have no elements of
+       order $p-1$;
+ \item The condition that $g$ has to be of order $p-1$ is a major restriction. 
+ The only elements that satisfy this are given by
+\end{itemize}
+\begin{center}
+\begin{tabular}{|c|c|}
+\hline
+$p$ & Elements of order $p-1$\\
+\hline
+3  & 2 \\
+5  & 2,3\\
+7  & 3,5\\
+\hline 
+\end{tabular} 
+\end{center}
+\begin{itemize}
+ \item The element $a$ has obviously to be non-zero in $\mathbb{Z}_p$.
+\end{itemize}
+Having this thoughts in mind, we expect that the set of possible inputs might
+be shrinked dramatically. Indeed, the tuples with values less than 10, which
+are in our scope might be explictly enumerated by
+\begin{center}
+\begin{tabular}{c}
+$(p,g,a)$\\
+\hline
+$(3,2,1)$, $(3,2,2)$\\
+$(5,2,1)$,$(5,2,2)$,$(5,2,3)$,$(5,2,4)$\\ 
+$(5,3,1)$,  $(5,3,2)$,  $(5,3,3)$, $(5,3,4)$\\
+ $(7,3,1)$, $(7,3,2)$, $(7,3,3)$,  $(7,3,4)$, $(7,3,5)$, $(7,3,6)$ \\
+$(7,5,1)$,  $(7,5,2)$,  $(7,5,3)$, $(7,5,4)$,  $(7,5,5)$, $(7,5,6)$ 
+\end{tabular} 
+\end{center}
+which gives a total of 22 elements to check.
 \appendix
 
 
+
+
 \begin{thebibliography}{9}
 \bibitem{hardylittlewood}
 G.H. Hardy and E.M. Wright. \textit{An Introduction to the Theory of Numbers}.