ABSTRACT

Security protocols are an important and very often crucial element of security in computer systems. In open computer networks, especially in systems realizing goals of the public key infrastructure, these concurrent algorithms are often used during an exchange of information for, generally speaking, ensuring an adequate level of security of data transmitted over networks and electronic transactions. Their principal tasks include, among others, mutual authentication of communicating parties (users, servers) or a new session key distribution. Basically, they are most often applied as essential components of large systems, such as widely used communication protocols. Important examples of such systems are Kerberos, SSL/TLS, and Zfone. However in literature and applications, one can find errors in a protocol design. This

justifies a vital need to develop methods to specify and to verify their properties in order to find faults allowing unwanted behavior, which can lower the security level or even discredit it completely.