Cryptographic protocols in practice

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