Original title: Formální analýza kryptografických protokolů
Translated title: Formal analysis of cryptographic protocols
Authors: Petrovský, Peter ; Martinásek, Zdeněk (referee) ; Člupek, Vlastimil (advisor)
Document type: Master’s theses
Year: 2015
Language: cze
Publisher: Vysoké učení technické v Brně. Fakulta elektrotechniky a komunikačních technologií
Abstract: [cze] [eng]
Táto diplomová práca sa zaoberá kryptografiou. Popisuje sa jej základné rozdelenie a problémy teórie čísel, ktoré musí riešiť. Taktiež sa zaoberá metódami, ktoré sa použí- vajú k ohodnoteniu formálnej bezpečnosti kryptografických protokolov z matematického hľadiska. Nakoniec sa analyzujú nástroje využívané k automatickému a poloautomatic- kému vyhodnoteniu bezpečnosti kryptografických protokolov. Popisuje sa spôsob práce s týmito nástrojmi a nakoniec sa otestuje bezpečnosť protokolov Kerberos, EKE a protokolov jednosmernej autentizácie využívajúcich symetrickú kryptografiu, funkciu HMAC a hashovaciu funkciu postupne v nástrojoch AVISPA, ProVerif a Scyther. Na záver je porovnanie výsledkov. This diploma thesis deals with cryptography. It describes its basic allocation and problems of number theory that needs to be addressed. It also deals with methods used to review the formal security of cryptographic protocols from a mathematical point of view. It analyse the tools used to automatic and semi-automatic evaluation of the safety of cryptographic protocols. It describes the process of working with these tools and finally test the security of protocols Kerberos, EKE and Unilateral authentication using symmetric cryptography, HMAC function and hash function. These tests are in tools AVISPA, ProVerif and Scyther. At the end is comparison of results.
Keywords: analysis; AVISPA; BAN logic; Cryptography; Dolev-Yao; EKE; Kerberos; ProVerif; Scyther; Unilateral authentication; analýza; AVISPA; BAN logika; Dolev-Yao; EKE; jednosmerná autentizácia; Kerberos; Kyptografia; ProVerif; Scyther

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/40020

Permalink: http://www.nusl.cz/ntk/nusl-594307


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses