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