@InBook{ basin.ea:model:2012, abstract = {Cryptographic protocols are communication protocols that use cryptography to achieve security goals such as secrecy, authentication, and agreement in the presence of adversaries. Examples of well-known cryptographic protocols are SSL/TLS [DR06], IKEV2 [KHNE10], and Kerberos [NHR05], which can be used, respectively, to secure web-based traffic, setup virtual private networks, and perform authentication in distributed environments. In order to ensure that such protocols always achieve their goals, they are designed under the assumption that the network is completely controlled by an adversary (also called the intruder or attacker). This means that the adversary can intercept, redirect, and alter data, have access to any operation that is available to legitimate agents, and even control one or more legitimate agents and thus access their keys. Given the hostility of the intended environment, it is not surprising that cryptographic protocols are difficult to design and are subject to subtle flaws, even when the cryptographic primitives used are themselves secure. }, author = {David Basin and Cas Cremers and Catherine Meadows}, booktitle = {Handbook of Model Checking}, chapter = 24, editor = {Edmund Clarke and Tom Henzinger and Helmut Veith}, language = {USenglish}, note = {To appear.}, publisher = {Springer }, title = {Model Checking Security Protocols}, year = 2012, user = {cremersc} }