Verifikace bezpečnostních protokolů

Verification of Security Protocols

Ph.D. thesis principal points

Czech

Bezpečnostní protokoly používají šifrování pro vytvoření privátních komunikačních kanálů v nezabezpečené síti. Pro dokázání jejich bezpečnosti se používá různých přístupů. Při formálním dokazování jsou demonstrovány pokusy útočníka o prolomení protokolu a odposlechnutí komunikace. Diplomová práce se zabývá souhrnem a analýzou jednotlivých formálních metod používaných pro dokazování těchto protokolů. Při demonstraci použití jednotlivých metod jsem se zaměřil na vyzdvižení specifických vlastností bezpečnostních protokolů.

In this paper an overview of the state of the art in the application of formal methods of cryptographic protocol analysis is given. Formal methods can be used in various phases of the design, such as specification, construction and verification. Up to now, most of the work concentrated on the formal verification of protocols, and in particular, on the application of modal logics of knowledge and belief for modeling and analyzing protocols. Further approaches represent model checking and inductive methods. Using formal methods in the specification of cryptographic protocols is an emerging area of research, while formal methods for construction of protocols in a systematic way are just appearing.

komunikace, bezpečnostní protokol, verifikace, zabezpečení, autentizace, veřejný klíč, privátní klíč, Needham-Schroeder, BAN logika, theorem proving

communication, security protocol, verification, protection, authentication, public key, private key, Needham-Schroeder, BAN logic, theorem proving

OČENÁŠEK, P.

20. 6. 2003

Fakulta informačních technologií VUT v Brně

Brno

54

https://www.fit.vut.cz/research/publication/7464/

msc_thesis.pdf