Joshua Guttman's Home Page

CSFW

The call for papers for CSF 20 is now available: CSF 20 Venice, July 6-8 2007. The Computer Security Foundations Workshop is planning (subject to IEEE approval) to become an IEEE Symposium in 2007.
See also the Computer Security Foundations home page.

A workshop on Formal and Computational Cryptography will be held in Venice before CSFW, in early July 2007. The previous version was held in Venice between CSF and ICALP, and information on it is available here. The Call For Papers is here.

Papers

Strand Spaces

• Searching for Shapes uses the skeletons-and-homomorphisms idea to mechanize strand space protocol analysis. This shorter version will appear in TACAS 07.
• The Sizes of Skeletons, in which we show that certain confidentiality and authentication goals are decidable using the "skeletons and homomorphisms" approach introduced in the paper above.
• Programming Cryptographic Protocols (pdf) describes a tiny programming language tailored to defining cryptographic protocols with trust management annotations, as in the ESOP paper below. The paper defines a semantics via strand spaces and provides methods for proving programs meet their security goals. Appeared in Trust in Global Computing, 2005 (postproceedings, LNCS 3705).
• Trust Management in Strand Spaces, pdf or alternatively Postscript Version, appearing in the 2004 European Symposium on Programming.
• Authentication tests and disjoint encryption: A design method for security protocols appeared in the Journal of Computer Security. It is a revised version of "Protocol Design via the Authentication Tests", which appeared in Computer Security Foundations Workshop, 2002 csfw version in pdf form.
• Key Compromise and the Authentication Tests, appearing in Electronic Notes in Theoretical Computer Science, with the proceedings of Mathematical Foundations of Programming Semantics 17.
• The Faithfulness of Abstract Protocol Analysis: Message Authentication, Journal of Computer Security, 2004, a paper showing the abstract Dolev-Yao model faithful to the behavior of a concrete cryptosystem, to within a small tolerance of failure. The original version appeared in ACM CCS '01.
• "Protocol Independence via Disjoint Encryption" (Computer Security Foundations Workshop, 2000)
• "Authentication Tests and the Structure of Bundles" (Theoretical Computer Science, 2002, full version)
• "Authentication Tests" (Oakland symposium version, 2000)
• "Strand Spaces: Proving Cryptographic Protocols Correct" (Journal of Computer Security, 1999)

Information Flow Policies for SELinux

Netwide Security Policies

• New: "Rigorous Automated Network Security Management" (in pdf), forthcoming in International Journal of Information Security. Also available in postscript. Incorporates material from the two papers below, with brief descriptions of our implementations.
• "Filtering Postures: Local Enforcement for Global Security Policies" (Oakland symposium, 1997)
• "Authentication and Confidentiality via IPsec" (ESORICS, 2000), or alternatively in pdf format here.

FOSAD Chapter

• My chapter is available in gzipped postscript format or else in pdf.

Emacs

• Do people send you those pesky MS Word documents? Even when a few paragraphs of ordinary text would be just as good?

  If so, you need undoc.el.

  To use it reading mail via gnus, use the following two forms:

  (setq mm-inline-media-tests (cons
  			     (list "application/.*msword" 
                                      'mm-display-msword-inline 
                                      (lambda (handle) t))
  			     mm-inline-media-tests)
        mm-inlined-types      (cons "application/.*msword" mm-inlined-types))
  
  (defun mm-display-msword-inline (handle) 
    (let (text)
      (with-temp-buffer
        (mm-insert-part handle)
        (save-window-excursion
  	(undoc-current-buffer)
  	(setq text (buffer-string))))
      (mm-insert-inline handle text)))
  

Older material

• Imps, an Interactive Mathematical Proof System (Home Page). I am grateful to the McMaster Computer Engineering Department for allowing us to maintain the Imps site on their server.
• Vlisp: A Verified Implementation of Scheme. This 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.

CSFW

The CSFW-18 program is here, or, in plain text format, here.

I am grateful to the College of Computer Science at Northeastern University for making this home page available to me.