C. Meadows. Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends. In IEEE Journal on Selected Areas in Communication, 21(1), pp. 44-54, 2003.
J. Clark and J. Jacob. A Survey of Authentication Protocol Literature. Unpublished manuscript, 1997.
B. Pierce. Foundational Calculi for Programming Languages. In Handbook of Computer Science and Engineering, chapter 139, CRC Press, 1996. Sections 1 and 2.
B. Pierce. Ibid. Section 3.
A. Pitts. Types, Chapter 1. Lecture notes for Computer Science Tripos, Cambridge University, 2002.
A. D. Gordon and A. S. A. Jeffrey. Authenticity by Typing for Security Protocols. In J. Computer Security 11(4), pp. 451-521, 2003. An extended version of this paper appears as Technical Report MSR-TR-2001-49, Microsoft Research, 2001. Note: I'd recommend skipping Section 5 and Appendix B.3 for now!
B. Blanchet. Cryptographic Protocol Verifier User Manual. Software Manual, Max Planck Institute, 2003. Note: we're using the spi-calculus syntax in this course, so you should concentrate on Sections 4 and 5.
A. D. Gordon and A. S. A. Jeffrey. Ibid. Section 5. Note: Read Appendix B.3 if you want the gorey details!
A. D. Gordon and A. S. A. Jeffrey. Cryptyc: Cryptograpic Protocol Type Checker. Software Tool, DePaul University, 2002.
H. R. Andersen. An Introduction to Binary Decision Diagrams. Lecture Notes, Technical Univresity of Denmark, 1998.
R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation In IEEE Trans. Computers C-35(8) pp. 677-691, 1986.
E. Clarke and D. Kroening. ANSI-C Bounded Model Checker User Manual. Technical Report, Carnegie Mellon University, 2003.
E. Clarke, D. Kroening and K. Yorav. Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking In Proc. Design and Automation Conf. pp. 368-371, 2003.
P. Lee and G. Necula. Research on Proof-Carrying Code for Mobile-Code Security. In Proc. DARPA Workshop on Foundations for Secure Mobile Code, 1997.
G. Necula and P. Lee. Safe Kernel Extensions Without Run-Time Checking In Proc. Symp. Operating Systems Design and Implementation. pp. 229-243, 1996.
G. Smith and D. Volpano. Secure Information Flow in a Multi-threaded Imperative Language. In Proc. ACM Symp. Principles of Programming Languages, pp. 355-364, 1998.
A. Myers. JFlow: Practical Mostly-Static Information Flow Control. In Proc. ACM Symp. Principles of Programming Languages, pp. 228-241, 1999.