From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sat, 25 Mar 2017 09:23:19 +0000 (+0100)
Subject: Initial revision of report
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=0e60284641c44717286b4008061dda7359929d71;p=cfuerst%2Fformal-numbers.git

Initial revision of report
---

diff --git a/report/formal.pdf b/report/formal.pdf
new file mode 100644
index 0000000..8ff3840
Binary files /dev/null and b/report/formal.pdf differ
diff --git a/report/formal.tex b/report/formal.tex
new file mode 100644
index 0000000..626f3a6
--- /dev/null
+++ b/report/formal.tex
@@ -0,0 +1,38 @@
+\documentclass[a4paper,10pt]{scrartcl}
+\usepackage[utf8]{inputenc}
+\usepackage{listings}
+%opening
+\title{Formal Verification of Algorithms arising in Cryptography}
+\author{Christoph F\"urst\qquad Wolfgang Schreiner\\ Research Institute for Symbolic Computation (RISC) Linz}
+\date{\today}
+
+\begin{document}
+
+
+
+\maketitle
+
+\begin{abstract}
+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 
+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
+prove exactness of the treated algorithms. We present the theories 
+developed in RISCAL, and put them into context of formal verification
+systems.
+\end{abstract}
+
+\section{Introduction}
+
+\section{Mathematical and Cryptographic Preliminaries}
+
+\section{The Formal Verification}
+
+\appendix
+\section{Listing of the developed Theory}
+
+\end{document}