Formal Correctness of Security Protocols

The author investigates proofs of correctness of realistic security protocols in a formal, intuitive setting. The protocols examined include Kerberos versions, smartcard protocols, non-repudiation protocols, and certified email protocols. This research advances significant extensions to the method of analysis, while the findings on the protocols analysed are novel and illuminating.