Seminář: Formal analysis of cryptographic protocols

Formal analysis of cryptographic protocols is a method of verifying the security of such protocols. It is based on the assumtion that the basic components of these protocols (cryptographic primitives) are perfect, and tries to discover information leakage. One the of best-known examples of formal analysis is the Lowe attack on the Needham-Schroeder protocol (after 15 years of protocol usage). Two tools for such formal analysis will be presented.