From: Christoph Fuerst Date: Mon, 3 Apr 2017 19:21:46 +0000 (+0200) Subject: Added source-listings, cleaned up discrete_log X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=2c78ac0c65ff2688c63dbad0e215ee6260cbea71;p=cfuerst%2Fformal-numbers.git Added source-listings, cleaned up discrete_log --- diff --git a/report/formal.pdf b/report/formal.pdf index 7a15370..55e74ad 100644 Binary files a/report/formal.pdf and b/report/formal.pdf differ diff --git a/report/formal.tex b/report/formal.tex index 23ee95d..35e09c8 100644 --- a/report/formal.tex +++ b/report/formal.tex @@ -38,6 +38,31 @@ \begin{center}\fbox{\box0}\end{center}% \endgroup} +\lstset{language=C++, + backgroundcolor=\color{black!5}, % set backgroundcolor + basicstyle=\ttfamily\tiny,% basic font setting + breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace + breaklines=true, % sets automatic line breaking + captionpos=b, % sets the caption-position to bottom + deletekeywords={...}, % if you want to delete keywords from the given language + escapeinside={\%*}{*)}, % if you want to add LaTeX within your code + extendedchars=true, % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8 + frame=single, % adds a frame around the code + keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible) + language=Octave, % the language of the code + morekeywords={*,...}, % if you want to add more keywords to the set + numbers=left, % where to put the line-numbers; possible values are (none, left, right) + numbersep=5pt, % how far the line-numbers are from the code + showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces' + 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 +} + +\newcommand{\CC}{C\nolinebreak\hspace{-.05em}\raisebox{.4ex}{\tiny\bf +}\nolinebreak\hspace{-.10em}\raisebox{.4ex}{\tiny\bf +}} +\def\CC{{C\nolinebreak[4]\hspace{-.05em}\raisebox{.4ex}{\tiny\bf ++}}} + %opening \title{Formal Verification of Algorithms arising in Cryptography} \author{Christoph F\"urst\qquad Wolfgang Schreiner\\ Research Institute for Symbolic Computation (RISC) Linz} @@ -78,6 +103,8 @@ $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)$. +An implementation of the extended Euclidean algorithm in \CC\, is formulated as follows: +{\tiny \lstinputlisting{../src/xGCD.cpp}} 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}$ such that @@ -220,14 +247,16 @@ i.e. the discrete logarithm problem is not effectively solvable. Effective solva context means that there is an algorithm which proceeds more effective than the brute-force method, which proceeds by computing $b^k\pmod p$ until $a\equiv b^x\pmod p$ is reached.\\ -We will now describe the Baby-Step/Giant-Step algorithm for computing the discrete logarithm. +For computing the discrete logarithm, the main algorithm is the Baby-Step Giant-Step algorithm. Suppose we are given an odd prime $p$, an element $g\in\mathbb{Z}_p$ and $a = a_0\in\mathbb{Z}$. -The algorithm proceeds by first compiling a table with entries $(i,t_i)$ where $t_i = g^i \pmod p$. -The table consists of $m := \lceil \sqrt{p-1}\rceil$ entries from zero to $m-1$. -In the next step, one computes $g^{-m}\pmod p$. If $a$ is in the second row of the table, -on reads of the index (in the first row), otherwise it computes $a_{i+1} = a_i g^{-m}\pmod p$. -At some stage between $i = 0$ and $m-1$ we find the index $j$ and return as solution $x=i\cdot m + j$. - +The algorithm proceeds by first compiling a table with entries $(i,t_i)$ where $t_i = g^i \pmod p$ +(computed by repeated multiplying modulo $p$). +The table consists of $m := \lceil \sqrt{p-1}\,\rceil$ entries from 0 to $m-1$. +In the next step, one computes $g^{-m}\pmod p$. Initialize an index $i$ with zero. +If $a_i$ happens to coincide with some $t_j$ where $0\leq j\leq m-1$, then the +algorithm terminates with $x=i\cdot m + j$, otherwise it computes $a_{i+1} = a_i g^{-m}\pmod p$. +An implementation of this algorithm in \CC\, might be written as follows: +{\tiny \lstinputlisting{../src/discrete_log.cpp}} \subsection{The RSA cryptosystem} At the RSA cryptosystem, named after its authors Rivest, Shamir and Adleman, the two @@ -334,7 +363,7 @@ y \leq y' \text{ and } $$ 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$. -\newpage + \subsection*{The RISCAL Formalization} {\scriptsize \verbatimboxed{../lefttoright.txt}} @@ -395,36 +424,12 @@ $$ y > a \Leftrightarrow (x^2+z) > a \Leftrightarrow x^2+2x+1 > a \Leftrightarrow (x+1)^2 > a, $$ hence we have shown $x^2\leq a < (x+1)^2$, and taking square roots shows the claim. -\newpage + \subsection*{The RISCAL Formalization} %{\scriptsize \verbatiminput{../integerroot.txt}} {\scriptsize \verbatimboxed{../integerroot.txt}} \appendix -% \section{Listing of Implementations} -% \lstset{language=C++, -% backgroundcolor=\color{black!5}, % set backgroundcolor -% basicstyle=\ttfamily\tiny,% basic font setting -% breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace -% breaklines=true, % sets automatic line breaking -% captionpos=b, % sets the caption-position to bottom -% deletekeywords={...}, % if you want to delete keywords from the given language -% escapeinside={\%*}{*)}, % if you want to add LaTeX within your code -% extendedchars=true, % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8 -% frame=single, % adds a frame around the code -% keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible) -% language=Octave, % the language of the code -% morekeywords={*,...}, % if you want to add more keywords to the set -% numbers=left, % where to put the line-numbers; possible values are (none, left, right) -% numbersep=5pt, % how far the line-numbers are from the code -% showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces' -% 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 -% } -% -% {\tiny \lstinputlisting{../src/primefactors.cpp}} \begin{thebibliography}{9} \bibitem{hardylittlewood} diff --git a/src/discrete_log.cpp b/src/discrete_log.cpp index 9421ba8..908d9db 100644 --- a/src/discrete_log.cpp +++ b/src/discrete_log.cpp @@ -14,50 +14,30 @@ using namespace std; void discrete_log(long p, long g, long a) { long m = -floor(-sqrt(p-1)); - cout << "So far we got: m=" << m << endl; long *A = new long[m]; long *b = new long[m]; + long gi, s, gim = 1; - A[0] = 1; - b[0] = a; + A[0] = 1; b[0] = a; for(int i=1;i