Abstract reworked

diff --git a/report/formal.pdf b/report/formal.pdf
index b009ad1..a8fa64f 100644 (file)
Binary files a/report/formal.pdf and b/report/formal.pdf differ

diff --git a/report/formal.tex b/report/formal.tex
index 9d7f9f5..61ce817 100644 (file)
--- a/report/formal.tex
+++ b/report/formal.tex
@@ -76,12 +76,16 @@ We present a formal verification of algorithms that are used
 in Number Theory. Classic cryptographic algorithms rest
 on number theory, where abstract mathematical problems are presented
 and algorithms to solve them are discussed. These 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 {\rm RISCAL}, and put them into context of formal verification
-systems.
+used for concepts to ensure secure encryption of secret messages. Popular examples are the
+Diffie-Hellman-key exchange as well as the RSA public-key/private-key exchange procedure.
+In its quint essence, the validity and the secureness of this algorithms rests on the fact,
+that there is no efficient algorithm for computing decompositions of numbers into prime
+numbers and the hardness of the discrete logarithm problem. Still, its not hopeless, and one
+can formulate methods, which, for moderate small input, will solve the problems. We will
+formulate and prove formal correctness of algorithms that solve this problems,
+where we use the recently developed algorithm specification and verification system {\rm RISCAL}.
+It can be used, for automatic checking of finite models, and verify invariants as well as
+formulated post-conditions are indeed valid.
 \end{abstract}
 
 \tableofcontents