The design and security analysis of protocols that use cryptographic primitives is one of the most fundamental and challenging areas of computer security research. Relatively succinct but subtle authentication, key exchange, negotiation, authorization, and related protocols are the building blocks for secure distributed systems. Protocol analysis is a successful scientific area with two important but historically independent foundations, one based on symbolic computation and one based on computational complexity theory. Here we highlight joint work with Cervesato, Jaggard, Tsay, and Walstad on the formal analysis of the Kerberos 5 authentication protocol suite. This work discovered a serious vulnerability in the Kerberos public-key extension and caused a Microsoft security patch for Windows 2000 and Windows XP operating systems. The work contributed to the reformulation of the IETF standard for Kerberos public-key extension and provided security proofs of the corrected version of the protocol, the latter jointly with Backes. The flaw discovered is not a flaw in implementation or in cryptography, but a protocol-level, structural flaw, which is present even when the underlying cryptographic operations and network infrastructure operate normally. The methodology developed in this work is applicable to a wide range of network security protocols. We also discuss current joint work with Blanchet on mechanized proofs of authentication and key secrecy properties of Kerberos 5, both with and without its public-key extension.