Kerberos Version 4: Inductive Analysis of the Secrecy Goals
作者： Giampaolo Bella , Lawrence C. Paulson
DOI: 10.1007/BFB0055875
关键词:
摘要: An operational model of crypto-protocols is tailored to the detailed analysis secrecy goals accomplished by Kerberos Version IV. The faithful specification protocol presented MIT technical plan [14] — e.g. timestamping, double session key delivery mechanism are included. It allows an eavesdropper exploit shared keys compromised agents, and admits accidental loss expired keys. Confidentiality expressed from viewpoint each party involved in a run, with particular attention assumptions relies on. If such unrealistic, they highlight weaknesses protocol. This particularly so responder: suggests proves reasonable correction.
springer.com
acm.org 
sci-hub.se 参考文章(19)
Clifford Neuman, John T. Kohl, The Evolution of the Kerberos Authentication Service ,(1992)
Lawrence C. Paulson, On two formal analyses of the Yahalom protocol ,(1997)
Elvinia Riccobene, Giampaolo Bella, Formal Analysis of the Kerberos Authentication System. Journal of Universal Computer Science. ,vol. 3, pp. 1337- 1381 ,(1997)
Tobias Nipkow, Lawrence C. Paulson, Isabelle: A Generic Theorem Prover ,(1994)
Giampaolo Bella, Using Isabelle to Prove Properties of the Kerberos Authentication System ,(1997)
Yuri Gurevich, Evolving algebras 1993: Lipari guide Specification and validation methods. pp. 9- 36 ,(1995)
S. M. Bellovin, M. Merritt, Limitations of the Kerberos authentication system acm special interest group on data communication. ,vol. 20, pp. 119- 132 ,(1990) , 10.1145/381906.381946
Lawrence C. Paulson, Inductive analysis of the Internet protocol TLS ACM Transactions on Information and System Security. ,vol. 2, pp. 332- 351 ,(1999) , 10.1145/322510.322530
Catherine Meadows, The NRL Protocol Analyzer: An Overview☆ Journal of Logic Programming. ,vol. 26, pp. 113- 131 ,(1996) , 10.1016/0743-1066(95)00095-X
R. Kemmerer, C. Meadows, J. Millen, Three systems for cryptographic protocol analysis Journal of Cryptology. ,vol. 7, pp. 79- 130 ,(1994) , 10.1007/BF00197942