UVa Security Group Bibliography

Like everything else on the web, this document is merely a starting point. There are a lot of comprehensive security resources available on the web. Rather than duplicating their efforts, this document presents an introduction to some of the most important aspects of security. Where possible, pointers to more in-depth information is presented.

Please note that this bibliography is under construction. Please send your comments, criticism, or suggested improvements to Darrell.

Cryptography

Network Security

Protocols and Proof Systems

The UVa CPAL system

Existing Systems

Applications

UVa Legion Security

Logics

Firewalls

Political / Legal / Ethical Issues

Other Security Sites

Cryptography

Network Security

General Overviews

• Kaufman, C., R. Perlman, M. Speciner, Network Security, Private Communication in a Public World, Prentice-Hall, 1995.
• Stallings, W., Network and Internetwork Security, Principles and Practice, Prentice-Hall, 1995.

Protocols and Proof Systems

The UVa CPAL System

• Yasinsac, Alec, and Wm. A. Wulf, "A Formal Semantics for Evaluating Cryptographic Protocols", University of Virginia, Technical Report # CS-93-53, August 1993

Existing Systems

• Sape J. Mullender, Andrew S. Tanenbaum, "The Design of a Capability-Based Distributed Operating System", The Computer Journal, Vol. 29, No. 4, pp. 289-300, March 1986
• Morris, James H., et al., "Andrew: A distributed personal computing environment", Communications of ACM, vol. 29, no. 3, March 1986
• Neuman, B. C., T. Y. Ts'o, "Kerberos: An Authentication Service for Computer Networks," IEEE Communications, Vol. 32, pp. 33-38, Sept. 1994
• http://www.fish.com/~zen/satan.html
• Tom Parker and Denis Pinkas, "SESAME Technology Version 3, Overview,"
• http://www.esat.kuleuven.ac.be/cosic/sesame/doc-txt/overview.txt, May 1995

Applications

Pretty Good Privacy

• Garfinkel, S., PGP: Pretty Good Privacy, O'Reilly & Associates, 1995.
• Zimmermann, P.R., PGP: Source Code and Internals, MIT Press, 1995.
• Zimmermann, P.R., The Official PGP Users Guide, MIT Press, 1995.

Privacy Enhanced Mail (PEM)

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

These and many other fascinating (if unrelated) Internet Requests for Comments can be found at http://www.cis.ohio-state.edu/hypertext/information/rfc.html

KryptoKnight

• Molva, R., G. Tsudik, E. Van Herreweghen, S. Zatti, "KryptoKnight Authentication and Key Distribution System," European Symposium on Research in Computer Security, 1992, pp. 155-174.
• Janson, P., G. Tsudik, M. Yung, "KryptoKnight Protocol Cookbook", in submission, 1994.

Monetary Transactions

• Internet Keyed Payment Protocols
• Digicash Publications
• Commerce on the Internet (Netscape)
• CommerceNet
• Internet Credit Card Encrypter & Credit Card Verification Server
  (This one scares me…)
• NIST Electronic Commerce Integration Facility
• Microsoft's Private Communication Technology Protocol
• Microsoft & Visa Secure Transaction Technology

WWW Security

• Netscape Standards (including Secure Socket Layer)
• EIT's Secure-HTTP
• Web Transaction Security: The IETF WTS Working Group Home Page

NFS and other File Systems

Apps - Databases

Unix Security

UVa Legion Security

Legion Tech Reports

• Wulf, Wm. A., C. Wang, D. Kienzle, "A New Model of Security for Distributed Systems," University of Virginia, Department of Computer Science, Technical Report TR-95-34, August 1995.

CORBA

• Deng, R.H., S.K. Bhonsle, W. Wang, A.A. Lazar, "Integrating Security in CORBA Based Object Architectures," ???
• Fairthorne, B.(ed.), OMG White Paper on Security, OMG Security Working Group, April 1994.

Vaguely Legion-Related

• Bull, J.A., L. Gong, K.R. Sollins, "Towards Security in Open Systems Federation," European Symposium on Research in Computer Security, 1992 ESORICS 92, pp. 3-20.
• Barkley, John (ed), Security in Open Systems, NIST Special Publication 800-7, July 1994.
• Denning, P.J. (ed.), Computers Under Attack - Intruders, Worms, and Viruses, ACM Press, Addison-Wesley, 1990.

Logics

Firewalls

• Cheswick, W., and S. Bellovin, Firewalls and Internet Security: Repelling the Wily Hacker, Addison-Wesley, Reading Mass., 1994.

Political / Legal / Ethical Issues

• "Review and Analysis of U.S. Laws, Regulations, and Case Laws Pertaining to the Use of Commercial Encryption Products for Voice and Data Communications", in Building In Big Brother, The Cryptographic Policy Debate, Lance J. Hoffman, Editor, Springer-Verlag 1994, pp. 435-448
• Zimmerman, Philip, "Pretty good Privacy: Public Key Encryption for the Masses" in Building In Big Brother, The Cryptographic Policy Debate, Lance J. Hoffman, Editor, Springer-Verlag 1994, pp. 93-110
• Denning, Dorothy E., "The U. S. Key Escrow Encryption Technology" in Building In Big Brother, The Cryptographic Policy Debate, Lance J. Hoffman, Editor, Springer-Verlag 1994, pp. 111-118
• Micali, Silvio, "Fair Cryptosystems" in Building In Big Brother, The Cryptographic Policy Debate, Lance J. Hoffman, Editor, Springer-Verlag 1994, pp. 149-173
• Silvio Micali, "Fair Public-Key Cryptosystems" Technical Report, Laboratory for Computer Science, MIT, March 25, 1993
• Froomkin, A. Michael, "The Constitutionality of Mandatory Key Escrow - A First Look" in Building In Big Brother, The Cryptographic Policy Debate, Lance J. Hoffman, Editor, Springer-Verlag 1994, pp. 413-434
• Parent, W. A., "Privacy, Morality, and the Law" in Ethical Issues in the Use of Computers, Deborah G. Johnson and John W. Snapper, Wadsworth Publishing, Belmont, Ca. 1985, pp 201-214
• Harris, Martha, "Encryption - Export Control Reform" in Building In Big Brother, The Cryptographic Policy Debate, Lance J. Hoffman, Editor, Springer-Verlag 1994, pp. 239-240
• "Attorney General Makes Key Escrow Announcements", Dept. of Justice, Feb. 4, 1995 in Building In Big Brother, The Cryptographic Policy Debate, Lance J. Hoffman, Editor, Springer-Verlag 1994, pp. 241-242
• "Digital Telephony and Communications Privacy Improvement Act of 1994" Aug 9, 1994 in Building In Big Brother, The Cryptographic Policy Debate, Lance J. Hoffman, Editor, Springer-Verlag 1994, pp. 325-342
• "EFF Statement on and Analysis of Digital Telephony Act", Electronic Frontier Foundation, in Building In Big Brother, The Cryptographic Policy Debate, Lance J. Hoffman, Editor, Springer-Verlag 1994, pp. 354-361
• Diffie, Whitfield, "The Impact of a Secret Cryptographic standard on Encryption, Privacy, Law Enforcement and Technology" in Building In Big Brother, The Cryptographic Policy Debate, Lance J. Hoffman, Editor, Springer-Verlag 1994, pp. 393-399

