Online Papers of John D. Ramsdell
- A Hybrid Analysis for
Security Protocols with State. The MITRE Corporation and
Worcester Polytechnic Institute, April 2014. This paper presents
a framework for modeling stateful protocols. It leverages
theorem-proving--in this instance,
the PVS prover--for
reasoning about computations over state. It combines that with an
focuses on the message-passing part. As a case study we give a
full analysis of the Envelope Protocol, due to Mark Ryan. Joint
work with Daniel J. Dougherty, Joshua D. Guttman, and Paul
D. Rowe. [PDF]
- Proving Security Goals
From Shape Analysis Sentences. The MITRE Corporation,
September 2013. A previous paper described a
method for extracting a sentence is First-Order Logic that
characterizes a run of
Cryptographic Protocol Shapes Analyzer. This paper presents a
method for importing the sentences into a proof assistant on top
of a detailed theory of strand spaces. The result is a
semantically rich environment in which the validity of a security
goal can be determined. [PDF]
- 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
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
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
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]
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
- 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
The theorem prover inputs for the connectness proof of the SECD machine
and its tail-recursive variant are available as [secd.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
report directory]. The Verification Yin-Yang logo graced the
cover of many Vlisp documents. [SVG]
- An Operational Semantics for Scheme. Lisp Pointers, V(2), 6-10,
April-June 1992. [Gzipped
- Scheme: The Next Generation. Lisp Pointers, Vol. VII, No. 4,
October-December 1994, pages 13-14. [Gzipped
- 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
- The song You Know I Know as [MP3],
- The poem Tigger on
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.