next up previous
Next: Appendix: Specifying Kerberos in Up: Using Isabelle to Prove Previous: Conclusion

References

1
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.
2
S. M. Bellovin, M. Meritt. Limitations of the Kerberos authentication system. Computer Comm. Review, 20(5) 119-132, 1990.
3
M. Burrows, M. Abadi, R. M. Needham. A logic of authentication. Proceedings of the Royal Society of London, 426:233-271, 1989.
4
G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, Margaria and Steffen (eds.), volume 1055 of Lecture Notes in Computer Science, Springer Verlag, 147-166, 1996.
5
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.
6
R. M. Needham, M. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12), 993-999, 1978.
7
L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828.
8
L. C. Paulson. Proving properties of security protocols by induction. Cambridge University, Computer Laboratory, Technical Report No. 409, 1996.
9
L. C. Paulson. Mechanized proofs of security protocols: Needham-Schroeder with public keys. Cambridge University, Computer Laboratory, Technical Report No. 413, 1997.
10
L. C. Paulson. Mechanized proofs for a recursive authentication protocol. Cambridge University, Computer Laboratory, Technical Report No. 418, 1997.
11
L. C. Paulson. On Two Formal Analyses of the Yahalom Protocol. Cambridge University, Computer Laboratory, Technical Report No. 432, 1997.



Giampaolo Bella
Mon Aug 4 18:43:12 BST 1997