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