Bounded Model Checking of Security Protocols

Security protocols (aka cryptographic protocols) are key to the secure functioning of distributed systems in virtually all application domains (e.g. finance, transportation, telecommunications, e-government). Yet, they are notoriously difficult to get right. For this reason the development of automated tools for the analysis of security protocols has received a great deal of attention by the Computer Science community in the recent years. I will report on my experience in developing a SAT-based, bounded model checker for security protocols. I will then show, through concrete examples, how model checking contributed to the discovery of severe vulnerabilities in security protocols used in prominent online applications.