Cryptographic protocols in practice

Cílem této práce bylo v první části popsat požadavky na kryptografické protokoly. Dále měla být provedena klasifikace těchto protokolů a uvedeny konkrétní příklady. V další části se práce měla věnovat metodami, které jsou vhodné pro popis a modelování kryptografických protokolů. Práce se dále měla zabývat také analýzou kryptografických protokolů vhodnými analytickými prostředky. V praktické části měla být aplikována metoda CSP pro modelování kryptografických protokolů. Jako protokol vhodný pro modelování byl vybrán protokol Yahalom. Byly provedeny dvě analýzy. První analýza se týkala standardního protokolu Yahalom, který byl testován na požadavky kryptografických vlastností utajení a autentičnosti. Druhá analýza se zabývala možností prozrazení klíče, včetně ukázky postupu, jak k prozrazení dojde. První analýza neodhalila žádné oslabení, co se týče dvou zmíněných kryptografických vlastností. Pro demonstraci možností aplikace FDR byl protokol Yahalom upraven s cílem vyvolat situaci, kdy dojde k prozrazení klíče. Aplikace FDR následně našla přesný postup, který musí útočník učinit, aby se klíče zmocnil.The purpose of this work was first to describe the requirements for cryptographic protocols. Furthermore, the classification of these protocols should have been made with specific examples given. The aim of the next part of the work was to describe the methods which are suitable for description and modeling of cryptographic protocols. This work also addressed the analysis of cryptographic protocols by appropriate analytical means. The CSP method for modeling of the cryptographic protocols was applied in the practical part. The Yahalom protocol was selected as a protocol suitable for modeling. Two analysis was made. The first analysis concerned the standard version of the Yahalom protocol, which was tested to the requirements of cryptographic properties of the secrecy and authenticity. The second analysis was based on the possibility of disclosure of the key, including counterexamples and traces given by FDR. The first analysis did not reveal any weakening, in terms of two cryptographic properties. To demonstrate the possibility of FDR, Yahalom protocol was modified in order to cause the situation when the disclosure of keys appears. FDR then finds the exact procedure that an intruder must make to get the possession of the key.