Formal analysis of Kerberos 5

DOI10.1016/J.TCS.2006.08.040MaRDI QIDQ860899zbMATH OpenOpenAlexFDO

Authors Frederick Butler, Iliano Cervesato, Aaron D. Jaggard, Christopher Walstad, Andre Scedrov

Publication date 9 January 2007

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2006.08.040

zbMATH Keywords

formal methodssecurity protocol analysisKerberos protocol

Mathematics Subject Classification ID

Authentication, digital signatures and secret sharing (94A62)

Recommendations

• Cryptographically sound security proofs for basic and public-key Kerberos
• scientific article; zbMATH DE number 1543079
• Breaking and fixing public-key Kerberos
• Formal correctness of security protocols.
• Inductive Proofs of Computational Secrecy

Cites work

• scientific article; zbMATH DE number 1588477 (Why is no real title available?)
• scientific article; zbMATH DE number 1024060 (Why is no real title available?)
• scientific article; zbMATH DE number 1746674 (Why is no real title available?)
• Conditional rewriting logic as a unified model of concurrency
• Formal analysis of Kerberos 5
• On the security of public key protocols
• Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types
• Using encryption for authentication in large networks of computers

Cited in

(10)

• scientific article; zbMATH DE number 1543079 (Why is no real title available?)
• Cryptographically sound security proofs for basic and public-key Kerberos
• Emerging issues and trends in formal methods in cryptographic protocol analysis: twelve years later
• Rule-based static analysis of network protocol implementations
• Bounded memory Dolev-Yao adversaries in collaborative systems
• Formal analysis of Kerberos 5
• Soft constraint programming to analysing security protocols
• Protocol composition logic (PCL)
• Formal correctness of security protocols.
• Breaking and fixing public-key Kerberos

Describes a project that uses

Uses Software

• Maude

This page was built for publication: Formal analysis of Kerberos 5

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q860899)