Original title:
Databáze specifikací bezpečnostních protokolů
Translated title:
Specifications Database of Security Protocols
Authors:
Hadaš, Petr ; Trchalík, Roman (referee) ; Očenášek, Pavel (advisor) Document type: Master’s theses
Language:
cze Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[cze][eng]
Diplomová práce popisuje čtyři nástroje určené pro verifikaci bezpečnostních protokolů Athena, Casper, Isabelle a Murphi. U každého je uvedena stručná charakteristika a část implementace protokolu Needham Schroeder. Součástí je také srovnání vybraných nástrojů. Druhá část práce podrobně popisuje nástroj Athena a uvádí příklady verifikovaných protokolů. U každého protokolu je uvedena specifikace komunikace, odhalený útok a výsledky vlastní verifikace. Na závěr práce porovnává výsledky verifikace s již publikovanými útoky.
This paper describes four tools for verification security protocols Athena, Casper, Isabelle and Murphi. Each tool is briefly characterized and implementation of protocol Needham Schroeder. One part of this paper is comparing of selected tools. The second part of this paper describes in detail a tool Athena and mentions examples of verified protocols. By each protocol is stated a specifications of communication, a detected attack and results of own verification. At the end compares this paper verification results with already publicated attacks.
Keywords:
Andrew Secure RPC; Athena; authentication; Casper; Isabelle; Murphi; Needham Schroeder; Security protocols; verification; Woo Lam; Yahalom; Andrew Secure RPC; Athena; autentizace; Bezpečnostní protokoly; Casper; Isabelle; Murphi; Needham Schroeder; verifikace; Woo Lam; Yahalom
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/54033