From: Christoph Fuerst Date: Sun, 26 Mar 2017 19:13:27 +0000 (+0200) Subject: Contents on Report X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=314ab92b619751a02fdf763211f6ede75e40bdee;p=cfuerst%2Fformal-numbers.git Contents on Report --- diff --git a/report/formal.pdf b/report/formal.pdf index 9fc3fd3..603f73c 100644 Binary files a/report/formal.pdf and b/report/formal.pdf differ diff --git a/report/formal.tex b/report/formal.tex index 92c0619..f0d654a 100644 --- a/report/formal.tex +++ b/report/formal.tex @@ -1,10 +1,14 @@ \documentclass[a4paper,10pt]{scrartcl} -\usepackage[utf8]{inputenc} +\usepackage[utf8x]{inputenc} +\usepackage{lmodern} +\usepackage[T1]{fontenc} +\usepackage{verbatim} \usepackage{amsmath} \usepackage{amsthm} \usepackage{amssymb} \usepackage{listings} - +\usepackage{xcolor} +\usepackage{textcomp} % \newtheorem{thm}{Theorem}[section] \newtheorem{cor}[thm]{Corollary} @@ -25,9 +29,6 @@ \date{\today} \begin{document} - - - \maketitle \begin{abstract} @@ -44,6 +45,8 @@ developed in RISCAL, and put them into context of formal verification systems. \end{abstract} +\tableofcontents + \section{Introduction} \section{Mathematical and Cryptographic Preliminaries} @@ -173,17 +176,71 @@ $$ \end{lem} - \subsubsection*{The discrete Logarithm problem} - TODO - \subsection{The RSA cryptosystem} - TODO +\subsubsection*{The Discrete Logarithm problem} +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$.\\ + +The Diffie-Hellmann key exchange algorithm relies on the assumption, that given $a^x$ and +$a^y$ (without knowing $x$ and $y$), the expression $a^{xy}$ can not be efficiently computed, +i.e. the discrete logarithm problem is not effectively solvable. Effective solvable in this +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.\\ +TODO: Baby Step Giant Step Algorithm +\subsection{The RSA cryptosystem} +TODO + +\subsection{The Diffie-Hellmann cryptosystem} +TODO \section{The Formal Verification} +TODO: Describe algorithm Left-To-Right Exponentation \appendix \section{Listing of the developed Theory} - +{\scriptsize \verbatiminput{../numbertheory.txt}} + + +\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} +G.H. Hardy and E.M. Wright. \textit{An Introduction to the Theory of Numbers}. +Oxford University Press, 6. edition. 2008. + +\bibitem{LidlNiederreiter} +R. Lidl and H. Niederreiter. \textit{Introduction to finite fields and their applications}. +Cambridge University Press, 1986. + +\bibitem{Schreiner} +W. Schreiner. \textit{The RISC Algorithm Language (RISCAL), Tutorial and Reference}. +Research Institute for Symbolic Computation (RISC) Linz, 2017. + +\end{thebibliography} \end{document}