Formal Correctness of Security Protocols

Computer network security is critical to fraud prevention and accountability. Network participants are required to observe predefined steps called security prools, whose proof of correctness is evidence that each prool step preserves some desired properties.

The author investigates proofs of correctness of realistic security prools in a formal, intuitive setting. The prools examined include Kerberos versions, smartcard prools, non-repudiation prools, and certified email prools. The method ...