Abstract
Communications security is an ancient art. Julius Caesar is said to have encrypted his messages, shifting each letter three places along the alphabet. Mary Queen of Scots was convicted of treason after a cipher used in her letters was broken. Today’s postal system incorporates security features. The envelope provides a degree of secrecy. The signature provides authenticity (proof of origin), as do departmental stamps and letterheads. Networks are vulnerable: messages pass through many computers, any of which might be controlled by an adversary, who thus can capture or redirect messages. People who wish to communicate securely over such a network can use cryptography, but if they are to understand each other, they need to follow a protocol : a pre-arranged sequence of message formats. Protocols can be attacked in many ways, even if encryption is unbreakable. A splicing attack involves an adversary’s sending a message composed of parts of several old messages. This fake message may have the correct format, fooling an honest party. The adversary might be able to masquerade as somebody else, or he might obtain a secret key.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
(2002). 10. Case Study: Verifying a Security Protocol. In: Nipkow, T., Wenzel, M., Paulson, L.C. (eds) Isabelle/HOL. Lecture Notes in Computer Science, vol 2283. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45949-9_10
Download citation
DOI: https://doi.org/10.1007/3-540-45949-9_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43376-7
Online ISBN: 978-3-540-45949-1
eBook Packages: Springer Book Archive