- B.A. Mathematics, Harvard, 1963
- M.S. Mathematics, Stanford, 1965
- Ph.D. Mathematics, Rensselaer Polytechnic Institute, 1969
On the Capacity and Homology of a Discrete
Metric. Partial results for a problem due to Shannon
involving graph theory, topology, and
coding theory: the zero-error capacity of a channel whose "confusion graph"
was a pentagon. (The problem was fully solved a few years later by
- The MITRE Corporation, 1969-1997
- SRI International, Computer Science Lab, 1997-2004
- The MITRE Corporation, 2004-2012
- Founding General Chair of the IEEE Computer Security Foundations Workshop and Symposium, 1988,
and Steering Committee Chair until 2012.
- Founding Editor in Chief (with S. Jajodia) of the Journal of Computer Security,
- Program and General Chair of the IEEE Symposium on Security and Privacy at times.
- Chair of the IEEE Computer Society Technical Committee on Security and Privacy 2006-7.
- Adventures in Cryptographic Protocol Analysis, ACM CCS 2010, keynote presentation.
- Annotated Sequence Diagrams, with J. Ramsdell,
- Call by Contract for Cryptographic Protocols,
with J. Guttman, J. Ramsdell, J. Sheehy, and B. Sniffen. FCS-ARSPA, August 2006.
- Symbolic Protocol
Analysis With Products and Diffie-Hellman Exponentiation,
with V. Shmatikov. Computer Security Foundations Workshop, June
with G. Denker, for DISCEX III, April, 2003.
- On the Freedom of
Decryption, Information Processing Letters,
86(6), June 2003, pp. 329-333.
- Constraint Solving for Cryptographic Protocol Analysis,
with V. Shmatikov, ACM CCS 2001.
- Depender Graphs: A Method for Fault-Tolerant
Certificate Distribution, with P. Lincoln and R. Wright, JCS 9(4), 2001.
- Proving secrecy is easy enough, with V. Cortier and
H. Ruess, CSFW 2001.
- Applications of Term Rewriting to Cryptographic Protocol Analysis,
WRLA 2000, and ENTCS Vol. 36, 2000.
- A Necessarily Parallel Attack, FLoC Workshop on
Formal Methods and Security Protocols, 1999 (the ffgg protocol).
- 20 Years of Covert Channel Modeling and Analysis,
IEEE Security and Privacy Symposium, 1999.
- Unwinding Forward Correctibility, CSFW 1994.
- Three systems for cryptographic protocol analysis, with
R. Kemmerer and C. Meadows, Journal of Cryptology 7(2) 79-130, 1994.
- A Resource Allocation Model for Denial of Service,
IEEE Security and Privacy Symposium, 1992, and J. Computer Security 2(2), 1993.
- Finite-state noiseless covert channels, CSFW 1989.
- The Interrogator: protocol security analysis, with S. Clark and S. Freedman,
IEEE Transactions on Software Engineering SE-3(2), 274-288, February 1987.
- The Interrogator: a tool for cryptographic protocol security,
IEEE Security and Privacy Symposium, 1984.
- Security kernel validation in practice, Communications of the ACM
19(5), (May 1976), 243-250.
LISP 1.5 and its implementation on the IBM System/360 at RPI, with
Jack Gelb, RPI Computer Lab Report, January 1969.
- Constraint Solving Techniques and Enriching the Model with Equational Theories,
with H. Comon-Lundh and S. Delaune, in Formal Models and Techniques for
Analyzing Security Protocols, ed. V. Cortier and S. Kremer, IOS Press, 2011, pp. 35-61.
- Models of Multilevel Computer Security, in Advances in Computers,
ed. Marshall C. Yovits, Vol 29, 1989, pp. 1-45.
- Operating System Security Verification, in Case Studies in Mathematical Modeling,
ed. W.E. Boyce, Pitman, 1981, pp. 335-386.
- A universal Turing Machine, BYTE, Dec. 1976.
- One-Dimensional Life, BYTE, Dec. 1978.
- Programming the game of Go, BYTE, April 1981.
- Some articles for nibble Mac, 1986-88, and Macintosh Hands On, 1989.