Course Readings

Primary Topics

• Course Outline
• Fundamental Concepts
• Calculus for Reasoning About Access Control, Delegation, and Roles
• Role-Based Access Control
• Simple Public Key Infrastructure (SPKI)
• Economic Crime

Additional Topics

• Kerberos
• Public Key Infrastructure
• Secure Email
• BAN Logic
• Medical Records
• Security and Information Assurance Education
• Common Criteria for Information Technology Security Evaluation

Course Outline

• Susan Older and Shiu-Kai Chin. Formal Methods for Assuring Security of Protocols. The Computer Journal, Vol. 45, No. 1, 2002

Fundamental Concepts

• Jerome Saltzer, Michael Schroeder. The Protection of Information in Computer Systems. Proceedings IEEE 63, 9 (Sept. 1975), 1278-1308
• Butler Lampson. Protection. Proceedings 5th Princeton Conference on Information Sciences and Systems, Princeton, 1971, 437.

Additional Background

• D.E. Bell, L.J. La Padula. Secure Computer System: Unified Exposition and Multics Interpretation, Technical Report ESD-TR-75-306, MITRE Corporation, Bedford, MA, March 1976.
• Department of Defense. DoD 5200.28-STD. Department of Defense Trusted Computer System Evaluation Criteria, December 1985.

Access Control Logic

• Martin Abadi, Michael Burrows, Butler Lampson, Gordon Plotkin. A Calculus for Access Control in Distributed Systems. ACM Transactions on Programming Languages and Systems, Vol. 15, No. 4, September 1993. 706-734.
• Butler Lampson, Martin Abadi, Michael Burrow, Edward Wobber. Authentication in Distributed Systems: Theory and Practice. ACM Transactions on Computer Systems, Vol. 10, No. 4, November 1992, 265-310.
• Edward Wobber, Martin Abadi, Michael Burrows, Butler Lampson. Authentication in the Taos Operating System. ACM Transactions on Computer Systems, Vol. 12, No. 1, February 1994, 3-32.
• Jon Howell, David Kotz. A Formal Semantics for SPKI. Technical Report TR 2000-363, March 2000, Dept. of Computer Science, Dartmouth College, Hanover, NH.

Additional Background

• Morrie Gasser, Andy Goldstein, Charlie Kaufman, Butler Lampson. The Digital Distributed System Security Architecture. Proceedings 12th National Security Conference. NIST/NCSC, 1989, 305-319.
• Andrew Birrell Andy Hisgen, Chuck Jerian, Timothy Mann, Garret Swart. The Echo Distributed File System. Technical Report 111, Systems Research Center, 1993, Digital Equipment Corp., Palo Alto, California.

Simple Public Key Infrastructure/Simple Distributed Security Initiative (SPKI/SDSI)

• C. Ellison, B. Frantz, B. Lampson, R. Rivest, B. Thomas, T. Ylonen. SPKI Certificate Theory. RFC 2693. ftp://ftp.isi.edu/in-notes/rfc2693.txt
• Ronal Rivest, Butler Lampson. SDSI - A Simple Distributed Security Infrastructure. http://theory.lcs.mit.edu/~cis/sdsi.html
• Dwaine Clarke, Jean-Emile Elien, Carl Ellison, Matt Fredette, Alexander Morcos, Ronald Rivest. Certificate Chain Discovery in SPKI/SDSI. To appear in Journal of Computer Security.  Draft of September 13, 2001.
• Martin Abadi. On SDSI's linked local name spaces. Journal of Computer Security. Vol. 6, No. 1-2, 1998, 3-21.

Role-Based Access Control

• David Ferraiolo, John Barkley, D. Richard Kuhn. A Role-Based Access Control Model and Reference Implementation Within a Corporate Intranet. ACM Transactions on Information and System Security, Vol. 2, No. 1, February 1999, 34-64.
• David Ferraiolo, Ravi Sandhu, Seban Gavrila, D. Richard Kuhn, Ramaswamy Chandramouli. Proposed NIST Standard for Role-Based Access Control. ACM Transactions on Information and System Security, Vol. 4, No. 3, August 2001, 224–274.
• David Ferraiolo, D. Richard Kuhn. Role Based Access Control. Proceedings of the 15th Annual Conference on National Computer Security. National Institute of Standards and Technology, Gaithersburg, MD, 1992, 554-563.

Economic Crime

