\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}
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
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
$$
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}}
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}
projects / cfuerst / formal-numbers.git / commitdiff