From: Christoph Fuerst Date: Sat, 25 Mar 2017 09:44:07 +0000 (+0100) Subject: Structure, first contents on mathematics X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=61f7de4432cd6f5bddc64c7e7daff6201a6c1f09;p=cfuerst%2Fformal-numbers.git Structure, first contents on mathematics --- diff --git a/report/formal.pdf b/report/formal.pdf index 8ff3840..ccfdd39 100644 Binary files a/report/formal.pdf and b/report/formal.pdf differ diff --git a/report/formal.tex b/report/formal.tex index 626f3a6..a4dca18 100644 --- a/report/formal.tex +++ b/report/formal.tex @@ -1,5 +1,8 @@ \documentclass[a4paper,10pt]{scrartcl} \usepackage[utf8]{inputenc} +\usepackage{amsmath} +\usepackage{amsthm} +\usepackage{amssymb} \usepackage{listings} %opening \title{Formal Verification of Algorithms arising in Cryptography} @@ -29,6 +32,23 @@ systems. \section{Introduction} \section{Mathematical and Cryptographic Preliminaries} +One of the most fundamental notions in mathematics is without doubt +the term \emph{divisor}, we say that \emph{$a$ divides $c$} if there is a number $b$ +such that $c = a\cdot b$. Among all divisors of two numbers $a$,$b$ there is +a unique \emph{greatest} common divisor of $a$ and $b$, denoted by $\gcd(a,b)$ +that is computed by the Euclidean algorithm. The extended Euclidean algorithm +allows to compute numbers $s$ and $t$ such that $a\cdot s + b\cdot t = \gcd(a,b)$. +\subsection{Finite Fields} +An elementary notion in cryptographic mathematical theories, is the notion +of a finite field. A field is a set $K$ where the elementary mathematical +operations of addition, subtraction, multiplication and division are applicable. +While the classic examples, the field of real numbers $\mathbb{R}$ and the +complex numbers $\mathbb{C}$, are infinite fields, the focus in cryptographic +applications is on \emph{finite fields}. A finite field with $p$ elements, where +$p$ is prime, is usually written as $\mathbb{Z}_p = \mathbb{Z}/p\mathbb{Z}$, +and consists of the elements $\{0,1,\ldots,p-1\}$. The number $p$ is called the +\emph{characteristic} of $\mathbb{Z}_p$, in fact, the characteristic of every +finite field is a prime power. \section{The Formal Verification}