Online Papers of John D. Ramsdell

Deducing Security Goals From Shape Analysis Sentences. The MITRE Corporation, January 2012. The paper describes a method for extracting a sentence is First-Order Logic that characterizes a run of CPSA, the Cryptographic Protocol Shapes Analyzer. Security goals can be deduced from the sentence. [PDF]
Implementing Strand Space Algebras. The MITRE Corporation, March 2011. The paper describes the order-sorted quotient term algebras used in the implementation of message algebras in CPSA, the Cryptographic Protocol Shapes Analyzer. Joint work with Moses D. Liskov. [PDF]
An Analysis of the CAVES Attestation Protocol using CPSA. MITRE Technical Report MTR90213. The MITRE Corporation, December 2009. The report describes the CAVES attestation protocol and presents a tool-supported analysis showing that the runs of protocol achieve stated goals. Joint work with Joshua Guttman, Jonathan Millen, and Brian O'Hanlon. [PDF]
Programming Cryptographic Protocols. LNCS, Vol. 3705, pp. 116-145. Springer-Verlag GmbH, 2005. The paper describes a tiny programming language tailored to defining cryptographic protocols with trust management annotations, as in the trust management paper below. It defines a semantics via strand spaces and provides methods for proving programs meet their security goals. Joint work with Joshua D. Guttman, Jonathan C. Herzog, and Brian T. Sniffen. [PDF] [Implementation].
Trust Management in Strand Spaces: A Rely-Guarantee Method. LNCS, Vol. 2986, pp. 325-339. Springer-Verlag GmbH, 2004. The paper shows how to combine trust management with nonce-based cryptographic protocols. Joint work with Joshua D. Guttman, Jonathan C. Herzog, F. Javier Thayer, Jay A. Carlson, and Brian T. Sniffen. [PDF].
Information Flow Policies for SELinux. WITS 2003. The paper describes the use of Linear Temporal Logic to specify information flow policies for SELinux, which can then be checked via model-checking. Joint work with Joshua D. Guttman and Amy L. Herzog. [PDF].
A Foundation for a Semantic Web. A semantic web is a web of data designed to be processed by machines. It enables processing based on the meaning of the data. To be useful, semantic data will be combined from several sources. This paper focuses on the relation of the combined data to its sources. Using the method of interpretations between theories in a logic with undefined terms, it establishes criteria for combining information in a fashion that preserves the inferences available in the original information. [Gzipped PostScript] [PDF].
The Tail-Recursive SECD Machine. Journal of Automated Reasoning, Vol. 23, No. 1, pp. 43-62, July 1999. The document describes a correctness proof of a tail-recursive variation of Landin's SECD machine using the Boyer-Moore theorem prover. A late draft is available as [Gzipped PostScript] [PDF]. The theorem prover inputs for the connectness proof of the SECD machine and its tail-recursive variant are available as [secd.events] and [trsecd.events].
Vlisp: A Verified Implementation of Scheme. The archive contains copies of three papers documenting the results of the Vlisp project. They made up Lisp and Symbolic Computation, volume 8 numbers 1/2 (1995), a special issue devoted to Vlisp. A related paper of Kelsey and Rees is also available here. [Vlisp LASC directory]. Also available is The Verified Programming Language Implementation project papers, The MITRE Corporation, and Northeastern University. [Vlisp report directory]. The Verification Yin-Yang logo graced the cover of many Vlisp documents. [SVG] [MetaPost].
An Operational Semantics for Scheme. Lisp Pointers, V(2), 6-10, April-June 1992. [Gzipped PostScript].
Scheme: The Next Generation. Lisp Pointers, Vol. VII, No. 4, October-December 1994, pages 13-14. [Gzipped PostScript].
CST: An Expression Oriented Dialect of C. ACM SIGPLAN Notices, Vol. 30, No. 12, December 1995. C State transformers (CST) is an expression oriented dialect of C designed to smoothly integrate functional programming into C based software [Gzipped PostScript] [PDF]. This link contains a desciption of CST and a compiler based on GCC.
Singular Edge Identification is CoNP-Complete. November 18, 1980. [Gzipped PostScript] [PDF].
The song You Know I Know as [MP3], [MID], [CSD], [Gzipped PostScript], or [PDF].
The poem Tigger on Scheme.

Other Publications

Guttman, J. D., Wand, W., Eds. VLISP: A Verified Implementation of Scheme, Kluwer Academic Press, Boston, 1995.

Farmer, W. M., Ramsdell, J. D., Watro, R. J., "A Correctness Proof for Combinator Reduction with Cycles," ACM Trans. on Programming Languages and Systems, Vol. 12, No. 1, pp. 123-134, January 1990.

Ramsdell, J. D., "The Alonzo Functional Programming Language," SIGPLAN Notices, Vol. 24, No. 9, pp. 152-157, September 1989.

Ramsdell, J. D., "The CURRY Chip," In 1986 ACM Symposium on LISP and Functional Programming, pp. 122-131, Cambridge, MA, August 1986.

Newsam, G. N., Ramsdell, J. D., "Estimation of Sparse Jacobian Matrices," J. Alg. Disc. Meth., Vol. 4, No. 3, pp. 404-418, September 1983.

Ramsdell, J. D., "Finding Minimal Feedback Vertex Sets," IEEE Trans. on Circuits and Systems, Vol. CAS-29, No. 9, pp. 644-646, September 1982.

Ramsdell, J. D., "Variable Elimination in the Home Fire Code," presented at the 20th Joint ASME/AIChE National Heat Transfer Conference, No. 81-HT-3, Milwaukee, WI, August 1981.

Ramsdell, J. D., "Prettyprinting Structured Programs with Connector Lines," ACM SIGPLAN Notices, Vol. 14, No. 9, p. 74, September 1979.