• Norman A. Willox, Jr. & Thomas M. Regan. Identity Fraud: Providing A Solution. Journal of Economic Crime Management, Vol. 1, Issue 1, Summer 2002.
• Edward J. Potter. Customer Authentication: The Evolution of Signature Verification in Financial Institutions. Journal of Economic Crime Management, Vol. 1, Issue 1, Summer 2002.
• Robert Jones. Taming the Beast: The Electronification of the U.S. Check System. Journal of Economic Crime Management, Vol. 1, Issue 1, Summer 2002.
• Tom Arnold. An Electronic Citadel: A Method For Securing Credit Card And Private Consumer Data In E-Business Sites And Database Systems. Journal of Economic Crime Management, Vol. 1, Issue 1, Summer 2002.

Back to top

Kerberos Protocol

• J. Kohl, C. Neuman. RFC 1510. The Kerberos Network Authentication Service (V5). September 1993.
• Don Davis, Ralph Swick. Workstation Services and Kerberos Authentication at Project Athena. Technical Report. March 17, 1989.
• Kerberos home page for software and documentation.

Back to top

Public Key Infrastructure

• Peter Gutmann. PKI: It's Not Dead, Just Resting. IEEE Computer, Vol. 35, No. 8, August 2002, 41-49.
• Web Site for PKIX, the public key infrastructure based on X.509.
• Thumrongsak Kosiyatrakul, Susan Older, Shiu-Kai Chin. Formal Verification of Authentication Protocols that Use the X.509 Standard for Public Key Distribution.  International Joint Conference on Automated Reasoning (IJCAR) June 18 - June 23, 2001 in Siena, Italy.

Back to top

Secure Email

Internet Email Standard

• David H. Crocker. RFC 822. Standard for the Format of ARPA Internet Text Messages. August 1982.

Privacy Enhanced Mail (PEM)

• J. Linn. RFC 1421. Privacy Enhancement for Internet Electronic Mail: Part I: Message Encryption and Authentication Procedures. February 1993.
• S. Kent. RFC 1422. Privacy Enhancement for Internet Electronic Mail: Part II: Certificate-Based Key Management. February 1993.
• D. Balenson.  RFC 1423. Privacy Enhancement for Internet Electronic Mail: Part III: Algorithms, Modes, and Identifiers. February 1993.
• B. Kaliski. RFC 1424. Privacy Enhancement for Internet Electronic Mail: Part IV: Key Certification and Related Services. February 1993.

Formal Verification and Synthesis of Secure Email Protocols

• Dan Zhou, Shiu-Kai Chin. Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol. Presented at FM'99 World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999.
• Dan Zhou, Joncheng Kuo, Susan Older, Shiu-Kai Chin. Formal Development of Secure Email. Presented in the Hawaii International Conference on System Sciences, Techniques for Secure Systems Development, Island of Maui, January 5 - 8, 1999.
• Dan Zhou, Shiu-Kai Chin, Verifying Privacy Enhanced Mail Functions with Higher Order Logic. Network Threats, Rebecca N. Wright and Peter G. Neumann (eds), DIMACS Series in Discrete Mathematics and Computer Science, Vol 38, 1998, pp. 11- 20.
• Shiu-Kai Chin, Dan Zhou. Formal Verification of Security Properties of Privacy Enhanced Mail. Technical Report, Department of Electrical Engineering and Computer Science, Syracuse University, Syracuse, NY, 1997.

Back to top

BAN Logic

• Michael Burrows, Martin Abadi, Roger Needham. A Logic of Authentication. SRC Research Report 39, Systems Research Center, Digital Equipment Corporation, Palo Alto, CA, 1990.

Back to top

Medical Records

• D.W. Chadwick, P.J. Crook, A.J. Young, D.M. McDowell, T.L. Dornan, J.P. New. Using the internet to access confidential patient records: a case study. BMJ, Vol. 321, September 2000, 612 - 614.

Back to top

Security and Information Assurance Education

• Cynthia Irvine, Shiu-Kai Chin, Deborah Frincke. Integrating Security into the Curriculum. IEEE Computer, December 1998.
• Susan Older, Shiu-Kai Chin. Building a Rigorous Foundation for Assurance into Information Assurance Education. to appear in Volume 1, Number 2 of the George Washington University Journal of Information Security.

Back to top

NIST Common Criteria for Information Technology Security Evaluation

• Part 1: Introduction and general model, August 1999, Version 2.1, CCIMB-99-031
• Part 2: Security functional requirements, August 1999, Version 2.1, CCIMB-99-032
• Part 3: Security assurance requirements, August 1999, Version 2.1, CCIMB-99-033

Back to top