Other Security Sites

General Information

• Texas Netinfo
  (http://wwwhost.ots.utexas.edu/netinfo/security.html)
• Yahoo Security Index
  (http://www.yahoo.com/Computers_and_Internet/Security_and_Encryption/)
• http://www.research.att.com/

Commercial Security Providers

• Trusted Information Systems

Organizations for Freedom, etc.

• Electronic Privacy Information Center
• HotWired Index of Privacy Resources
• CPSR (Computer Professionals for Social Responsibility)
• ACM (Association for Computing Machinery)

Alphabet Soup

• NIST Computer Security Resource Clearinghouse
• CERT (Computer Emergency Response Team)
• NASIRC (NASA Automated Systems Incident Response Capability)
• FIRST (Forum of Incident Response and Security Teams)
• COAST (Computer Operations, Audit, and Security Technology)
• AUSCERT (Australian Computer Emergency Response Team)
• DFN-CERT (Computer Emergency Response Team for the German Research Network)

Hacker Culture & Stuff

• Brunner, John, The Shockwave Rider, Del Rey / Ballantine Books, 1975, pp. 280.
• Stoll, Clifford, The Cuckoo's Egg: Tracking a Spy Through the Maze of Computer Espionage", Doubleday, 1989, pp. 326.
• Cyberantropology Bibliography
  (http://www.clas.ufl.edu/anthro/cyberanthro-biblio.html)
• The Electronic Frontier Foundation
• Cypherpunks Archive

People with Interesting Security Pages

• Ron Rivest
• Dorothy Denning

Here begins all the stuff I have yet to sort or categorize. Proceed at your own risk

Cryptography Background

• Dorothy Denning. "Cryptography and data security". Addison-Wesley, 1982
• National Bureau of Standards(NBS). Data Encryption Standard. Federal Information Processing Standard, Publication 46, NBS, Washinton, D.C., January 1977
• T. ElGamal, "A public Key Cryptosystem and a Signature Scheme Based on Discrete Logarithms", IEEE Transactions on Information Theory, IT-31 (4), pp 469-472
• U.S. Department of Commerce, NIST, "Digital Signature Standard", FIPS PUB 186, May 19, 1994
• M. Riordan, "Exportable RIPEM/SIG Available," ftp://ripem.msu.edu/pub/cypt/ripem/ripemsig/posting. 1994
• R. Rivest, A. Shamir, and L. Adleman, "A Method for Obtaining Digital Signatures and Public-key cryptosystems", Communications of ACM, vol. 21, no. 2 Feb. 1978, pp. 120-126
• Bruce Schneier, "Applied Cryptography", John Wiley & Sons, INc. 1994
• U. Feige, A. Fiat, and A. Shamir. "Zero-knowledge proffs of Identity" Journal of Cryptology, 1:77-94, 1988

Historical Interest

• Kahn, "Code Breakers", 1967
• Diffie, W., "The First Ten Years of Public Key Cryptography", Proceedings of The IEEE, Vol 76, No. 5, May 1988, pp 560-577
• Dennis, J., and van Horn, E., "Programming Semantics for Multiprogrammed Computations", Communications of the ACM, v9 n3, March 1966, pp 143-155.
• Graham, R., "Protection in an Information Processing Utility", Communications of the ACM, v11 n2, May 1968.
• Graham, G. and Denning, P., "Protection--Principles and Practice", Proceedings 1972 Joint Computer Conference, pp 417-29.
• Branstad, D., "Privacy and Protection in Operating Systems", Computer, v6 n1, January 1973, pp 43-46.
• Lampson, B., "A Note on the Confinement Problem", Communications of the ACM, v16 n 10, October 1973, pp 613-615.
• Fabry, R, "Capability-based Addressing", Communications of the ACM, v17 n 7, July 1974.
• Lampson, B., "Protection", Proceedings of the 5th Symposium on Operating Systems, v8 n1, January 1974, pp 18-24.
• Saltzer, J., "Protection and the Control of Information Sharing in Multics", Communication of the ACM, v17 n7, July 1974, pp 388-402.
• Lipner, S., "A Comment on the Confinement Problem", Operating System Review, v9 n5, November 1975.

Example Systems - Architectures

• Schroeder, M. D., Saltzer, J. E., "A Hardware Architecture for Implementing Protection Rings", Communications of the ACM, v15 n3, March 1972, pp. 157-170.
• Levin, R., et al., "Policy/Mechanism Separation in Hydra," Fifth Symposium on Operating Systems Principles, November 1975.
• Needham, R., and Walker, R., "The Cambridge CAP Computer and Its Protection System", Proceedings of the ACM SIGOPS Sixth Symposium on Operating System Principles, November 1977, pp 1-10.
• Davida, G., "A System Architecture to Support a Verifiably Secure Multilevel Security System", Proceedings 1980 IEEE Symposium of Security and Privacy, pp 137-144.
• Schell, R.R., "Evaluating Security Properties of Computer Systems", Proceedings 1983 Symposium on Security and Privacy, April 1983, pp. 89-95.
• Karger, P. A., Herbert, A. J., "An Augmented Capability Architecture to Support Lattice Security and Traceability of Access", Proceedings 1984 Symposium on Security and Privacy, April 1984, pp.2-12.
• Landwehr, C., Carroll, J.M., "Hardware Requirements for Secure Computer Systems: A Framework", Proceedings of the 1984 Symposium on Security and Privacy, Oakland, CA., April 1984, pp 34-40.
• Levy, H M., , "Capability based Computer Systems," Digital Press, 1984.
• MacEwen, G. H., et. at., "Multi-Level Security Based on Physical Distribution", Proceedings 1984 Symposium on Security and Privacy, April 1984, pp. 167-177.
• Kain R. Y., Landwehr C. E., "On Access Checking in Capability based systems", Proceedings of 1985 Symposium on Security and Privacy, 1985, pp. 95-101.
• Neely, R. B., Freeman, J. W., "Structuring Systems for Formal Verfication", Proceedings 1985 Symposium on Security and Privacy, April 1985, pp.2-13.
• Boebert W. E., Kain R. Y., Young W. D., Hansohn S. A., "Secure ADA Target: Issues, System Design and Verification", Proceedings of the 1985 Symposium on Security and Privacy, 1985, pp 176-183.
• Dobson, J. E., Randell, B., "Building Reliable Secure Computing Systems out of Unreliable Insecure Components", Proceedings 1986 IEEE Symposium on Security and Privacy, April 1986, pp. 187-193.
• Gligor, V. D., et. al., "On the Design and the Implementation of Secure Xenix Workstations", Proceedings 1986 IEEE Symposium on Security and Privacy, April 1986, pp. 102-117.
• Wiseman, S., "A Secure Capability Computer System", Proceedings IEEE Symposium on Security and Privacy, April 1986, pp. 86-94.
• Landwehr, C., et al. "A Framework for Evaluating Computer Architectures to Support Systems with Security Requirements, with Applications", NRL Report 9088, Naval Research Laboratory, Washington, DC., November 1987.
• White, S. R., Comerford. L., "ABYSS: A Trusted Architecture for Software Protection", Proceedings 1987 IEEE Symposium on Security and Privacy, April 1987, pp. 38-51.
• Colwell, R. P., et. al., "Performance Effects of Architectural Complexity in the Intel 432", ACM Transactions on Computer Systems, v6 n3, August 1988, pp. 296-339.
• Bondi, J. O., Branstad, M. A., "Architectural Support of Fine-Grained Secure Computing", Fifth Annual Computer Security Applications Conference, December 1989, pp. 121-130.
• Cummings P. T., Fullam D. A., Goldstein M. J., Gosselin M. J., Picciotto J., Woodward J. P. L., Wynn J., "Compartmented Mode Workstation: Results through prototyping", Proceedings 1987 IEEE Symposium of Security and Privacy, 1987, pp. 2-12.

Example Systems - Operating Systems

• Wulf, W. , et al, "Hydra - The Kernel of a Multiprocessor Operating System," Communications of the ACM, June 1974.
• William A. Wulf, Roy Levin, Samuel P. Harbison, "HYDRA/C.mmp: An Experimental Computer System", McGraw-Hill, New York, 1981
• Cohen, E. and Jefferson D, "Protection in the Hydra Operating System", ACM SIGOPS Fifth Symposium on Operating Systems Principles, November 1975.
• Jones, Anita K. and Wulf, W., "Towards the Design of Secure Systems", Software-Practice and Experience, v5 n4, Oct-Dec 1975, pp 321-336.

Miscellaneous

• Popek, G.J., Farber, D. "A Model for Verification of Data Security in Operating Systems", Communications of the ACM, v21, September 1978, pp737-749.
• Walker, B.J., et al. "Specification and Verification of the UCLA Unix Security Kernel", Communications of the ACM, v23, February 1980, p 118-131.
• Grampp, F and Morris, R., "UNIX Operating System Security", AT&T Bell Laboratories Technical Journal, v63, October 1984.
• Popek, G.J., "Secure Reliable Processing Systems: Final Technical Report, July 77 - March 82", CSD-840228, AD-A140 150, UCLA Computer Science Department, Los Angeles, CA, February, 1984.
• Farrow, R., "Security Issues and Strategies for Unix", UNIX World, May 86.
• Steiner, J.G., Neuman, C., Schiller, J.I. "Kerberos: An Authentication Service for Open Network Systems". Usenix Conference Proceedings, Winter 1988.
• Grenier, F.-L., Holt, R. C., Funkenhauser, M., "Policy vs Mechanism in The Secure Tunis Operating System", IEEE, July 1989, pp. 84-93.

Formal Models

• Redell, D and Fabry, R., "Selective Revocation of Capabilities", Proceedings of the INRIA International Workshop on Operating Systems, 1974.
• Harrison, M., et al, "Protection in Operating Systems", Communications of the ACM, v19 n8, August 1976., pp. 461-471
• Lipton, R and Snyder, L., "A Linear Time Algorithm for Deciding Subject Security", Journal of the ACM, v24 n3, July 1977, pp 455-464.
• Jones, Anita K., "Protection Mechanism Models: Their Usefulness", Foundations of Secure Computation, Academic Press, 1978 pp 237-252.
• Landwehr, C., "Formal Models for Computer Security", Computing Surveys, v13 n3, September 1981, pp 247-278.
• Snyder, L., "Formal Models of Capability-Based Protection Systems", IEEE Transactions on Computers, vC-30 n3, March 1981, pp 172-181.
• Bishop M., "Practical take-grant systems: Do they exist ?", Ph.D Dissertation, Purdue University, May 1984.
• Downs, D. D., et. al., "Issues in Discretionary Access Control", Proceedings 1985 Symposium on Security and Privacy, April 1985, pp. 208-218.
• Harrison, M., "Theoretical Issues Concerning Protection in Operating Systems", Advances in Computers, v24, 1985, pp 61-100.
• Glasgow, J.I., MacEwen, G.H., "The Development and Proof of a Formal Specification for a Multilevel Secure System", ACM Transactions on Computer Systems, v5 n2, May 1987, pp 151-184.
• McLean, J., "Reasoning about Security Models" , Proceedings 1987 IEEE Symposium of Security and Privacy, 1987, pp. 123-133.
• McCullough D., "Specifications for Multi-level Security and Hook-Up Property", Proceedings 1987 IEEE Symposium of Security and Privacy, 1987, pp. 161-166.
• Lamport L., "The Existence of Refinement Mappings", Digital Technical Report 29, 1988.
• McLean, J., "The Algebra of Security" , Proceedings 1988 IEEE Symposium of Security and Privacy.
• Sandhu R. S., "The Schematic Protection Model: Its definition and Analysis for Acyclic Attenuating Schemes", JACM, April 1988
• Vinter, S. T., "Extended Discretionary Access Controls", IEEE, May 1988, May 1988, pp. 39-49.
• Benson, G., Appelbe, Akyildiz, I., "The Hierarchical Model of Distributed System Security", IEEE, July 1989, pp. 194-203.
• Bishop, Matt, "A Model of Security Monitoring", Fifth Annual Computer Security Applications Conference, December 1989, pp. 46-52.
• Millen J. K., "Models of Multi-level Security", Advances in Computers, Vol 29, 1989.
• Benson G. S., Akyildiz I. F., Appelbe W. F., "A Formal Protection Model of Security in Centralized, Parallel and Distributed Systems", ACM transactions on Computer Systems, August 1990, pp. 183-213.
• Lamport L., "Composing Specifications", Digital Technical Report 66, 1990.
• Abadi, Martin, Plotkin G. D.,"A Logical View of Composition", Digital Technical Report 86, 1992.

Information Flow Models

• Denning, D., "A Lattice Model of Secure Information Flow", Communications of the ACM, v19 n5, May 1976, pp 236-243.
• Denning, D. and Denning, P., "Certification of Programs for Secure Information Flow", Communications of the ACM, v20 n7, July 1977, pp 504-513.
• Goguen, J. A., Meseguer, J. "Security Policies and Security Models", Proceedings 1982 IEEE Symposium of Security and Privacy, April 1982, pp. 11-20.
• Goguen, J. A., Meseguer, J. "Unwinding and Inference Control", Proceedings 1984 IEEE Symposium of Security and Privacy, April 1984.
• Sutherland D., "A Model of Information", 9th National Security Conference, 1986.
• Johnson, D.M., Thayer, F.J., "Stating Security Requirements with Tolerable Sets", ACM Transactions on Computer Systems, v6 n3, August 1988, pp 284-293.
• McCullough, D., "Noninterference and the Composability of Security Properties", IEEE, May 1988, pp. 177-186.
• Sandhu, R., "Transformation of Access Rights", IEEE, July 1989, pp. 259-268.
• Foley, S. N., "A Model for Secure Information Flow", IEEE, July 89, pp. 248-258.
• Moser L. E., "A Logic of Knowledge and Belief for Reasoning about Computer Security", Proceedings The computer Security Foundations Workshop III, June 1990, pp. 57-63.
• Foley S. N., "Secure Information Flow Using Security Groups", Proceedings The computer Security Foundations Workshop III, June 1990, pp. 62-73.
• Fine T., "Constructively Using Nonintereference to Analyze Systems", Proccedings 1990 IEEE Conference on Security and Privacy, 1990, pp.162-169.
• McLean J., "Security Models and Information Flow", Proceedings 1990 IEEE Conference on Security and Privacy, 1990, pp. 170-189.
• Varadharajan V., "Petri Net Based Modelling of Information Flow Security Requirements", Proceedings The computer Security Foundations Workshop III, June 1990, pp. 51-61.
• Wittbold J. T., Johmson D. M., "Information Flow in Non-Deterministic Systems", Proceedings 1990 IEEE Conference on Security and Privacy, 1990, pp. 144-161.
• Bishop, M., "Theft of Information in Take-Grant Protection Model", Dartmouth technical report 1991.
• Cumming, J. G., "On Refinement of Non-Interference", Proceedings 1991 IEEE Symposium of Security and Privacy, 1991.
• Gray J. W., "On Information Flow Security Models", Proceedings 1991 IEEE Symposium of Security and Privacy, 1991.
• Shi Qi, "A Formal Approach to Security Evaluation", IEEE Conference on Secure Computing, 1992.

Verification

• Jones, Anita K., "Protection in Programmed Systems", PhD. Dissertation, CMU Department of Computer Science, 1973.
• Millen, J.K., "Security Kernel Validation in Practice", Communications of the ACM, v19, May 1976, pp 243-250.
• Feiertag, R.J., Levitt, K.N., Robinson, L., "Proving Multilevel Security of a System Design", Proceedings of Sixth ACM Symposium of Operating Systems Principles, November 1977.
• Cheheyl, M., et. al., "Verifying Security", Computer Surveys, v13 n3, September 1981, pp 279-339.
• Gligor, V.D., "The Verification of the Protection Mechanisms of High-Level Language Machines", International Journal of Computer and Information Sciences, V12, No. 4, June 1983, pp 211-247.
• Benzel, A., et. al., "Analysis of Kernel Verification", Proceeding of 1984 IEEE Symposium of Security and Privacy, pp 125-131.
• Britton, D. E., "Formal Verification of a Secure Network with End-to-End Encryption", Proceedings 1984 Symposium on Security and Privacy, April 1984, pp.154-166.
• Benzel, T. C. V., Ravilla, D. A., "Trusted Software Verification: A Case Study", Proceedings 1985 Symposium on Securitgy and Privacy, April 85, pp. 14-31.
• Gligor, V. D., "Analysis of the Hardware Verification of the Honeywell Scomp", Proceedings 1985 Symposium on Security and Privacy, April 1985, pp.32-43.
• Wing, J. M., Nixon, M. R., "Extending INA JO with Temporal Logic", Proceedings 1986 IEEE Symposium on Security and Privacy, April 1986, pp. 2-13.
• Halpern J. D., Owre S., Proctor N., Wilson W. F., "Muse-A Computer Assisted Verification System", Proceedings 1986 Symposium on Security and Privacy, April 1986, pp. 25-33.
• Bevier, W. R., et. al., "Toward Verified Execution Environments", Proceedings 1987 Symposium on Security and Privacy, Aprifl 1987, pp. 106-115.
• McCullough, Daryl, "Specifications for Multi-Level Security and a Hook-up Property", Proceedings 1987 Symposium on Security and Privacy, April 1987, pp. 161-166.
• McLean, John, "Reasoning About Security Models", Proceedings 1987 Symposium on Security and Privacy, April 1987, pp. 123-131.
• Williams, J. C., Dinolt, G. W., "A Graph-Theoretic Formulation of Multilevel Secure Distributed Systems: An Overview", Proceedings 1987 IEEE Symposium on Security and Privacy, April 1987, pp. 97-103.
• Bell, D.E., "Concerning 'Modeling' of Computer Security", IEEE, May 1988, pp. 8-13.
• Denning, D. R., Lunt, T. F., "The SeaView Security Model", IEEE, May 1988, pp. 218-233.
• Glasgow, J. I., MacEwen, G. H., "Reasoning About Knowledge in Multilevel Secure Distributed Systems", IEEE, May 1988, pp. 122-128.
• Good D. I., et. al., "Using the Gypsy Methodology", Computational Logic Inc Technical report, Jan 1988.
• Jacob, J., "Security Specifications", IEEE, May 1988, pp. 14-23.
• Dobson, J.E., McDermid, J. A., "A Framework forf Expressing Models of Security Policy", IEEE, July 1989, pp. 229-239.
• Jacob, J., "On The Derivation of Secure Components", IEEE, July 1989, pp. 242-247.
• Neely R. B., Freeman J. W., Krenzin M. D., "Achieving Understandable Results in Formal Design Verification", Proceedings The computer Security Foundations Workshop II, June 1989, pp. 115-124.
• Rosenthal, D., "Implementing a Verfication Methodology for McCullough Security", Proceedings of The Computer Security Foundations Workshop II, June 1989, pp. 133-140.
• Whitehurst, R. A., Lunt, T. F., "The SeaView Verification", Proceedings of The Computer Secuirty Foundations Workshop II, June 1989, pp. 125-132.
• Brix H., Dietl A., "Formal Construction of Provably Secure Systems with Cartesiana", Proceedings of the 1990 Symposium on Security and Privacy, 1990, pp. 319-332.
• Glasgow, J., MacEwen, G., "A Logic for Reasoning About Security", Proceedings of The Computer Security Foundations Workshop III, June 1990, pp. 2-13.
• Gong, Li, et. al., "Reasoning about Belief in Cryptographic Protocols", Proceedings 1990 IEEE Symposium of Security and Privacy, May 1990, pp. 234-248.
• Millen, J. K., "Hookup Security for Synchronous Machines", Proceedings of the Computer Security Foundations Workshop III, June 1990, pp. 84-90.
• Rosenthal, D., "Security Models for Priority Buffering and Interrupt Handling", Proceedings The Computer Security Foundations Workshop III, June 1990, pp. 91-97.
• Windley P. J., "A Hierarchical Methododlogy for Verifying Microprogrammed Microprocessors", Proceedings of the 1990 Symposium on Security and Privacy, 1990, pp. 345-359.
• Rushby J., Henke F. O., Owre S., "An Introduction to Formal Specification and Verification using Ehdm", SRI-CSL-91-02,Feb 1991

Examples of Verification

• Neumann P. G., Boyer R. S., Feiertag R J, Levitt K. N., Robinson L.,"A Provably Secure Operating System: The system its Applications and Proofs", SRI-CSL-80-116, May1980.
• Whitehurst R. A., Lunt T. F., "The SeaView Verification", Proceedings The Computer Security Foundations Workshop II, June 1989, pp. 125-132.
• Vito B. L. D., Palmquist P. H., Anderson E. R., Johnston M. L., "Specification and Verification of the ASOS Kernel", Proceedings of the 1990 Symposium on Security and Privacy, 1990, pp. 61-74.
• Guttman J. D., Ko H. P., "Verifying a Hardware Security Architecture", Proceedings of the 1990 Symposium on Security and Privacy, 1990, pp. 333-344.

Security Policy

• Bell, D. and Lapadula, L., "Secure Computer Systems: Mathematical Foundations and a Model", Mitre Report MTR 2547, v2 November 1973.
• Biba, K., "Integrity Considerations for Secure Computer Systems", US Air Force Electronic Systems Division, 1977.
• Jones, Anita K. and Lipton, R., "The Enforcement of Security Policies for Computation", Journal of Computer and Systems Science, v17 n1, August 1978, pp 35-55.
• Lipner, S. B., "Non-Discretionary Controls for Commercial Applications", Proceedings of 1982 Symposium on Security and Privacy, 1982, pp. 2-10.
• Gligor V. D., "A Note on denial of Service Problem", Proceedings of 1983 Symposium on Security and Privacy, 1983, pp. 139-149.
• McLean, J., et. al, "A Formal Statement of the MMS Security Model", Proceedings 1984 Symposium on Security and Privacy, April 1984, pp. 188-194.
• Haigh J., Young W., "Extending the Non-Interference Version of MLS for SAT", Proccedings of the 1985 Symposium on Security and Privacy, 1985, pp. 232-239.
• Clark, D. D., Wilson, D. R., "A Comparison of Commercial and Military Computer Security Policies", Proceedings 1987 IEEE Symposium on Security and Privacy, April 1987, pp. 184-194.
• Karger, P. A., "Implementing Commercial Data Integrity with Secure Capabilities", IEEE, May 1988, pp. 130-139.
• Lee, T. M. P., "Using Mandatory Integrity to Enforce 'Commercial' Security", IEEE, May 1988, pp. 140-155.
• Badger, L., "A Model for Specifying Multi-Granularity Integrity Policies", IEEE, July 1989, pp 269-277.
• Brewer, D. F. C., Nash, M. J., "The Chinese Wall Security Policy", IEEE, July 1989, pp. 206-214.
• Landauer, J., et. al., "Formal Policies for Trusted Processes", Proceedings of The Computer Security Foundations Workshop II, June 1989, pp. 31-40.
• Terry, P., Wiseman, S., "A 'New' Security Policy Model", IEEE, July 1989, pp. 215-228.
• Amoroso, E., "A Policy Model for Denial of Service", Proceedings of the Computer Security Foundations Workshop III, June 1990, pp. 110-114.
• La Padula, L. J., "Formal Modeling in a Generalized Framework for Access Control", Proceedings The Computer Security Foundations Workshop III, 1990.

Other & Misc.

• Schaefer, M., Chair, Panel Session, Kernel Performance Issues, Proceedings 1981 IEEE Symposium on Security and Privacy, April 1981, pp. 162-178.
• Leiss, E.L., "Principles of Data Security", Plenum Press, New York and London, 1982.
• Landwehr, C., "The Best Available Technologies for Computer Security", IEEE Computer Magazine, July 1983, pp 86-100.
• Summers, R.C., "An Overview of Computer Security", IBM Systems Journal, v23 n4, 1984, pp 309-325.
• Downs, D. D., et. al., Issues in Discretionary Access Control, Proceedings 1985 Symposium on Security and Privacy, April 1985, pp. 208-218.
• Gligor, V. D., et. al., "A New Security Testing Method and its Application to the Secure Xenix Kernel", Proceedings 1986 IEEE Symposium on Security and Privacy, April 1986, pp. 40-58.
• Haigh, J. T., et. al., "An Experience Using Two Covert Channel Analysis Techniques ON a Real System Design", Proceedings 1986 IEEE Symposium on Security and Privacy, April 1986, pp. 14-24.
• Millen, J. K., "Covert Channel Capacity", Proceedings 1987 Symposium on Security and Privacy, Aprifl 1987, pp. 60-73.
• Millen, J.K., et al. "The Interrogator: Protocol Security Analysis", IEEE Transactions on Software Engineering, SE-13-2, February 1987.
• Millen, J. K., "Finite-State Noiseless Covert Channels", Proceedings of The Computer Security Foundations Workshop II, June 1989, pp. 81-86.
• Pfleeger, C., "Security in Computing", Prentice Hall, 1989.
• Walker, S. T., "Information Security: How Far We have Come! How Far Can We Go?", Fifth Annual Computer Security Applications Conference, December 1989, pp. vii-x.
• He, J., Giligor, V. D., "Information-Flow Analysis for Covert-Channel Identification in Multilevel Secure Operating Systems", June 1990, pp. 139-148.
• McCollum, C. J., et. al., "Beyond the Pale of MAC and DAC-Defining New Forms of Access Control", Proceedings 1990 IEEE Symposium on Security and Privacy, May 1990, pp. 190-200.

Authentication

• Otway, D., Rees, O. "Efficient and Timely Mutual Authentication" Operating Systems Review, v21 n1, January 1987, pp 8-10.

Audits and Footprints

• Denning, D. E., "An Intrusion-Detection Model", Proceedings 1986 IEEE Symposium on Security and Privacy, April 1986, pp. 118-131.
• Lunt, T. F., Jagannathan, R., "A Prototype Real-Time Intrusion-Detection Expert System", IEEE, May 1988, pp. 59-6
• Rabin, M., "An Integrated Toolkit for Operating System Security", Harvard Univ TR-05-87, August 1988 (revised).
• Seiden, K.F., Melanson, J.P., "The Auditing Facility for a VMM Security Kernel", Proceedings 1990 IEEE Symposium of Security of Privacy, pp. 262-277.
• Vaccaro, H. S., Liepins, G. E., "Detection of Anomalous Computer Session Activity", IEEE, July 1989, pp. 280-289.
• Wagner, N. R., "Fingerprinting", Proceedings 1983 IEEE Symposium on Security and Privacy, April 1983, pp. 18-22.

Network and Distributed System Security

• Anderson, D. P., Ferrari, D., Rangan, P.V., Sartirana,B. "A Protocol for Secure Communications in Large Distributed Systems" AD-A179 326, Computer Science Division, University of California, Berkeley, CA, January 1987.
• Anderson, D. P., Rangan, P. V., "A Basis for Secure Communication in Large Distributed Systems", Proceedings 1987 IEEE Symposium on Security and Privacy, April 1987, pp. 167-172.
• Anderson, J. P., "A Unification of Computer and Network Security Concepts", Proceedings 1985 Symposium on Security and Privacy, April 1985, pp. 77-87.
• Birrell, A. D., et. al., "A Global Authentication Service without Global Trust", Proceedings 1986 IEEE Symposium on Security and Privacy, April 1986, pp. 223-230.
• Birrell, A.D., "Secure Communication Using Remote Procedure Call", ACM Transactions on Computer Systems, February 1985, pp 1-14.
• Bussolati, U., Martella, G., "Security Design in Distributed Database Systems", The Journal of Systems and Software, 1983, pp 219-229.
• Casey, T. A., et. al., "A Secure Distributed Operating System", IEEE, May 1988, pp. 27-38.
• Estrin, D., Tsudik, G., "Visa Scheme for Inter-Organization Network Security", Proceedings 1987 IEEE Symposium on Security and Privacy, April 1987, pp. 174-183.
• Halpern, J.Y., Moses, Y.O. Tuttle, M.R. "Knowledge and Common Knowledge in a Distributed Environment". Proceedings of the 3rd ACM Conference on the Principles of Distributed Computing, August 1984, pp 480-490.
• Kak, S.C., "Data Security in Computer Networks", IEEE Computer Magazine, February 1983, pp 8-10.
• Landwehr, C., et al, "A Security Model for Military Message Systems", ACM Transactions on Computer Systems, v2 n3, August 1984, pp 198-222.
• Merkle, R. C., "Secure Communications over Insecure Channels" in CACM, Vol. 21, No. 4 (April 1978), pp. 294-300.
• Millen, J.K., "Network Security Verification", M85-32, Mitre Corp., September 1985.
• Nessett, D. M., "Factors Affecting Distributed System Security", IEEE Transactions On Software Engineering, Vol. SE-13, No 2, Feb 1987, pp. 204-222
• Proctor, N., Wong, R., "The Security Policy of the Secure Distributed Operating System Prototype", December 1989, pp. 95-102.
• Rushby J.M., Randell, B., "A Distributed Secure System", Proceedings 1983 Symposium on Security and Privacy, April 1983, pp. 127-135.
• Satyanarayanan, M. "Integrating Security in a Large Distributed System", ACM Transactions on Computer Systems, v7 n3, August 1989, pp 247-280.
• Stephen T. Walker, "Network Security: The Parts of the Sum,"1989, (IEEE) ...
• Voydock, V.L., Kent, S.T., "Security Mechanisms in a Transport Protocol", Computer Networks, 1984, pp 433-449.
• Walker, S. T., "Network Security Overview", Proceedings 1985 Symposium on Security and Privacy, April 1985, pp. 62-76.

Cryptographic Protocols

• Needham, R.M., and Schroeder, M.D., "Authentication Revisited", in Operating Systems Review, Vol. 21, No. 1 (January 1987), p. 7.
• Needham, Roger M., and Schroeder, Michael D., "Using Encryption for Authentication in Large Networks of Computers", in CACM, Vol. 21, No. 12 (December 1978), pp. 993-999.
• Denning, Dorothy E, "Cryptography and Data Security", Addison-Wesley, 1982.
• Rivest, R.L., Shamir, A., and Adelman, L., "A Method for Obtaining Digital Signatures and Public-Key Cryptosystems", in CACM, Vol. 21, No. 2 (February 1978), pp. 120-126.
• Denning, Dorothy E, "The Many-Time Pad: Theme and Variations", Proceedings 1983 IEEE Symposium of Security and Privacy, pp. 23-30.
• Denning, Dorothy E., and Sacco, Giovanni Maria, "Timestamps in Key Distribution Protocols" in CACM, Vol. 24, No. 8 (August 1981), pp. 533-536.
• Bauer, R.K., Berson, T.A., and Feiertag, R. J. "A key distribution protocol using event markers", ACM Transactions on Computing Systems, Vol. 1, No. 3 (Aug. 1983), 249-255
• Bellovin, Steven M. & Michael Merritt, "Limitations of the Kerberos Authentication System", Computer Communications Review, Oct 1990
• Davida, G.,Chair, Panel Session, Cryptography, Proceedings 1981 Symposium on Security and Privacy, April 1981, pp. 151-161.
• Diffie, W., Hellman, M.E. "Privacy and Authentication: an Introduction to Cryptography" Proceedings of the IEEE, v67 n3, March 1979, pp. 397-427.
• Lamport, L., "Password Authentication with Insecure Communications", Communications of the ACM, v24 n11, November 1981, pp. 770-772.
• Lampson, B., Abadi, Martin, Burrows, M., and Wobber, E., "Authentication in Distributed Systems: Theory and Practice", in ASM OS Review, Vol. 25, No. 5, pp. 165-182.
• M. Beller, L. Chang, and Y. Yacobi, "Privacy and Authentication on a Portable Communications System", IEEE Global Telecommunications Conference, Dec 1991
• Miller, S. P., Neuman, C., Schiller, J.I., and Saltzer, J.H., Kerberos Authentication and Authorization System. In Project Athena Technical Plan, Section E.2.1, MIT, Cambridge, Mass., July 1987
• Nessett, D. M., "Layering Central Authentication on Existing Distributed System Terminal Services", From 1989 IEEE Computer Society Symposium on Security and Privacy, pp. 290-299.
• Otway, Dave, and Rees, Owen, "Efficient and Timely Mutual Authentication", in Operating Systems Review, Vol. 21, No. 1 (January 1987), pp. 8-10.
• Voydoc, Victor L., and Kent, Stephen T., "Security Mechanisms in High-Level Network Protocols" in Computing Surveys, Vol. 15, No. 2 (June 1983), pp. 135-171.

Cryptographic Protocol Verification

• Abadi, Martin and Mark R. Tuttle, "A Semantics for a Logic of Authentication", Tenth Annual ACM Symp on Princ of Dist Computing, Montreal, Canada, August, 1991
• Burrows, M., Abadi, Martin, and Needham, R. M. "A Logic of Authentication", Technical Report 39, Digital Systems Research Center, 130 Lytton Avenue, Palo Alto, Cal, 94301, February 1989
• Burrows, M., Abadi, Martin, and Needham, R. M. "A Logic of Authentication", ACM Transactions on Computer Systems, Vol. 8, No. 1, Feb 1990, pp. 18-36.
• Burrows, M., Abadi, Martin, and Needham, R. M. "Authentication: A Practical Study in Belief and Action", In Proceedings of the 2nd Conference on Theoretical Aspects of Reasoning about Knowledge (Asilomar, Ca., Feb. 1988) M. Vardi, Ed. Morgan Kaufmann, Los Altos, Calif., 1988, pp. 325-342
• Burrows, M., Abadi, Martin, and Needham, R. M., "Rejoinder to Nessett", ACM Operating Systems Review, vol. 24, no. 2, April 1990, pp. 39-40
• Burrows, Michael, Abadi, Martin, and Needham, Roger, "A Logic of Authentication" in Proceedings of the Royal Society of London A, Vol. 426, 1989, pp. 233-271.
• Cheng, Pau-Chen, and Gligor, Virgil D., "On the Formal Specification and Verification of a Multiparty Session Protocol", in Proceedings of the 1990 IEEE Symposium on Research in Security and Privacy, pp. 216-233.
• Dolev, Danny, and Yao, Andrew C., "On the Security of Public Key Protocols", in IEEE Transactions on Information Theory, Vol. IT-29, No. 2 (March 1983), pp. 198-208.
• U. Feige, A. Fiat, and A. Shamir, "Zero-knowledge Proofs of Identity", Journal of Cryptology, 1(2):77-94, 1988.
• Glasgow, Janice I., and Glenn H. MacEwen, "Reasoning About Knowledge in Multilevel secure Distributed Systems", in Proceedings of the 1988 IEEE Symposium on Security and Privacy, Washington (IEEE), 1988, pp. 122-128
• Gong, L., Needham, R., and Yahalom, R. "Reasoning about Belief in Cryptographic protocols". From 1990 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 234-248
• Halpern, J.Y., and Moses, Y.O. "A Knowledge-based analysis of zero knowledge" (preliminary report). In Proceedings of the 20th ACM symposium on Theory of Computing (Chicago, Ill, May 1988), ACM, New York, 1988, pp. 132-147
• Kemmerer, R. A., "Using Formal Methods to Analyze Encryption Protocols," IEEE Journal on Selected Areas in Communications, vol. 7, mo. 4, pp. 448-457, May 1989
• Meadows, C., "Using Narrowing in the Analysis of Key Management Protocols". From 1989 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 138-147.
• Meadows, Catherine, "A System for the Specification and Analysis of Key Management Protocols", in Proceedings of the 1991 IEEE Symposium on Research in Security and Privacy, pp. 182-195.
• Millen, Jonathan K., Clark, Sidney C., and Freedman, Sheryl B., "The Interrogator: Protocol Security Analysis", in IEEE Transactions on Software Engineering, Vol. SE-13, No. 2 (February 1987), pp. 274-288.
• Moser, L., "A Logic of Knowledge and Belief for Reasoning about Computer Security" in Proceedings of the Computer Security Foundations Workshop II, Washington (IEEE), 1989, pp. 57-63
• Nessett, D., "A Critique of the Burrows, Abadi, and Needham Logic", ACM Operating Systems Review, vol. 24, no. 2, April 1990, pp. 35-38
• Rangan, P. Venkat, "An Axiomatic Basis for Trust in Distributed Systems", in Proceedings of the 1988 IEEE Symposium on Security and Privacy, pp. 204-211, IEEE Computer Society Press, Washington, DC, 1988
• Snekkenes, E., "Exploring the BAN Approach to Protocol Analysis". From 1991 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 171-181.
• Syverson, Paul, "The Use of Logic in the Analysis of Cryptographic Protocols", in Proceedings of the 1991 IEEE Symposium on Research in Security and Privacy, pp. 156-170.

Database Security

Alec & Brett's Combined Reference Lists

• Abadi, Martin, and Needham, Roger, "Prudent Engineering Practice for Cryptographic Protocols", in Proceedings of the 1994 IEEE Symposium on Research in Security and Privacy, pp. 122-136.
• Bellovin, Steven M., and Merritt, Michael, "Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionary Attacks", in Proceedings of the 1992 IEEE Symposium on Research in Security and Privacy, pp. 72-84.
• Bird, Ray, Inder Gopal, Amir Herzberg, Phil Janson, Shay Kutten, Refik Molva, and Moti Yung. "Systematic Design of Two-Party Authentication Protocols." In Joan Fegenbaum, editor, Advances in Cryptography - CRYPTO '91, volume 576 of Lecture Notes in Computer Science. Springer Verlag, Berlin, 1992
• Bird, Ray, Inder Gopal, Amir Herzberg, Phil Janson, Shay Kutten, Refik Molva, and Moti Yung. "Systematic Design of a Family of Attack Resistant Authentication Protocols", IEEE Journal on Selected Areas in Communications, Vol 11, No. 5, June 1993
• Bieber, P., "A Logic of Communication in a Hostile Environment", in Proceedings of the ComputereSecurity Foundations Workshop III, Washington (IEEE), 1990, pp.14-22
• Boyer, Robert S., and J. Strother Moore, "A Computational Logic", Academic Press 1979, From the ACM Monographic Series
• Boyer, Robert S., and J. Strother Moore, "A Computational Logic Handbook", Academic Press 1988, From the series "Perspectives in Computing", v23
• Carlsen, Ulf, "Generating Formal Cryptographic Protocol Specifications", From the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pp 137-145
• CCITT draft recommendation X.509. The directory-authentication framework, version 7. CCITT, Gloucester, Nov. 1987
• CCITT, CCITT Blue Book, "Recommendation X.509 and ISO 9594-8, Information Processing Systems - Open Systems Interconnection - The Directory - Authentication Framework", Technical Report, Geneva, March, 1988.
• Clockson, W. F., and Mellish, C. S., "Programming in Prolog", Springer-Verlag 1981
• Crow, Judy, Sam Owre, John Rushby, Natarajan Shankar, Mandayam Srivas, "A Tutorial Introduction to PVS", Computer Science Laboratory, SRI International, Menlo Park, Ca 94025
• National Bureau of Standards (NBS). Data Encryption Standard. Dederal Information Processing Standard, Publication 46, NBS, Washington, D.C., January 1977
• Diffie, W., M. Hellman, New Directions in Cryptography, IEEE Transactions on Information Theory, Vol. it-22, no 6, Nov 1976, pp. 644-654
• Diffie, W., "The First Ten Years of Public Key Cryptography", Proceedings of The IEEE, Vol 76, No. 5, May 1988, pp 560-577
• Dijkstra, Edsger W., "A Discipline of Programming", Prentice Hall Series in Automatic Computation, Prentice-Hall Inc. Englewood Cliffs, NJ, 1976
• ElGamal, T., "A Public Key Cryptosystem and a Signature Scheme Based on Discrete Logarithms", IEEE Transactions on Information Theory, IT-31 (4):469-472
• Goldreich, O., S. Micali, and A. Wigderson, "Proofs That Yield Nothing but Their Validity and a Methodology of Cryptographic Protocol Design", Proceedings of the 27th IEEE Symposium on foundations of Computer Science, 1986, pp. 174-187
• Goldwasser, Shafi, Silvio Micali, and Charles Rackoff, "The Knowledge Complexity of Interactive Proof Systems," Proc. 27th Annual IEEE Symposium on Foundations of Computer Science, 1985, pp. 291-304
• Goldwasser, Shafi, Micali, Silvio, and Rackoff, Charles, "The Knowledge Complexity of Interactive Proof Systems," Siam Jrnl of Comp, Vol 18, No 1, Feb 1989, pp. 186-208.
• Gong, Li, "Increasing Availability and Security of an authentication Service" in IEEE Journal on Selected Areas in Communications, Vol. 11, No. 5, June, 1993, pp. 657-662.
• Good, D I., et. al. Report on the language Gypsy - version 2.0, Univ. of Texas at Austin, Certifiable Minicomputer Project, Report ICSCA-CMP-10, 1978
• Gordon, J., speech at the Zurich Seminar, 1984. In this lecture, which has unfortunately never been published (but was reported by Whitfield Diffie), Gordon assembled the facts of Alice and Bob's precarious lives, which had previously been available only as scattered references in the literature.
• Gaarder, Klaus, and Einar Snekkenes, "Applying a Formal Analysis Technique to the CCITT X.509 Strong Two-Way Authentication Protocol", Journal Of Cryptology, 3:81-98, 1991.
• Gumb, Raymond D., "On the Underlying Logics of Specification Languages", ACM Sigsoft, Software Engineering Notes, Vol 7, No 4, Oct 82, pp 21-23
• Heintze, Nevin, and Tygar, J.D., "A Model for Secure Protocols and Their Compositions", in Proceedings of the 1994 IEEE Symposium on Research in Security and Privacy, pp. 2-13.
• Hoare, C. A. R., "An Axiomatic Basis for Computer Programming", Communications of the ACM, Vol 12, Number 10, Oct 1969
• Hoare, C. A. R., and N. Wirth: "An Axiomatic Definition of the Programming Language Pascal," Acta Informatica, 2, 1973
• Hoare, C. A. R., "Communicating Sequential Processes", Communications of the ACM, Vol 21, Number 8, Aug 1978, pp 666-677
• Hoare, C. A. R., "Communicating Sequential Processes", Prentice Hall, 1985
• I'Anson, C., and Mitchell, C., "Security Defects in CCITT recommendation X.509 - the directory authentication framework" in ACM Computer Communication Review, Vol. 20, No. 2 (April 1990), pp. 30-34.
• Kahn, D., "The Codebreakers, The Story of Secret Writing", New York: MacMillan, 1967
• Kailar, Rajashekar and Virgil D. Gligor. "On Belief Evolution n Authentication Protocols", In Proceedings og the Computer Security Foundations Workshop IV, pp. 103-116, IEEE Computer Society Press, Los Alamitos, Ca. 1991
• Kehne, A., Schonwalder, J., and Langendorfer, H., "A nonce-based protocol for multiple authentication" in ACM Operating Systems Review, Vol. 26, No. 4 (October 1992), pp. 84-89.
• Kemmerer, Richard A., "Analyzing Encryption Protocols Using Formal Verification Techniques", in IEEE Journal on Selected Areas in Communication, Vol. 7, No. 4 (May 1989), pp. 448-457.
• Kemmerer, R., Meadows, C., and Millen, J., "Three Systems for Cryptographic Protocol Analysis", The Journal of Cryptology, 1993.
• Kemmerer, R., C. Meadows, and J. Millen, "Three Systems for Cryptographic Protocol Analysis", To appear in The Journal of Cryptography
• Lomas, Mark, Li Gong, Jerome H. Saltzer, Roger Needham, "Reducing Risks from Poorly Chosen Keys", Operating Systems Review, 12th ACM Symposium on Operating Sstems Principles, Vol 23, Number 5, 3-6 Dec 1989, p 14-18
• Mao, Wenbo and Colin Boyd, "Towards a Formal Analysis of Security Protocols", In Proceedings of the Computer Security Foundations Workshop VI, pp 147-158, IEEE Computer Society Press, Los Alamitos, California, 1993
• Meadows, C., "Applying Formal Methods to the Analysis of Key Management Protocols", Journal of Computer Security, Vol. 1, No. 1, 1992
• Moore, Judy H., "Protocol Failures in Cryptosystems", Proceedings of the IEEE, Vol. 76, No. 5, May 1988
• Neuman, B. Clifford and StuartG. Stubblebine. A Note on the Use of Timestamps as Nonces. Operating Systems Review, 27(2):10-14, April 1993
• Owre, S., N. Shankar, and J. M. Rushby. "The PVS Specification Language (Draft). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993
• Owre, S., N. Shankar, and J. M. Rushby. "User Guide for the PVS Specification and Verification System (Draft). Computer Science Laboratory, SRI International, Menlo Park, CA, March 1, 1993
• Owre, S., N. Shankar, and J. M. Rushby. "PVS Tutorial. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993
• Owre, S., N. Shankar, and J. M. Rushby. "The PVS Proof Checker: A Reference Manual". Computer Science Laboratory, SRI International, Menlo Park, CA, March 1, 1993
• Piessens, F., De Decker, B., Janson, P., "Interconnecting Domains with Heterogeneous Key Distribution and Authentication Protocols", in Proceedings of the 1993 IEEE Symposium on Research in Security and Privacy, pp. 66-79.
• Simmons, G.J., "How to (Selectively) Broadcast a Secret," in Proceedings of the 1985 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1985, pp. 108-113
• Snekkenes, Einar, "Roles in Cryptographic Protocols", in Proceedings of the 1992 IEEE Symposium on Research in Security and Privacy, pp. 105-119.
• Stubblebine, Stuart G., and Gilgor, Virgil D., "On Message Integrity in Cryptographic Protocols", in Proceedings of the 1992 IEEE Symposium on Research in Security and Privacy, pp. 85-104.
• Stubblebine, Stuart G., and Gilgor, Virgil D., "Protocol Design for Integrity Protection", in Proceedings of the 1993 IEEE Symposium on Research in Security and Privacy, pp. 41-53.
• Syverson, P., "A Logic for Cryptographic Protocol Analysis", NRL Formal Report 9305, December 1990
• Syverson, P., "Knowledge, Belief, and Semantics in the Analysis of Cryptographic Protocols", Journal of Computer Security 1 (1992), pp. 317-334
• Syverson, P., "Adding Time to a Logic of Authentication", in Proceedings of the First ACM Conference on Computer and Communications Security (Fairfax VA, Nov 3-5).
• Syverson, P., "On Key Distribution Protocols for Repeated Authentication" ACM Operating Systems Review vol. 27, no. 4 (October 1993), pp. 24-30.
• Syverson, Paul, and Meadows, Catherine, "A Logical Language for Specifying Cryptographic Protocol Requirements", in Proceedings of the 1993 IEEE Symposium on Research in Security and Privacy, pp. 165-177.
• Syverson, Paul F., and van Oorschot, Paul C., "On Unifying Some Cryptographic Protocol Logics", in Proceedings of the 1994 IEEE Symposium on Research in Security and Privacy, pp. 14-28.
• Tatebayashi, M., Mattsukaki, N., and Newman, D. B., "Key Distribution Protocol for Digital Mobile Communication Systems", in Advances in Cryptography - CRYPTO '89, pp. 324-333.
• van Oorschot, Paul C., "Extending Cryptographic Logics of Belief to Key Agreement Protocols (Extended Abstract), In Proceedings of the First ACM Conference on Computer and Communications Security, pp 232-243, Nov 1993
• Woo, T. Y. C., and Lam, S. S., "Authentication for Distributed Systems" in IEEE Computer, Vol. 25, No. 1 (January 1992), pp. 39-52.
• Wulf, Wm. A., Mary Shaw, Paul N. Hilfinger, and Lawrence Flon, "Fundamental Structures of Computer Science" Addison-Wesley, 1981
• Wulf, Wm. A., Alec Yasinsac, Katie S. Oliver, and Ramesh Peri, "Remote Authentication Without Prior Shared Knowledge", Proceedings of the Internet Society Symposium on Network and Distributed System Security, Feb 2-4, 1994, San Diego, Ca., pp. 159-164