Initial revision of report

diff --git a/report/formal.pdf b/report/formal.pdf
new file mode 100644 (file)
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 (file)
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}