Kerberos Version IV: Inductive analysis of the secrecy goals

1. G. Bella, L. C. Paulson. Using Isabelle to Prove Properties of the Kerberos Authentication System. Proc. of DIMACS Workshop on Design and Formal Verification of Security Protocols, Orman and Meadows (eds.), 1997.

   Google Scholar 

2. G. Bella, L. C. Paulson. Mechanising BAN Kerberos by the Inductive Method. Proc. of Conference on Computer Aided Verification, Springer, LNCS Series, 1998.

   Google Scholar 

3. G. Bella, E. Riccobene. Formal Analysis of the Kerberos Authentication System. Journal of Universal Computer Science: Special Issue on Gurevich’s Abstract State Machine, Springer, 1997.

   Google Scholar 

4. S. M. Bellovin, M. Meritt. Limitations of the Kerberos authentication system. Computer Comm. Review, 20(5) 119–132, 1990.

   Article  Google Scholar 

5. S. H. Brackin. A HOL Extension of GNY for Automatically Analyzing Cryptographic Protocols. Proc. of Computer Security Foundations Workshop, IEEE Press, 1996.

   Google Scholar 

6. M. Burrows, M. Abadi, R. M. Needham. A logic of authentication. Proceedings of the Royal Society of London, 426:233–271, 1989.

   Article  MATH  MathSciNet  Google Scholar 

7. Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In Specification and Validation Methods, Oxford University Press, E. Börger (ed.), 1995.

   Google Scholar 

8. R. Kemmerer, C. Meadows, J. Millen. Three Systems for Cryptographic Protocol Analysis. Journal of Cryptology, 7(2), 79–130, 1994.

   Article  MATH  Google Scholar 

9. J. Kohl, B. Neuman. The Kerberos Network Authentication Service (Version V). Internet Request for Comment RFC-1510, 1993.

   Google Scholar 

10. J. Kohl, B. Neuman, T. Ts’o. The Evolution of the Kerberos Authentication Service. IEEE Press, 78–94, 1994.

    Google Scholar 

11. G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. Tools and Algorithms for the Construction and Analysis of Systems, Margaria and Steffen (eds.), LNCS1055, Springer Verlag, 147–166, 1996.

    Google Scholar 

12. G. Lowe. Casper: a Compiler for the Analysis of Security Protocols. Oxford University, Computing Laboratory, Technical Report, 1996.

    Google Scholar 

13. C. Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, 26(2), 113–131, 1996.

    Article  MATH  Google Scholar 

14. S. P. Miller, J. I. Neuman, J. I. Schiller, J. H. Saltzer. Kerberos authentication and authorisation system. Project Athena Technical Plan, Sec. E.2.1, 1–36, MIT, 1989.

    Google Scholar 

15. J. C. Mitchell, M. Mitchell, U. Stern: Automated Analysis of Cryptographic Protocols Using Murphi. Proc. of IEEE Symposium on Security and Privacy, 141–151, 1997.

    Google Scholar 

16. L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828.

    Google Scholar 

17. L. C. Paulson. Proving properties of security protocols by induction. Proc. of Computer Security Foundations Workshop, IEEE Press, 1997.

    Google Scholar 

18. L. C. Paulson. On Two Formal Analyses of the Yahalom Protocol. Cambridge University, Computer Laboratory, Technical Report No. 432, July 1997.

    Google Scholar 

19. L. C. Paulson. Inductive Analysis of the Internet Protocol TLS. Cambridge University, Computer Laboratory, Technical Report No. 440, Dec. 1997.

    Google Scholar 

20. S. Schneider. Verifying Authentication Protocols Using CSP. Proc. of Computer Security Foundations Workshop, IEEE Press, 1997.

    Google Scholar 

Download references