Security Protocols and Threat Models – Security and Privacy via The Applied π-Calculus
Protocols connect the many devices used in our personal and professional lives. Hence we require
assurances that they are secure in the face of threats. Security is too important to leave to intuition and experience alone. We need methodologies to precisely determine our security goals. A security property is one that holds despite the best efforts of an attacker, as captured by a threat model. When attacking a protocol, an eavesdropper may
inject messages leading to sessions being hijacked and other data breaches. This textbook goes from intuition, to theory, to tools, explaining different security properties. Ubiquitous protocols keep the discussion real: ePassport protocols used at border checkpoints; the EMV protocol for contactless payments; and Open ID Connect used to sign in to websites. Even threats enabling car theft via relay attacks are taken into consideration by authenticating proximity. The book also analyses threats to privacy such as tracking, mitigated by making sessions unlinkable.
Authors: Reynaldo Gil-Pons, Ross Horne, Sjouke Mauw, Felix Stutz, and Semen Yurko