diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,40 @@ +2012-11-09 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as version 2.2.12. + +2012-11-06 John D. Ramsdell + + * doc/index.tex: Added a section on useful tips. + + * doc/cpsauser.tex: Added description of Emacs Compilation Mode + support. + +2012-10-30 John D. Ramsdell + + * src/cpsaperm.scm: Added a Scheme program that renumbers the + strands in a skeleton while preserving all information in the + skeleton. + +2012-10-29 John D. Ramsdell + + * doc/cpsaintroslides.tex: Added introductory slides for new + users. + +2012-10-26 John D. Ramsdell + + * src/cpsa.pl: Added support for penetrator non-origination + assumptions. + +2012-10-25 John D. Ramsdell + + * src/perm.pl: Added a program that renumbers the strands within a + skeleton. This program also strips the skeleton of non-essential + information. + +2012-10-02 John D. Ramsdell + + * src/CPSA/Pretty/Main.hs (pjson): Added JSON output option. + 2012-08-24 John D. Ramsdell * cpsa.cabal (Version): Tagged as version 2.2.11. diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,5 +1,17 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.2.12 + +** Documentation improved + The introductory documentation has been improved and a set of + slides has been added that is aimed at new users. + +** JavaScript Object Notation (JSON) output supported + The CPSA pretty printer cpsapp produces JSON output when given the + -j or --json command-line option. A CPSA string translates to a + JSON string in which the first and last characters are a double + quote. A CPSA symbol translates directly to a JSON string. + * Changes in version 2.2.11 ** Strand bounded runs produce more output diff --git a/README b/README --- a/README +++ b/README @@ -96,6 +96,9 @@ DOCUMENTATION +The starting point for CPSA documentation doc/index.html. Most users +should read it and skip the rest of this section. + To build the documentation, the file supp-pdf.tex must be installed. It is part of the TexLive texmf ConTeXt package. On Linux, the name of the package is context or texlive-context. The design document and @@ -132,8 +135,10 @@ The src directory of the source distributions includes programs written in Scheme, Prolog, and Elisp for performing tasks. Use them -as templates for your special perpose CPSA analysis and transformation -needs. +as templates for your special purpose CPSA analysis and transformation +needs. Also, when given the --json option, the CPSA pretty printer +cpsapp will transform CPSA S-expressions into JavaScript Object +Notation (JSON). On Linux, the GHC runtime can request so much memory that thrashing results. The script in src/ghcmemlimit sets an environment variable diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 2.2.11 +Version: 2.2.12 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3 @@ -14,27 +14,29 @@ determine from them, as are attacks and anomalies. . For each input problem, the CPSA program is given some initial - behavior, and it discovers what shapes are compatible with it. - Normally, the initial behavior is from the point of view of one - participant. The analysis reveals what the other participants must - have done, given the participant's view. - . - We are working towards a version of CPSA with the property that - whenever it successfully terminates, every possible execution is - described by its output. A proof of this correctness property is - also in development. + behavior, and it discovers what shapes are compatible with + it. Normally, the initial behavior is from the point of view of one + participant. The analysis reveals what the other participants must + have done, given the participant's view. The search is based on a + high-level algorithm that was claimed to be complete, i.e. every + shape can in fact be found in a finite number of steps. Further + theoretical work showed classes of executions that are not found by + the algorithm, however it also showed that every omitted execution + requires an unnatural interpretation of a protocol's roles. Hence + the algorithm is complete relative to natural role semantics. . The package contains a set of programs used to perform and display the analysis. A standards complient browser, such as Firefox, Safari, or Chrome, is required to display the results. Program documentation is in the doc directory in the source distribution, and installed in the package's data directory. You can locate the - package's data directory by typing "cpsa --help" in a command + package's data directory by typing "cpsa --help" to a command prompt. New users should study the documentation and the sample inputs in the data directory. The source distribution includes a - test suite with an expanded set of input files and program design - documentation. Serious Windows users should install MSYS so as to - allow the use of make and script execution. + test suite with an expanded set of input files and is easily + installed on operating systems that decend from Unix. Serious + Windows users should install MSYS so as to allow the use of make and + script execution. . The theory and algorithm used by CPSA was developed with the help of Joshua D. Guttman, John D. Ramsdell, Jon C. Herzog, Shaddin @@ -43,69 +45,72 @@ Category: Cryptography Build-Type: Simple Data-Files: - index.html cpsauser.html cpsa.mk Make.hs cpsaprimer.pdf - cpsaoverview.pdf cpsaspec.pdf cpsadesign.pdf cpsadha.pdf - ffgg.scm ns.scm or.scm woolam.scm yahalom.scm dhke.scm + index.html readme.html cpsauser.html cpsa.mk Make.hs cpsaprimer.pdf + cpsaoverview.pdf cpsaintroslides.pdf cpsaspec.pdf cpsadesign.pdf + cpsadha.pdf ffgg.scm ns.scm blanchet.scm or.scm woolam.scm + yahalom.scm dhke.scm Data-Dir: doc Extra-Source-Files: - Makefile ChangeLog README NEWS ghci cpsatst setup.bat doc/README - doc/Makefile doc/macros.tex doc/cpsaprimer.tex doc/bcasyntax.tex + Makefile ChangeLog README NEWS ghci cpsatst setup.bat + doc/README doc/Makefile doc/macros.tex doc/cpsaprimer.tex + doc/bcasyntax.tex doc/cpsaintroslides.tex doc/mitreslides.sty doc/cpsaspec.tex doc/cpsadesign.tex doc/cpsaoverview.tex doc/cpsadha.tex doc/cpsadiagrams.mp doc/strands.mp doc/cmstrands.mp - doc/carriers.mp doc/termtree.mp doc/cpsa.bib doc/SDAG.lhs + doc/carriers.mp doc/termtree.mp doc/blanchet.mp doc/mitrelogo.mp + doc/cpsa.bib doc/SDAG.lhs src/index.html src/cpsacgi src/cpsacgi.py src/cpsa2svg src/cpsa.el - src/httpd_allow_execmem.te src/cpsaops.scm src/preskel src/cpsa.pl - src/pp.pl src/sexpr.pl src/prover9.pl src/zoom.js src/js2hs - src/ghcmemlimit build.xml src/cpsaextras/Main.scala - src/cpsaextras/Pretty.scala src/cpsaextras/Printer.scala - src/cpsaextras/SExpr.scala tst/README tst/Makefile tst/Make.hs - tst/checktst tst/cpsagraphall tst/cpsashapesall tst/blanchet.scm - tst/blanchet.tst tst/completeness-test.scm tst/completeness-test.tst - tst/crushing.tst tst/crushing.tst tst/dass.lisp tst/dass-mod.lisp - tst/dass_simple.scm tst/dass_simple.tst tst/denning-sacco.scm - tst/denning-sacco.tst tst/deorig_contract.scm - tst/deorig_contract.tst tst/dhke.scm tst/dhke.tst - tst/deorig_simple.scm tst/deorig_simple.tst tst/ds-short.lisp - tst/deorig_mesg.scm tst/deorig_mesg.tst - tst/dy.lsp tst/dy.tst tst/encsig.scm tst/encsig.tst - tst/epmo_acctnum.scm tst/epmo_acctnum.tst tst/epmo.scm tst/epmo.tst - tst/ffgg.scm tst/ffgg.tst tst/fragile_pruning.scm - tst/fragile_pruning.tst tst/isoreject.scm tst/isoreject.tst - tst/kelly1.scm tst/kelly1.tst tst/kelly64.lisp tst/kerb5.lisp - tst/kerberos.scm tst/kerberos.tst tst/missing_contraction.scm - tst/missing_contraction.tst tst/neuman-stubblebine-alt.lisp - tst/neuman-stubblebine-reauth.lisp tst/neuman-stubblebine-reauth.lsp - tst/neuman-stubblebine-reauth.tst tst/neuman-stubblebine.scm - tst/neuman-stubblebine.tst tst/no_contraction.scm - tst/no_contraction.tst tst/nonaug-prune.scm tst/nonaug-prune.tst - tst/non_transforming.scm tst/non_transforming.tst tst/nsl3.scm - tst/nsl3.tst tst/nsl4cm1.lsp tst/nsl4cm1.tst tst/nsl4.lisp - tst/nsl4resp2.lisp tst/nsl5i.lisp tst/nsl5.lisp tst/nslsk.scm - tst/nslsk.tst tst/ns.scm tst/ns.tst tst/or.scm tst/or.tst - tst/pca.scm tst/pca.tst tst/pruning1.scm tst/pruning1.tst - tst/sigenc.scm tst/sigenc.tst tst/sorted_epmo_acctnum.scm - tst/sorted_epmo_acctnum.tst tst/targetterms2.scm - tst/targetterms2.tst tst/targetterms6.scm tst/targetterms6.tst - tst/targetterms8.scm tst/targetterms8.tst tst/tnsl5.lisp - tst/uncarried_keys.scm tst/uncarried_keys.tst tst/uo.scm tst/uo.tst - tst/updatetst tst/weird.scm tst/weird.tst tst/wide-mouth-frog.lsp - tst/wide-mouth-frog.tst tst/wide-mouth-frog-scyther.lsp - tst/wide-mouth-frog-scyther.tst tst/wonthull2.scm tst/wonthull2.tst - tst/wonthull3.scm tst/wonthull3.tst tst/wonthull.scm - tst/wonthull.tst tst/woolam.scm tst/woolam.tst tst/yahalom-6.3.6.scm - tst/yahalom-6.3.6.tst tst/yahalom.scm tst/yahalom.tst tst/tor.scm - tst/tor.tst tst/dh_cert.scm tst/dh_cert.tst - tst/epmo_acctnum-key-hash.scm tst/epmo_acctnum-key-hash.tst - tst/epmo-key-hash.scm tst/epmo-key-hash.tst tst/wang.lisp - tst/pkinit.scm tst/pkinit.tst tst/print.scm tst/print.tst - tst/epmo-hash.scm tst/epmo-hash.tst tst/hashtest-key-hash.scm - tst/hashtest-key-hash.tst tst/hashtest.scm tst/hashtest.tst - tst/wang-key-hash.scm tst/wang-key-hash.tst tst/wang-hash.scm - tst/wang-hash.tst tst/mass.lsp tst/mass.tst tst/mass2.lsp tst/mass2.tst - tst/DH_hack.scm tst/DH_hack.tst tst/timestamping.scm tst/timestamping.tst - tst/ns-l.scm tst/ns-l.tst tst/pen-non-orig-test.scm - tst/pen-non-orig-test.tst tst/preprocess.scm tst/preprocess.tst - tst/incompleteness_example.scm tst/incompleteness_example.tst + src/httpd_allow_execmem.te src/cpsaperm.scm src/cpsaops.scm + src/preskel src/cpsa.pl src/pp.pl src/sexpr.pl src/perm.pl + src/prover9.pl src/zoom.js src/js2hs src/ghcmemlimit build.xml + src/cpsaextras/Main.scala src/cpsaextras/Pretty.scala + src/cpsaextras/Printer.scala src/cpsaextras/SExpr.scala + tst/README tst/Makefile tst/Make.hs tst/checktst tst/cpsagraphall + tst/cpsashapesall tst/blanchet.scm tst/blanchet.tst + tst/completeness-test.scm tst/completeness-test.tst tst/crushing.tst + tst/crushing.tst tst/dass.lisp tst/dass-mod.lisp tst/dass_simple.scm + tst/dass_simple.tst tst/denning-sacco.scm tst/denning-sacco.tst + tst/deorig_contract.scm tst/deorig_contract.tst tst/dhke.scm + tst/dhke.tst tst/deorig_simple.scm tst/deorig_simple.tst + tst/ds-short.lisp tst/deorig_mesg.scm tst/deorig_mesg.tst tst/dy.lsp + tst/dy.tst tst/encsig.scm tst/encsig.tst tst/epmo_acctnum.scm + tst/epmo_acctnum.tst tst/epmo.scm tst/epmo.tst tst/ffgg.scm + tst/ffgg.tst tst/fragile_pruning.scm tst/fragile_pruning.tst + tst/isoreject.scm tst/isoreject.tst tst/kelly1.scm tst/kelly1.tst + tst/kelly64.lisp tst/kerb5.lisp tst/kerberos.scm tst/kerberos.tst + tst/missing_contraction.scm tst/missing_contraction.tst + tst/neuman-stubblebine-alt.lisp tst/neuman-stubblebine-reauth.lisp + tst/neuman-stubblebine-reauth.lsp tst/neuman-stubblebine-reauth.tst + tst/neuman-stubblebine.scm tst/neuman-stubblebine.tst + tst/no_contraction.scm tst/no_contraction.tst tst/nonaug-prune.scm + tst/nonaug-prune.tst tst/non_transforming.scm + tst/non_transforming.tst tst/nsl3.scm tst/nsl3.tst tst/nsl4cm1.lsp + tst/nsl4cm1.tst tst/nsl4.lisp tst/nsl4resp2.lisp tst/nsl5i.lisp + tst/nsl5.lisp tst/nslsk.scm tst/nslsk.tst tst/ns.scm tst/ns.tst + tst/or.scm tst/or.tst tst/pca.scm tst/pca.tst tst/pruning1.scm + tst/pruning1.tst tst/sigenc.scm tst/sigenc.tst + tst/sorted_epmo_acctnum.scm tst/sorted_epmo_acctnum.tst + tst/targetterms2.scm tst/targetterms2.tst tst/targetterms6.scm + tst/targetterms6.tst tst/targetterms8.scm tst/targetterms8.tst + tst/tnsl5.lisp tst/uncarried_keys.scm tst/uncarried_keys.tst + tst/uo.scm tst/uo.tst tst/updatetst tst/weird.scm tst/weird.tst + tst/wide-mouth-frog.lsp tst/wide-mouth-frog.tst + tst/wide-mouth-frog-scyther.lsp tst/wide-mouth-frog-scyther.tst + tst/wonthull2.scm tst/wonthull2.tst tst/wonthull3.scm + tst/wonthull3.tst tst/wonthull.scm tst/wonthull.tst tst/woolam.scm + tst/woolam.tst tst/yahalom-6.3.6.scm tst/yahalom-6.3.6.tst + tst/yahalom.scm tst/yahalom.tst tst/tor.scm tst/tor.tst + tst/dh_cert.scm tst/dh_cert.tst tst/epmo_acctnum-key-hash.scm + tst/epmo_acctnum-key-hash.tst tst/epmo-key-hash.scm + tst/epmo-key-hash.tst tst/wang.lisp tst/pkinit.scm tst/pkinit.tst + tst/print.scm tst/print.tst tst/epmo-hash.scm tst/epmo-hash.tst + tst/hashtest-key-hash.scm tst/hashtest-key-hash.tst tst/hashtest.scm + tst/hashtest.tst tst/wang-key-hash.scm tst/wang-key-hash.tst + tst/wang-hash.scm tst/wang-hash.tst tst/mass.lsp tst/mass.tst + tst/mass2.lsp tst/mass2.tst tst/DH_hack.scm tst/DH_hack.tst + tst/timestamping.scm tst/timestamping.tst tst/ns-l.scm tst/ns-l.tst + tst/pen-non-orig-test.scm tst/pen-non-orig-test.tst + tst/preprocess.scm tst/preprocess.tst tst/incompleteness_example.scm + tst/incompleteness_example.tst -- Algebra implementations must import CPSA.Lib.CPSA. -- Tools may additionally import CPSA.Lib.Entry. diff --git a/doc/Makefile b/doc/Makefile --- a/doc/Makefile +++ b/doc/Makefile @@ -11,6 +11,7 @@ PRIMER = cpsaprimer OVERVIEW = cpsaoverview +SLIDES = cpsaintroslides DESIGN = cpsadesign SPEC = cpsaspec DHA = cpsadha @@ -18,7 +19,7 @@ TEX_SRCS = macros.tex bcasyntax.tex -MP_SRCS = cpsadiagrams.mp carriers.mp termtree.mp +MP_SRCS = cpsadiagrams.mp carriers.mp termtree.mp blanchet.mp mitrelogo.mp %-0.mps: %.mp mpost -tex=latex $* @@ -31,7 +32,8 @@ %.ind: %.idx makeindex $* -all: $(PRIMER).pdf $(OVERVIEW).pdf $(DESIGN).pdf $(SPEC).pdf $(DHA).pdf +all: $(PRIMER).pdf $(OVERVIEW).pdf $(SLIDES).pdf \ + $(DESIGN).pdf $(SPEC).pdf $(DHA).pdf $(PRIMER).pdf: $(MP_SRCS:.mp=-0.mps) $(TEX_SRCS) \ $(PRIMER).tex $(PRIMER).bbl @@ -43,6 +45,9 @@ if test ! -f $(OVERVIEW).aux; then pdflatex $(OVERVIEW).tex; fi pdflatex $(OVERVIEW).tex +$(SLIDES).pdf: $(MP_SRCS:.mp=-0.mps) $(SLIDES).tex + pdflatex $(SLIDES).tex + $(DESIGN).pdf: $(MP_SRCS:.mp=-0.mps) $(TEX_SRCS) \ $(DESIGN).tex $(DESIGN).bbl if test ! -f $(DESIGN).aux; then pdflatex $(DESIGN).tex; fi @@ -59,7 +64,7 @@ if test ! -f $(DHA).aux; then pdflatex $(DHA).tex; fi pdflatex $(DHA).tex -CLEAN_FILES := $(PRIMER).pdf $(OVERVIEW).pdf \ +CLEAN_FILES := $(PRIMER).pdf $(OVERVIEW).pdf $(SLIDES).pdf \ $(DESIGN).pdf $(SPEC).pdf $(DHA).pdf \ $(wildcard *.log *.aux *.toc *.mps *.mpx) \ $(wildcard *.bbl *.blg *.ind *.idx *.ilg *.out) diff --git a/doc/README b/doc/README --- a/doc/README +++ b/doc/README @@ -1,5 +1,7 @@ This directory contains CPSA documentation. +* index.html: Documentation starting point with some useful tips. + * cpsauser.html: CPSA User Guide, an essential reference document * cpsaprimer.pdf: CPSA Primer, an introduction to using CPSA @@ -11,7 +13,7 @@ * cpsadesign.pdf: CPSA Design, a description of implementation choices -* cpsadha.pdf: Diffie-Hellman Algebra +* cpsadha.pdf: Diffie-Hellman Algebra (an experiment with known flaws). To build the documentation, you need Metapost and XY-pic. On Linux, Metapost is supplied via the package texlive-metapost, and XY-pic is diff --git a/doc/blanchet.mp b/doc/blanchet.mp new file mode 100644 --- /dev/null +++ b/doc/blanchet.mp @@ -0,0 +1,146 @@ +filenametemplate "%j-%c.mps"; + +verbatimtex +\documentclass{slides} +\usepackage{color} +\newcommand{\enc}[2]{\{\!|#1|\!\}_{#2}} +\newcommand{\privk}[1]{\ensuremath{K^{-1}_{#1}}} +\newcommand{\pubk}[1]{\ensuremath{K_{#1}}} +\newcommand{\msgone}{$\enc{\enc{S}{\privk{A}}}{\pubk{B}}$} +\newcommand{\msgtwo}{$\enc{D}{S}$} +\newcommand{\msgthree}{$\enc{\enc{S,B}{\privk{A}}}{\pubk{B}}$} +\newcommand{\msgfour}{$\enc{\enc{S}{\privk{A}}}{\pubk{\textcolor{blue}{B'}}}$} +\newcommand{\msgfive}{$\enc{\enc{S}{\privk{A}}}{\pubk{B'}}$} +\newcommand{\msgsix}{\ensuremath{\enc{S}{\privk{A}}}} +\begin{document} +etex + +input boxes; + +input strands; + +input cmstrands; + +ahlength := 2mm; % Arrow head length + +picture node; node = btex $\bullet$ etex; + +% The height of a downarrow is the unit of length for a strand +% succession edge. + +numeric delta; +begingroup; + path p; p = bbox(btex $\downarrow$ etex); + delta = ypart(ulcorner p - llcorner p); +endgroup; + +% The width of a leftarrow is the unit of length for a directed term +% symbol. + +numeric dir_width; +begingroup; + path p; p = bbox(btex $\leftarrow$ etex); + dir_width = xpart (lrcorner p - llcorner p); +endgroup; + +w = 19cm; % Width of diagram + +% Node vertical node separation is gamma + +numeric gamma; +gamma = 2delta; + +beginfig(0); + % Backbone + strand.a(2, origin, gamma, btex $\mathstrut\mathit{init}$ etex, node); + + % Messages + outbnd.a(1, dir_width, btex \msgone etex); + inbnd.a(2, dir_width, btex \msgtwo etex); +endfig; + +% Responder role + +beginfig(1); + % Backbone + strand.a(2, origin, gamma, btex $\mathstrut\mathit{resp}$ etex, node); + + % Messages + rinbnd.a(1, dir_width, btex \msgone etex); + routbnd.a(2, dir_width, btex \msgtwo etex); +endfig; + +beginfig(2); + % Backbone + strand.a(2, origin, gamma, btex $\mathstrut\mathit{init}$ etex, node); + + % Messages + outbnd.a(1, dir_width, btex \msgthree etex); + inbnd.a(2, dir_width, btex \msgtwo etex); +endfig; + +% Responder role + +beginfig(3); + % Backbone + strand.b(2, origin, gamma, btex $\mathstrut\mathit{resp}$ etex, node); + + % Messages + rinbnd.b(1, dir_width, btex \msgthree etex); + routbnd.b(2, dir_width, btex \msgtwo etex); +endfig; + +beginfig(4); + % Backbones + strand.b(2, origin, gamma, + btex $\mathstrut\mathit{resp}$ etex, node); + strand.a(1, (w, ypart b1.c), gamma, + btex $\mathstrut\mathit{init}$ etex, node); + + boxit.o1(btex $\succ$ etex); + o1.c = .5[b1.c,a1.c]; + draw pic o1; + + drawmsg(a1.w -- o1.e); + drawmsg(o1.w -- b1.e); + label.top(btex \msgfour etex, .5[a1.w,o1.e]); + label.top(btex \msgone etex, .5[o1.w,b1.e]); +endfig; + +beginfig(5); + % Initial point-of-view + strand.b(2, origin, gamma, + btex $\mathstrut\textcolor{red}{\mathit{resp}}$ etex, node); +endfig; + +beginfig(6); + % Bundle + strand.b(2, origin, gamma, + btex $\mathstrut\mathit{resp}$ etex, node); + strand.e(3, (2w/3, ypart b1.c), gamma, + btex $\mathstrut\mathit{enc}$ etex, node); + strand.g(1, (w/3, ypart e2.c), gamma, + btex $\mathstrut\mathit{gen}$ etex, node); + strand.d(3, (w/3, ypart e1.c), gamma, + btex $\mathstrut\mathit{dec}$ etex, node); + strand.h(1, (2w/3, ypart d2.c), gamma, + btex $\mathstrut\mathit{gen}$ etex, node); + strand.a(1, (w, ypart d1.c), gamma, + btex $\mathstrut\mathit{init}$ etex, node); + + drawmsg(e3.w -- b1.e); + label.top(btex \msgone etex, .5[e3.w,b1.e]); + drawmsg(g1.e -- e2.w); + label.top(btex \pubk{B} etex, .5[g1.e,e2.w]); + drawmsg(d3.e -- e1.w); + label.top(btex \msgsix etex, .5[d3.e,e1.w]); + drawmsg(h1.w -- d2.e); + label.top(btex \privk{B'} etex, .5[h1.w,d2.e]); + drawmsg(a1.w -- d1.e); + label.top(btex \msgfive etex, .5[a1.w,d1.e]); +endfig; + +verbatimtex +\end{document} +etex +bye; diff --git a/doc/blanchet.scm b/doc/blanchet.scm new file mode 100644 --- /dev/null +++ b/doc/blanchet.scm @@ -0,0 +1,88 @@ +(herald "Blanchet's Simple Example Protocol" + (comment "There is a flaw in this protocol by design")) + +(defprotocol blanchet basic + (defrole init + (vars (a b name) (s skey) (d data)) + (trace + (send (enc (enc s (privk a)) (pubk b))) + (recv (enc d s)))) + (defrole resp + (vars (a b name) (s skey) (d data)) + (trace + (recv (enc (enc s (privk a)) (pubk b))) + (send (enc d s)))) + (comment "Blanchet's protocol using named asymmetric keys")) + +(defskeleton blanchet + (vars (a b name) (s skey) (d data)) + (defstrand init 2 (a a) (b b) (s s) (d d)) + (non-orig (privk b)) + (uniq-orig s) + (comment "Analyze from the initiator's perspective")) + +(defskeleton blanchet + (vars (a b name) (s skey) (d data)) + (defstrand init 2 (a a) (b b) (s s) (d d)) + (deflistener d) + (non-orig (privk b)) + (uniq-orig s d) + (comment "From the initiator's perspective, is the secret leaked?")) + +(defskeleton blanchet + (vars (a b name) (s skey) (d data)) + (defstrand resp 2 (a a) (b b) (s s) (d d)) + (non-orig (privk a) (privk b)) + (uniq-orig s) + (comment "Analyze from the responder's perspective")) + +(defskeleton blanchet + (vars (a b name) (s skey) (d data)) + (defstrand resp 2 (a a) (b b) (s s) (d d)) + (deflistener d) + (non-orig (privk a) (privk b)) + (uniq-orig s d) + (comment "From the responders's perspective, is the secret leaked?")) + +(defprotocol blanchet-fixed basic + (defrole init + (vars (a b name) (s skey) (d data)) + (trace + (send (enc (enc s b (privk a)) (pubk b))) + (recv (enc d s)))) + (defrole resp + (vars (a b name) (s skey) (d data)) + (trace + (recv (enc (enc s b (privk a)) (pubk b))) + (send (enc d s)))) + (comment "Fixed Blanchet's protocol using named asymmetric keys")) + +(defskeleton blanchet-fixed + (vars (a b name) (s skey) (d data)) + (defstrand init 2 (a a) (b b) (s s) (d d)) + (non-orig (privk b)) + (uniq-orig s) + (comment "Analyze from the initiator's perspective")) + +(defskeleton blanchet-fixed + (vars (a b name) (s skey) (d data)) + (defstrand init 2 (a a) (b b) (s s) (d d)) + (deflistener d) + (non-orig (privk b)) + (uniq-orig s d) + (comment "From the initiator's perspective, is the secret leaked?")) + +(defskeleton blanchet-fixed + (vars (a b name) (s skey) (d data)) + (defstrand resp 2 (a a) (b b) (s s) (d d)) + (non-orig (privk a) (privk b)) + (uniq-orig s) + (comment "Analyze from the responder's perspective")) + +(defskeleton blanchet-fixed + (vars (a b name) (s skey) (d data)) + (defstrand resp 2 (a a) (b b) (s s) (d d)) + (deflistener d) + (non-orig (privk a) (privk b)) + (uniq-orig s d) + (comment "From the responders's perspective, is the secret leaked?")) diff --git a/doc/cpsadesign.pdf b/doc/cpsadesign.pdf Binary files a/doc/cpsadesign.pdf and b/doc/cpsadesign.pdf differ diff --git a/doc/cpsadha.pdf b/doc/cpsadha.pdf Binary files a/doc/cpsadha.pdf and b/doc/cpsadha.pdf differ diff --git a/doc/cpsadha.tex b/doc/cpsadha.tex --- a/doc/cpsadha.tex +++ b/doc/cpsadha.tex @@ -38,6 +38,9 @@ \maketitle \cpsacopying +\emph{The current attempts to support an algebra for Diffie-Hellman + are experimental and they all known to have flaws.} + A natural way to model protocols that use Diffie-Hellman is with an algebra that includes a sort for exponents, one with members that form an Abelian group. Implementation experiments have shown that it is diff --git a/doc/cpsaintroslides.pdf b/doc/cpsaintroslides.pdf new file mode 100644 Binary files /dev/null and b/doc/cpsaintroslides.pdf differ diff --git a/doc/cpsaintroslides.tex b/doc/cpsaintroslides.tex new file mode 100644 --- /dev/null +++ b/doc/cpsaintroslides.tex @@ -0,0 +1,395 @@ +\documentclass[landscape]{slides} +\usepackage{mitreslides} +\usepackage{amssymb} +\usepackage{amsmath} +\usepackage{color} +\usepackage{graphicx} +\usepackage{alltt} +\usepackage{url} +%\usepackage{hyperref} + +\newcommand{\cpsa}{CPSA} +\DeclareMathOperator{\domm}{\mathit{dom}} +\newcommand{\cn}[1]{\ensuremath{\mathop{\relax + \smash{\sf#1}}\!\mathop{\vphantom{#1}}\nolimits}} +\newcommand{\dom}[1]{\ensuremath{\mathop{\relax + \smash{\rm#1}}\!\mathop{\vphantom{#1}}\nolimits}} +\newcommand{\fn}[1]{\ensuremath{\mathop{\relax + \smash{\it#1}}\!\mathop{\vphantom{#1}}\nolimits}} +\newcommand{\termalg}{\ensuremath{\mathfrak T}} +\newcommand{\mesgalg}{\ensuremath{\mathfrak A}} +\newcommand{\tr}{\ensuremath{\mathfrak C}} +\newcommand{\ints}{\ensuremath{\mathbb Z}} +\newcommand{\bundle}{\ensuremath{\mathcal{B}}} +\newcommand{\nterm}[1]{\ensuremath{\langle\mathit{#1}\rangle}} +\newcommand{\nterms}[1]{\ensuremath{\nterm{#1}^\ast}} +\newcommand{\ntermp}[1]{\ensuremath{\nterm{#1}^+}} +\newcommand{\ntermo}[1]{#1$^?$} +\newcommand{\enc}[2]{\{\!|#1|\!\}_{#2}} +\newcommand{\invk}[1]{{#1}^{-1}} +\newcommand{\pubk}[1]{K_{#1}} +\newcommand{\privk}[1]{K^{-1}_{#1}} +\newcommand{\eqq}{\stackrel{?}{=}} +\newcommand{\hash}[1]{\#(#1)} +\newcommand{\inbnd}{\mathord -} +\newcommand{\outbnd}{\mathord +} +\newcommand{\cert}{\mathsf{cert}} +\newcommand{\valid}{\mathsf{valid}} +\newcommand{\data}{\mathsf{data}} +\newcommand{\says}{\mathbin{\mathrm{says}}} +\DeclareMathOperator{\ok}{\mathit{ok}} +\DeclareMathOperator{\id}{\mathit{id}} +\DeclareMathOperator{\resource}{\mathit{resource}} +\DeclareMathOperator{\approved}{\mathit{approved}} +\DeclareMathOperator{\ask}{\mathit{ask}} +\DeclareMathOperator{\meas}{\mathit{meas}} +\DeclareMathOperator{\verifier}{\mathit{verifier}} +\DeclareMathOperator{\auth}{\mathit{auth}} +\DeclareMathOperator{\epca}{\mathit{epca}} +\DeclareMathOperator{\ltk}{\mathsf{ltk}} +\newcommand{\ctosa}{\enc{R,A,K}{K_S}} +\newcommand{\stova}{\enc{S,A,R,N_S}{K_V}} +\newcommand{\ptova}{\enc{\cert,A,I,E}{\invk{K}_E}} +\newcommand{\vtosa}{\enc{N_V,J,V,N_S,M}{K_S}} +\newcommand{\stoca}{\enc{N_V,J,V,M}{K}} +\newcommand{\ctoaa}{\enc{S, N_V,J,V,M,R}{\ltk(A,A)}} +\newcommand{\atoca}{\enc{K',N_V,B}{\ltk(A,A)}} +\newcommand{\blob}{\enc{K',S,J_O,M,P, +\enc{\hash{\hash{A,V,N_V,J_O},M,P}}{\invk{}}}{K_V}} +\newcommand{\vtosb}{\enc{\valid,N_S,K'}{K_S}} +\newcommand{\stocb}{\enc{\data,D}{K'}} +\newcommand{\seq}[1]{\langle#1\rangle} +\newcommand{\append}{\mathbin{{}^\frown}} +\newcommand{\flow}[3]{\ensuremath{#1,#2\rhd#3}} +\newcommand{\infer}[2]{\begin{array}{c}#1\\\hline#2\end{array}} +\newcommand{\inferb}[2]{\begin{array}[b]{c}#1\\\hline#2\end{array}} +\newcommand{\infertwo}[3]{\inferb{#1\quad#2}{#3}} +\newcommand{\termat}{\mathbin{@}} +\newcommand{\all}[1]{\forall#1\mathpunct{.}} +\newcommand{\some}[1]{\exists#1\mathpunct{.}} +\newcommand{\idsigma}{\sigma_{\mathrm{id}}} + +\newenvironment{zitemize} +{\begin{itemize} +\setlength{\itemsep}{0em} +\setlength{\topsep}{0em} +\setlength{\partopsep}{0em} +\setlength{\parsep}{0em} +\setlength{\parskip}{0em}}% +{\end{itemize}} + +\begin{document} + +\begin{titleslide}{Symbolic Cryptographic Protocol \\ Analysis using CPSA} +% +John D.~Ramsdell\\ +~\\ +The MITRE Corporation\\ +~\\ +October 2012 +\end{titleslide} + +\begin{mitreslide}{Cyptographic Protocol Shapes Analyzer} +\begin{description} +\item [Goal:] Protocol analysis using Dolev-Yao model +\item [Foundation:] Strand Spaces +\item [Distribution:] \url{http://hackage.haskell.org/package/cpsa} +\item [Contributors:] + Joshua D. Guttman, John D. Ramsdell, Jon C. Herzog, Shaddin + F. Doghmi, F. Javier Thayer, Paul D. Rowe, and Moses D. Liskov +\end{description} +\end{mitreslide} + +\begin{note} + Pages of this form attempt to fill in the spoken part of a + class using these slides. + + The Cryptographic Protocol Shapes Analyzer ({\cpsa}) attempts to + enumerate all essentially different executions possible for a + cryptographic protocol. We call them the \emph{shapes} of the + protocol. Naturally occurring protocols have only finitely many, + indeed very few shapes. Authentication and secrecy properties are + easy to determine from them, as are attacks and anomalies. + + This presentation gives a very brief tour of the tool and how it is + used in practice. +\end{note} + +\begin{mitreslide}{Anatomy of a CPSA Installation} +\begin{zitemize} +\item Programs +\begin{zitemize} +\item \texttt{cpsa}: main analysis tool +\item \texttt{cpsashapes}: extracts shapes from \texttt{cpsa} output +\item \texttt{cpsagraph}: visualize output using XHTML and SVG +\item \texttt{cpsadiff}: compare two \texttt{cpsa} output files +\item \texttt{cpsaannotations}: support rely-guarantee method +\item \texttt{cpsalogic}: produce shape analysis sentences +\item \texttt{cpsapp}: pretty print input and output +\item Build tools: GNU makefile template and a Haskell script +\end{zitemize} +\item Documentation +\begin{zitemize} +\item User documentation: user guide, primer, and overview +\item Sample input: Needham-Schroeder, Blanchet, Woo-Lam, Otway-Rees, + Yahalom, ffgg +\end{zitemize} +\end{zitemize} +\end{mitreslide} + +\begin{note} + Although there are many programs in the {\cpsa} package, typical + usage is very simple. +\end{note} + +\begin{mitreslide}{Using CPSA} +\begin{itemize} +\item With a text editor, user enters a description of a +\begin{zitemize} +\item protocol as a set of roles +\item problem point-of-view\\ (what is assumed to have happened) +\end{zitemize} +\item User runs the tool (\texttt{\$ echo build | ghci Make.hs} \\ + or on Windows, click on \texttt{Make.hs} and type \texttt{build}) +\item In a web browser, user views the output that shows +\begin{zitemize} +\item what else CPSA inferred must have happened, or +\item all CPSA steps used to produce the answers +\end{zitemize} +\end{itemize} +\end{mitreslide} + +\begin{note} + At this point, if you have not already done so, follow the + instructions in \url{index.html} and analyze the examples. The rest + of these slides will focus on Blanchet's ``Simple Example + Protocol'', so open \url{blanchet.xhtml}. Click on + Derivation Tree 9. +\end{note} + +\begin{mitreslide}{Blanchet's ``Simple Example Protocol''} +$$\begin{array}{r@{{}\colon{}}l} +A\to B&\enc{\enc{S}{\privk{A}}}{\pubk{B}}\\ +B\to A&\enc{D}{S} +\end{array}$$ +\begin{center} +CPSA Style Roles \\[2ex] +\begin{tabular}{c} +Initiator ($\fn{init}$ role)\\[3ex] +\includegraphics{blanchet-0.mps} +\end{tabular}\hfil +\begin{tabular}{c} +Responder ($\fn{resp}$ role)\\[3ex] +\includegraphics{blanchet-1.mps} +\end{tabular}\\[3ex] +\end{center} +\end{mitreslide} + +\begin{note} + Blanchet's protocol has two steps. + Alice sends to Bob a freshly generated symmetric key~$S$ signed with Alice's + private key~$\privk{A}$ and then encrypted with Bob's public + key~$\pubk{B}$. Bob sends data~$D$ encrypted with the symmetric key. + + Locate the description of the protocol in \url{blanchet.xhtml} in + the third derivation tree. +\end{note} + +\begin{mitreslide}{Blanchet Protocol in CPSA} +\begin{quote} +\begin{verbatim} +(defprotocol blanchet basic + (defrole init + (vars (a b name) (s skey) (d data)) + (trace + (send (enc (enc s (privk a)) (pubk b))) + (recv (enc d s)))) + (defrole resp + (vars (a b name) (s skey) (d data)) + (trace + (recv (enc (enc s (privk a)) (pubk b))) + (send (enc d s))))) +\end{verbatim} +\end{quote} +\end{mitreslide} + +\begin{note} + Locate the description of scenario in \url{blanchet.xhtml} in + Derivation Tree 9. +\end{note} + +\begin{mitreslide}{Blanchet Problem Statement} +\begin{itemize} +\item Analyze from the point-of-view of a full length responder +\item Assume $\privk{B}$ is uncompromised +\item Assume symmetric key~$S$ is freshly generated +\hfill\raisebox{0ex}[0ex]{\includegraphics{blanchet-5.mps}} +\end{itemize} +\begin{quote} +\begin{verbatim} +(defskeleton blanchet + (vars (a b name) (s skey) (d data)) + (defstrand resp 2 (a a) (b b) (s s) (d d)) + (non-orig (privk b)) + (uniq-orig s)) +\end{verbatim} +\end{quote} +\end{mitreslide} + +\begin{note} + {\cpsa} takes one step to find the shape associated with the scenario. + Locate the shape for the scenario in this derivation tree. +\end{note} + +\begin{mitreslide}{Blanchet Shape} +\begin{quote} +\begin{alltt} +(defskeleton blanchet + (vars (d data) (a b \textcolor{blue}{b-0} name) (s skey)) + (defstrand resp 2 (d d) (a a) (b b) (s s)) + (defstrand init 1 (a a) (b \textcolor{blue}{b-0}) (s s)) + (precedes ((1 0) (0 0))) + (non-orig (privk a) (privk b)) + (uniq-orig s) + ...) +\end{alltt} +\end{quote} +\end{mitreslide} + +\begin{note} + Observe that the responder role variable \texttt{b} maps to skeleton + variable \texttt{b}, but the initiator role variable \texttt{b} maps + to skeleton variable \texttt{b\_0}. The two strands disagree on + Bob's identity when agreement is expected. The dotted line in + Skeleton 10 indicates the message transmitted differs from the one sent. + + In the next slide, the traces show the implication of the + disagreement on the instantiations of variable \texttt{b}. +\end{note} + +\begin{mitreslide}{Blanchet Shape with Traces} +\begin{quote} +\begin{alltt} +(defskeleton blanchet + (vars (d data) (a b \textcolor{blue}{b-0} name) (s skey)) + (defstrand resp 2 (d d) (a a) (b b) (s s)) + (defstrand init 1 (a a) (b \textcolor{blue}{b-0}) (s s)) + ... + (traces + ((recv (enc (enc s (privk a)) (pubk b))) + (send (enc d s))) + ((send (enc (enc s (privk a)) (pubk \textcolor{blue}{b-0}))))) + ...) +\end{alltt} +\end{quote} +\end{mitreslide} + +\begin{mitreslide}{Blanchet Shape} +\begin{center} +\includegraphics{blanchet-4.mps} +\end{center} +\begin{quote} +\begin{alltt} +(defskeleton blanchet + (vars (d data) (a b \textcolor{blue}{b-0} name) (s skey)) + (defstrand resp 2 (d d) (a a) (b b) (s s)) + (defstrand init 1 (a a) (b \textcolor{blue}{b-0}) (s s)) + (precedes ((1 0) (0 0))) + ...) +\end{alltt} +\end{quote} +\end{mitreslide} + +\begin{note} + The operation field describes the authentication test that was + solved to produce the shape. Authentication tests are introduced in + \url{cpsaprimer.pdf}. +\end{note} + +\begin{mitreslide}{Blanchet Shape with Operation} +\begin{quote} +\begin{alltt} +(defskeleton blanchet + (vars (d data) (a b \textcolor{blue}{b-0} name) (s skey)) + (defstrand resp 2 (d d) (a a) (b b) (s s)) + (defstrand init 1 (a a) (b \textcolor{blue}{b-0}) (s s)) + ... + (operation + encryption-test ; Authentication test type + (added-strand init 1) ; Regular augmentation + (enc s (privk a)) ; Critical message + (0 0)) ; Test node + ...) +\end{alltt} +\end{quote} +\end{mitreslide} + +\begin{note} + The operation field explains why {\cpsa} produced strands that do + not agree on the identity of \texttt{b}. The critical message does + not refer to it, so there is nothing that forces agreement. + + Navigate to Derivation Tree 23 in \url{blanchet.xhtml}. +\end{note} + +\begin{mitreslide}{Corrected Blanchet Example Protocol} +$$\begin{array}{r@{{}\colon{}}l} +A\to B&\enc{\enc{S,B}{\privk{A}}}{\pubk{B}}\\ +B\to A&\enc{D}{S} +\end{array}$$ +\begin{center} +CPSA Style Roles \\[2ex] +\begin{tabular}{c} +Initiator ($\fn{init}$ role)\\[2ex] +\includegraphics{blanchet-2.mps} +\end{tabular}\hfil +\begin{tabular}{c} +Responder ($\fn{resp}$ role)\\[2ex] +\includegraphics{blanchet-3.mps} +\end{tabular}\\[3ex] +\end{center} +\end{mitreslide} + +\begin{mitreslide}{Corrected Blanchet Protocol in CPSA} +\begin{quote} +\begin{alltt} +(defprotocol blanchet-fixed basic + (defrole init + (vars (a b name) (s skey) (d data)) + (trace + (send (enc (enc s \textcolor{blue}{b} (privk a)) (pubk b))) + (recv (enc d s)))) + (defrole resp + (vars (a b name) (s skey) (d data)) + (trace + (recv (enc (enc s \textcolor{blue}{b} (privk a)) (pubk b))) + (send (enc d s))))) +\end{alltt} +\end{quote} +\end{mitreslide} + +\begin{note} + The corrected protocol ensures the critical message refers to + \texttt{b}. As a result, {\cpsa} infers the desired agreement. +\end{note} + +\begin{mitreslide}{Corrected Blanchet Shape} +\begin{quote} +\begin{alltt} +(defskeleton blanchet-fixed + (vars (d data) (a b name) (s skey)) + (defstrand resp 2 (d d) (a a) (b b) (s s)) + (defstrand init 1 (a a) (b b) (s s)) + (precedes ((1 0) (0 0))) + (non-orig (privk a) (privk b)) + (uniq-orig s) + (operation encryption-test + (added-strand init 1) + (enc s \textcolor{blue}{b} (privk a)) ; Critical message + (0 0)) + ...) +\end{alltt} +\end{quote} +\end{mitreslide} + +\end{document} diff --git a/doc/cpsaoverview.pdf b/doc/cpsaoverview.pdf Binary files a/doc/cpsaoverview.pdf and b/doc/cpsaoverview.pdf differ diff --git a/doc/cpsaprimer.pdf b/doc/cpsaprimer.pdf Binary files a/doc/cpsaprimer.pdf and b/doc/cpsaprimer.pdf differ diff --git a/doc/cpsaprimer.tex b/doc/cpsaprimer.tex --- a/doc/cpsaprimer.tex +++ b/doc/cpsaprimer.tex @@ -17,8 +17,16 @@ \maketitle \cpsacopying -%\tableofcontents +\tableofcontents +\listoffigures + +\listoftables + +\newpage + +\section{Introduction} + \begin{sloppypar} Analyzing a cryptographic protocol means finding out what security properties---essentially, authentication and secrecy properties---are @@ -643,16 +651,16 @@ \section{Authentication Tests}\label{sec:authentication tests} \index{nonce test}\index{encryption test} -Authentication tests guide the search for skeletons that refine one -with an unrealized node into ones in which it is realized. There are -two types of authentication tests, nonce and encryption tests. In -both cases, an unrealized node is selected, called the \index{test - node}\emph{test node.} A term carried by the inbound message at the -test node is identified as the \index{critical term}\emph{critical - term.} A critical term is one that occurs in a message -context, the construction of which cannot be explained by the regular -behavior in the current skeleton or by penetrator behavior. An -authentication test determines the additional regular behavior +Authentication tests~\cite{GuttmanThayer02} guide the search for +skeletons that refine one with an unrealized node into ones in which +it is realized. There are two types of authentication tests, nonce +and encryption tests. In both cases, an unrealized node is selected, +called the \index{test node}\emph{test node.} A term carried by the +inbound message at the test node is identified as the \index{critical + term}\emph{critical term.} A critical term is one that occurs in a +message context, the construction of which cannot be explained by the +regular behavior in the current skeleton or by penetrator behavior. +An authentication test determines the additional regular behavior required to refine a skeleton into ones in which the test node is realized. @@ -1186,11 +1194,11 @@ The \texttt{cpsalogic} program extracts a formula in the language of order-sorted first-order logic for each problem and its shapes from a -{\cpsa} run. The formula is called a shape analysis sentence. The -formula is satisfied in all realized skeletons when {\cpsa} finds all -the shapes for the problem. The details of formula extraction are -presented in Appendix~B of The {\cpsa} -Specification~\cite{cpsaspec09}. +{\cpsa} run. The formula is called a shape analysis +sentence~\cite{Ramsdell12}. The formula is satisfied in all realized +skeletons when {\cpsa} finds all the shapes for the problem. The +details of formula extraction are presented in Appendix~B of The +{\cpsa} Specification~\cite{cpsaspec09}. \section{Annotations}\label{sec:annotations} diff --git a/doc/cpsaspec.pdf b/doc/cpsaspec.pdf Binary files a/doc/cpsaspec.pdf and b/doc/cpsaspec.pdf differ diff --git a/doc/cpsauser.html b/doc/cpsauser.html --- a/doc/cpsauser.html +++ b/doc/cpsauser.html @@ -80,10 +80,11 @@ $ firefox -remote "openFile(`pwd`/prob_shapes.xhtml)" -

The distribution comes with the file cpsa.mk -for inclusion into your makefile. A sample makefile follows. If you -cut-and-paste from a browser window, be sure to convert the leading spaces in -the last line to a tab character.

+

The distribution comes with the +file cpsa.mk for inclusion into your +makefile. A sample makefile follows. If you cut-and-paste from a +browser window, be sure to convert the leading spaces in the last line +into a tab character.

CPSAFLAGS = +RTS -M512m -RTS
@@ -99,6 +100,14 @@
         -rm *.txt *.xhtml
+

The CPSA program + is Emacs friendly. + If you run the above makefile via "M-x + compile", the results will be displayed in a buffer in + Compilation Mode. The command "C-x `" will visit + the locus of the next error message or match (next-error) + in your CPSA input file.

+

For platforms without GNU make, the Haskell program Make.hs can be loaded into a Haskell interpreter and perform a similar function. Users are expected to copy the makefile or the @@ -167,7 +176,7 @@ | (pubk STRING ID) | (privk STRING ID) -

The form (cat a b c d e) is sugar for (cat a (cat +

The form (cat a b c d e) is expands to (cat a (cat b (cat c (cat d e)))).

A term in the Basic Crypto Algebra is an atom if it is variable of a sort @@ -584,6 +593,7 @@ -o FILE --output=FILE output FILE -m INT --margin=INT set output margin (default 72) -i --infix output uses infix notation + -j --json output uses JSON notation -h --help show help message -v --version show version number diff --git a/doc/index.html b/doc/index.html --- a/doc/index.html +++ b/doc/index.html @@ -9,9 +9,12 @@ -

[CPSA User Guide] [CPSA -Primer] [CPSA Overview]

+

[CPSA User Guide] +[CPSA Primer] +[CPSA Overview] +[CPSA Introductory Slides]

+

CPSA

The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to enumerate all @@ -20,33 +23,106 @@ finitely many, indeed very few shapes. Authentication and secrecy properties are easy to determine from them, as are attacks and anomalies.

-

CPSA comes with a user guide, a primer, and an overview. To make effective -use of CPSA, new users should read the primer.

+

CPSA comes with a user guide, a primer, an overview, and some slides. + The user guide provides usage information for each program in the + CPSA package. The primer provides an English language description + of the CPSA algorithm and is the primary user documentation. The + overview is another attack at user documentation and includes an + introduction to the Rely-Guarantee Method of demonstrating that a + protocol achieves its security goals. This is an advanced technique + beginners should feel free to ignore.

-

Start using CPSA by analyzing the protocols that come with this document. -Copy the contents of this directory to a place that allows it to be modified. -In a Unix shell, type:

+

At this point, new users should open the + introductory slides and start + using CPSA by analyzing the protocols that come with this document. + Copy the contents of this directory to a place that allows it to be + modified. In a Unix shell, type:

$ echo build | ghci Make.hs
-

In Windows, you can click on Make.hs and type build. The -CPSA User Guide describes a better way to analyze -protocols when GNU Make is available.

+

In Windows, click on Make.hs and type build at + the GHCi + prompt *Make>. The CPSA User + Guide describes a better way to analyze protocols when GNU Make + is available.

After running the analysis, you will note files with the extension .xhtml. These are XHTML/SVG compound documents that can be viewed by -standards compliant browsers such as Firefox, Chrome, or Safari.

+standards compliant browsers such as Firefox, Chrome, Safari, and +later versions of Internet Explorer. See the section +on visualization in the user +guide for help interpreting these documents.

-

New users should study CPSA's analysis of the following protocols in order, -Needham-Schroeder (ns.xhtml), Woo-Lam (woolam.xhtml), Yahalom -(yahalom.xhtml), ffgg (ffgg.xhtml), and finally Otway-Rees -(or.xhtml). When studying the full output, simultaneously display the -extracted shapes. The shapes file has an extension of _shapes.xhtml.

+

New users should study CPSA's analysis of the following protocols + in order, Blanchet (blanchet.xhtml), Needham-Schroeder + (ns.xhtml), Woo-Lam (woolam.xhtml), Yahalom + (yahalom.xhtml), ffgg (ffgg.xhtml), and finally + Otway-Rees (or.xhtml). When studying the full output, + simultaneously display the extracted shapes. The shapes file has an + extension of _shapes.xhtml.

+

To make effective use of CPSA, new users should scan the + user guide to get a flavor of its + contents, and then read the primer. + The remainder of this document contains some usage tips to be read + after running CPSA and learning to understand its output.

+ +

Tips

+

Choose a small, simple protocol for your first analysis task. When analyzing complex protocols, analyze small parts of the protocol first, and then enrich the description of the problem.

+ +

The source distribution contains additional programs and a test + suite with many examples. The README in the top-level directory of + the source distribution contains the installation instructions and + is essential reading for its effective use. Serious users should + favor the source distribution.

+ +

Authentication tests guide the search for new skeletons in CPSA. + The authentication test solved at each step of the search is + described by the operation form in CPSA output. When CPSA + generates unexpected output, find the first skeleton in the + derivation tree that exhibits the problem and read + the operation form to find out what happened. + Authentication tests are introduced in + the primer and described in full + detail in the The CPSA + Specification.

+ +

An origination assumption + (non-orig, pen-non-orig, and unig-orig), + can be specified in a role or in a skeleton. Be sure to read the + advice in the primer on the proper + placement of origination assumptions.

+ +

Variables of sort message unify with any message. See Otway-Rees + (or.xhtml) for an example of the use of variables of this + sort.

+ +

A quoted string is a constant of sort message and is called a tag. + Tags can be used to distinguish messages that have similar + structure in the case where the implementation of the protocol + contains protections against message conflation.

+ +

Lisp-like macros in cpsa input can be used to replace + multiple occurrences of a message with one named definition of it. + Macros are described in the primer.

+ +

When the cpsagraph program is given the --zoom + option, it produces diagrams that scale. This is useful when + viewing large diagrams.

+ +

When the cpsapp program is given the --json + option, it translates S-expressions into JavaScript Object + Notation.

+ +

The specification describes the CPSA + algorithm as a term reduction system. + The design describes implementation + choices made and should be read when viewing the source code.

+ diff --git a/doc/macros.tex b/doc/macros.tex --- a/doc/macros.tex +++ b/doc/macros.tex @@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}} -\newcommand{\version}{2.2.11} +\newcommand{\version}{2.2.12} \newcommand{\cpsacopying}{\begingroup \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The MITRE Corporation. Permission to copy without fee all or part of diff --git a/doc/mitrelogo.mp b/doc/mitrelogo.mp new file mode 100644 --- /dev/null +++ b/doc/mitrelogo.mp @@ -0,0 +1,182 @@ +filenametemplate "%j-%c.mps"; + +% Original comment in the METAFONT version of the MITRE logo. + +%% The MITRE logo version 1.1 released 11/16/89. + +%% Created by Richard Shaeff --- 1981 +%% Shaeff Design Inc, Needham, MA +%% +%% Programmed in METAFONT by John D. Ramsdell --- November 1989 +%% The MITRE Corporation, Bedford, MA +%% Copyright 1989 by The MITRE Corporation. + +%% Richard Shaeff's original design was done by creating an +%% outline. Therefore, this METAFONT version generates letters +%% by filling an outlined region. + +%% The program expects ht# and only ht# to be defined in a +%% parameter file. All other parameters are derived from this +%% one. This is in conformance with the MITRE policy which states +%% that the logo may be changed only by linearly scaling all of +%% the logo's dimensions. + +% The single parameter in METAPOST is h. +h=15pt; + +%% Note: +%% Measurements from the original design and are in inches. +%% The height of the logo is 4.25 inches and that height is +%% used to scale all dimensions. +%% + +%% MITRE blue is Pantone Matching System (PMS) 293 Blue, with an RGB +%% value of (0, 81, 186). + +prologue:=1; + +I_w = 0.87500/4.25h; % I width. (7/8in) +T_bar_h = 0.78125/4.25h; % T bar height. (25/32in) +T_lft_w = 1.03125/4.25h; % Left T bar. (1 1/32in) +T_rt_w = 1.00000/4.25h; % Right T bar. (1in) +E_gap_h = 0.93750/4.25h; % Upper E gap. (15/16in) +E_bar_shrink_h = 0.06250/4.25h; % Mid bar shrink. (1/16in) +E_bar_w = 1.56250/4.25h; % E bar width. (1 9/16in) +R_tail_a = 125; % R tail angle. +M_vee_h = 1.62500/4.25h; % M vee height. (1 5/8in) +M_vee_a = 70; % M vee angle. +M_edge_a = 100; % M edge angle. +M_w = 5.25000/4.25h; % M width. (5 1/4in) +skip_w = 0.12500/4.25h; % Distance between T and R. + % (1/8in) +s = max(1, round(skip_w)); % Rounded interletter space. +color mitreblue; +mitreblue = (0,70/255,174/255); % MITRE blue PMS 293 Blue + +def draw_M(expr o) = + begingroup + save x, y; + w = M_w + skip_w; + x1 = o; + y2 = y3 = y5 = y6 = h; + y4 = h - y12 = h - y9 = M_vee_h; % The vee heights are the same. + y1 = y13 = y11 = y10 = y8 = y7 = 0; + + x13 = x1 + I_w; + x7 = w - max(1, round(.5skip_w)); + x8 = x7 - I_w; + x3 - x2 = x6 - x5; % Top edges widths are the same. + x5 - x2 = x10 - x1; % A strange fact---measure it! + + z6 = z7 + whatever * dir M_edge_a; % The right side has all nice + z9 = z8 + whatever * dir M_edge_a; % and neat angles defining it. + z10 = z9 + whatever * dir M_vee_a; + z4 = (-I_w, 0) + whatever[z10,z9]; % Width of right diagonal is I_w. + z5 = z4 + whatever * dir M_vee_a; + z12 = z13 + whatever * (z2 - z1); + z11 = z12 + whatever * (z3 - z4); + % The width of the left diagonal is only approximately I_w. + % The following is only "almost" true. + % z4 = (I_w, 0) + whatever[z11,z12]; + + fill z1--z2--z3--z4--z5--z6--z7 + & z7--z8--z9--z10--z11--z12--z13--cycle withcolor mitreblue; + w + endgroup; +enddef; + +def draw_I(expr o) = + begingroup + save x, y; + y2 = y3 = h; + y1 = y4 = 0; + + x1 = x2 = o; + x3 = x4 = o + round(I_w); + + fill z1--z2--z3--z4--cycle withcolor mitreblue; + x3 + s + endgroup; +enddef; + +def draw_T(expr o) = + begingroup; + save x, y; + y4 = y5 = h; + y3 = y2 = y7 = y6 = h - T_bar_h; + y1 = y8 = 0; + + x3 = x4 = o; + x2 = x1 = o + round(T_lft_w); + x7 = x8 = o + round(T_lft_w + I_w); + x6 = x5 = o + round(T_lft_w + I_w + T_rt_w); + + fill z1--z2--z3--z4--z5--z6--z7--z8--cycle withcolor mitreblue; + x6 + s + endgroup; +enddef; + +def draw_R(expr o) = + begingroup; + save x, y; + y2 = y3 = h; + y10 = y11 = h - T_bar_h; % y10, y8, y5, y3 must be integers. + y9 = y4 = y10 - .5E_gap_h; % They help determine the position + y7 = y15 = y8 = y10 - E_gap_h; % of horizontal tangents to curves. + y6 = y5 = y7 - (T_bar_h - E_bar_shrink_h); + y1 = y12 = y13 = y16 = 0; + + x1 = x2 = o; + x11 = x12 = o + round(I_w); % The space in the "R" must be the + x7 = x6 = x14 = x11 + s; % same as the interletter space. + x3 = x10 = x8 = x5 = o + I_w + y7 - y 14; % The location of the tail + x13 = x3 + .5E_gap_h; % (x13) must not be rounded or + % METAFONT cannot solve the equations. + z14 = z13 + whatever * dir R_tail_a; + z16 = (x13+I_w+skip_w, skip_w) + whatever * dir R_tail_a; + z15 = z16 + whatever * dir R_tail_a; + + x9 = round(x13); % x4 and x9 determine vertical tangents + x4 = round(x13 + I_w); % so they must be integers. + + fill z1--z2--z3 + & z3{z3-z2}..z4{z5-z3}..{z6-z5}z5 + & z5--z6--z7--z8 + & z8{z8-z7}..z9{z10-z8}..{z11-z10}z10 + & z10--z11--z12--cycle withcolor mitreblue; + + % "R" Tail + fill z13--z14--z7--z15--z16--cycle withcolor mitreblue; + x4 + s + endgroup; +enddef; + +def draw_E(expr o) = + begingroup; + save x, y; + y2 = y3 = h; + y5 = y4 = h - T_bar_h; + y6 = y7 = y5 - E_gap_h; + y9 = y8 = y6 - (T_bar_h - E_bar_shrink_h); + % Notice that the lower bar is bigger than the upper one. + y10 = y11 = T_bar_h + E_bar_shrink_h; + y1 = y12 = 0; + + x1 = x2 = o; + x5 = x6 = x9 = x10 = o + round(I_w); + x3 = x4 = x7 = x8 = x11 = x12 = o + round(I_w + E_bar_w); + + fill z1--z2--z3--z4--z5--z6--z7--z8 + & z8--z9--z10--z11--z12--cycle withcolor mitreblue; + x3 + max(1, round(.5skip_w)) + endgroup; +enddef; + +beginfig(0); + x1 = draw_M(0); + x2 = draw_I(x1); + x3 = draw_T(x2); + x4 = draw_R(x3); + x5 = draw_E(x4); +endfig; +bye; diff --git a/doc/mitreslides.sty b/doc/mitreslides.sty new file mode 100644 --- /dev/null +++ b/doc/mitreslides.sty @@ -0,0 +1,97 @@ +% mitreslides package for use with the slides class in LaTeX. + +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{mitreslides}[2005/02/21] +% +% John D. Ramsdell +% +% Example file: +% +% \documentclass[landscape]{slides} +% \usepackage{mitreslides} +% \renewcommand{\footercomment}{A Title} +% \begin{document} +% ... +% \end{document} +% +% Defines environments: titleslide, mitreslide, and mitreoverlay +% +% The "slide" pagestyle is also defined. It prints the slide +% number, and the MITRE logo in the lower right corner. +% +% titleslide example: +% +% \begin{titleslide}{A Briefing\\of Major Importance} +% R. J. Drofnats +% +% 30 Feb 93 +% \end{titleslide} +% +% The first argument is optional and is passed to +% the slide environment and is used for color slides. +% The second argument is the briefing title. +% +% mitreslide example: +% +% \begin{mitreslide}{A Slide\\Title} +% ...slide contents... +% \end{mitreslide} +% +% The first argument is optional and is passed to +% the slide environment and is used for color slides. +% The second argument is the slide title. +% +% Set the footer comment with footercomment. +% The options are, date, nopagenumbers, and marks. +% +% Initial code +\RequirePackage{ifthen} +\newboolean{date} % Show current date +\newboolean{nopagenums} % Omit page numbers +\newboolean{marks} % Show top marks +% Declaration of options +\DeclareOption{date}{\setboolean{date}{true}} +\DeclareOption{nopagenums}{\setboolean{nopagenums}{true}} +\DeclareOption{marks}{\setboolean{marks}{true}} +% +\ProcessOptions +\RequirePackage{graphicx} +% ----------- main code ---------------- +% Footer comment is empty by default. +\newcommand{\footercomment}{} + +\ifthenelse{\boolean{date}}{% +\newcommand{\show@date}{\the\year{/}\the\month{/}\the\day}% +}{% +\newcommand{\show@date}{}% +} + +\ifthenelse{\boolean{nopagenums}}{% +\newcommand{\show@slidenum}{\phantom{\theslide}}% +}{% +\newcommand{\show@slidenum}{\theslide}% +} + +\ifthenelse{\boolean{marks}}{% +\newcommand{\show@mark}{+}% +}{% +\newcommand{\show@mark}{\phantom{+}}% +} +% +% slide page style -- MITRE logo goes flush right +\def\ps@slide{% +\def\@oddfoot{{\tiny\show@slidenum\qquad\show@date\quad\footercomment}% +\hfil\includegraphics{mitrelogo-0.mps}} +\def\@oddhead{\show@mark\hfil\show@mark} +\def\@evenfoot{\@oddfoot} +\def\@evenhead{\@oddhead}} +% +% \begin{mitreslide}[COLORS]{TITLE} ... \end{mitreslide} +\newenvironment{mitreslide}[2][]% Built on the slide environment. +{\begin{slide}{#1}{\noindent\raggedright\Large#2\par}}% +{\vfill\end{slide}} +% +% \begin{titleslide}[COLORS]{TITLE} ... \end{titleslide} +\newenvironment{titleslide}[2][]% +{\begin{slide}{#1}\begin{center}{{\Large#2\par}}}% +{\end{center}\end{slide}} diff --git a/doc/readme.html b/doc/readme.html new file mode 100644 --- /dev/null +++ b/doc/readme.html @@ -0,0 +1,13 @@ + + + + + + + CPSA + + + +

Start here.

+ diff --git a/setup.bat b/setup.bat --- a/setup.bat +++ b/setup.bat @@ -1,3 +1,8 @@ -runghc Setup.hs configure -runghc Setup.hs build -runghc Setup.hs install +@setlocal enableextensions +@cd /d "%~dp0" +runghc Setup.hs configure +runghc Setup.hs build + +runghc Setup.hs install + +pause diff --git a/src/CPSA/Lib/Pretty.hs b/src/CPSA/Lib/Pretty.hs --- a/src/CPSA/Lib/Pretty.hs +++ b/src/CPSA/Lib/Pretty.hs @@ -58,11 +58,13 @@ brk = Brk -- Indentation blocks +-- If the line is too long, not all breaks must be used blo :: Int -> [Pretty] -> Pretty blo indent es = Blo es indent (len es 0) -- Indentation groups +-- If the line is too long, all breaks are used grp :: Int -> [Pretty] -> Pretty grp indent es = Grp es indent (len es 0) diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs --- a/src/CPSA/Lib/Strand.hs +++ b/src/CPSA/Lib/Strand.hs @@ -11,7 +11,7 @@ firstSkeleton, Pair, Preskel, gen, protocol, insts, orderings, pov, knon, kpnon, kunique, korig, kcomment, nstrands, kvars, kterms, uniqOrig, preskelWellFormed, verbosePreskelWellFormed, - Strand, GraphStrand, inst, nodes, Vertex, GraphNode, preds, event, + Strand, inst, nodes, Vertex, preds, event, graphNode, strands, vertex, Gist, gist, contract, augment, inheritRnon, inheritRpnon, inheritRunique, addListener, Cause (..), Direction (..), Method (..), Operation (..), operation, diff --git a/src/CPSA/Pretty/Main.hs b/src/CPSA/Pretty/Main.hs --- a/src/CPSA/Pretty/Main.hs +++ b/src/CPSA/Pretty/Main.hs @@ -19,6 +19,7 @@ data Params = Params { file :: Maybe FilePath, -- Nothing specifies standard output prefix :: Bool, -- Use prefix notation? + json :: Bool, -- Use JSON notation? margin :: Int } -- Output line length deriving Show @@ -30,7 +31,8 @@ do (p, params) <- start options interp h <- outputHandle $ file params - let printer = if prefix params then pp else printItem + let printer = if json params then pjson + else if prefix params then pp else printItem go (writeCpsaLn (printer (margin params) indent) h) p hClose h @@ -61,6 +63,7 @@ | Info -- Version information | Margin String -- Output line length | Infix -- Select output notation + | Json -- Select output format | Output String -- Output file name deriving Show @@ -73,6 +76,7 @@ Option ['m'] ["margin"] (ReqArg Margin "INT") ("set output margin (default " ++ show defaultMargin ++ ")"), Option ['i'] ["infix"] (NoArg Infix) "output uses infix notation", + Option ['j'] ["json"] (NoArg Json) "output uses JSON notation", Option ['h'] ["help"] (NoArg Help) "show help message", Option ['v'] ["version"] (NoArg Info) "show version number" ] @@ -81,6 +85,7 @@ interp flags = loop flags (Params { file = Nothing, -- By default, no output file prefix = True, + json = False, margin = defaultMargin }) where loop [] params = return params @@ -88,7 +93,19 @@ | file params == Nothing = loop flags $ params { file = Just name } loop (Infix : flags) params = - loop flags $ params { prefix = False } + if json params then + do + msg <- usage options ["Bad option combination\n"] + abort msg + else + loop flags $ params { prefix = False } + loop (Json : flags) params = + if not (prefix params) then + do + msg <- usage options ["Bad option combination\n"] + abort msg + else + loop flags $ params { json = True } loop (Margin value : flags) params = case readDec value of [(margin, "")] -> @@ -107,3 +124,21 @@ do -- Show help then exit with failure msg <- usage options ["Bad option combination\n"] abort msg + +-- A simple JSON pretty printer using only block style breaks. +-- A quoted string is distinguished from a symbol by +-- surrounding the string with double quotes. +pjson :: Int -> Int -> SExpr a -> String +pjson margin indent sexpr = + pr margin (block indent sexpr) "" + +block :: Int -> SExpr a -> Pretty +block _ (S _ s) = str (showQuoted s "") +block _ (Q _ s) = str (showString "\"\\\"" (showString s "\\\"\"")) +block _ (N _ n) = str (show n) +block _ (L _ []) = str "[]" +block indent (L _ (x:xs)) = + loop [block indent x, str "["] xs + where + loop es [] = blo indent (reverse (str "]" : es)) + loop es (x:xs) = loop (block indent x : brk 1 : str ",": es) xs diff --git a/src/cpsa.pl b/src/cpsa.pl --- a/src/cpsa.pl +++ b/src/cpsa.pl @@ -112,9 +112,9 @@ %% Top ::= c(Comment) -- Comment %% | h(Name, Alist) -- Herald %% | p(Name, Alg, Roles) -- Defprotocol -%% | k(Prot, Decls, Strands, Precedes, Nons, Uniqs). +%% | k(Prot, Decls, Strands, Precedes, Nons, Pens, Uniqs). %% -- Defskeleton -%% Role ::= r(Name, Decls, Trace, Nons, Uniqs). +%% Role ::= r(Name, Decls, Trace, Nons, Pens, Uniqs). %% -- Defrole %% Decl ::= d(Sort, Vars). %% @@ -124,9 +124,11 @@ %% %% Nons ::= [Term]. %% +%% Pens ::= [Term]. +%% %% Uniqs ::= [Term]. %% -%% Strand ::= s(RoleName, Height, Map). +%% Strand ::= s(RoleName, Height, Map) | l(Term). %% %% Height ::= Int. %% @@ -142,7 +144,7 @@ %% %% Var ::= Atom. %% -%% Tag ::= String. +%% Tag ::= String as a Prolog atom. sexpr_to_cpsa([comment|X], c(X)). sexpr_to_cpsa([herald, Name|Alist], h(Name, Alist)). @@ -151,7 +153,7 @@ atom(Name), atom(Alg), sexpr_to_roles(Rest, Roles). sexpr_to_cpsa([defskeleton, Prot, [vars|Vars]|Rest], - k(Prot, Decls, Strands, Precedes, Nons, Uniqs)) :- + k(Prot, Decls, Strands, Precedes, Nons, Pens, Uniqs)) :- atom(Prot), decls(Vars, Decls), sexpr_to_strands(Rest, Strands, Alist), @@ -159,6 +161,8 @@ edges(Values, Precedes), lookup('non-orig', Alist, Snons), sexprs_to_terms(Snons, Nons), + lookup('pen-non-orig', Alist, Spens), + sexprs_to_terms(Spens, Pens), lookup('uniq-orig', Alist, Suniqs), sexprs_to_terms(Suniqs, Uniqs). @@ -169,11 +173,13 @@ sexpr_to_roles(_, []). sexpr_to_role([Name, [vars|Vars], [trace|Strace]|Alist], - r(Name, Decls, Trace, Nons, Uniqs)) :- + r(Name, Decls, Trace, Nons, Pens, Uniqs)) :- decls(Vars, Decls), sexprs_to_trace(Strace, Trace), lookup('non-orig', Alist, Snons), sexprs_to_terms(Snons, Nons), + lookup('pen-non-orig', Alist, Spens), + sexprs_to_terms(Spens, Pens), lookup('uniq-orig', Alist, Suniqs), sexprs_to_terms(Suniqs, Uniqs). @@ -192,8 +198,6 @@ sexpr_to_term(Term, Term) :- atom(Term). -sexpr_to_term(Term, Term) :- - string(Term). sexpr_to_term([cat, Sterm], Term) :- sexpr_to_term(Sterm, Term). sexpr_to_term([cat, Sterm1, Sterm2|Sterms], cat(Term1, Term)) :- @@ -289,18 +293,18 @@ cpsa_to_sexpr(h(Name, Alist), [herald, Name|Alist]). cpsa_to_sexpr(p(Name, Alg, Roles), [defprotocol, Name, Alg|Rest]) :- roles_to_sexprs(Roles, Rest). -cpsa_to_sexpr(k(Prot, Decls, Strands, Precedes, Nons, Uniqs), +cpsa_to_sexpr(k(Prot, Decls, Strands, Precedes, Nons, Pens, Uniqs), [defskeleton, Prot, [vars|Vars]|Rest]) :- decls(Vars, Decls), - preds(Precedes, Nons, Uniqs, Alist), + preds(Precedes, Nons, Pens, Uniqs, Alist), strands_to_sexprs(Strands, Alist, Rest). -preds([], Nons, Uniqs, Alist) :- +preds([], Nons, Pens, Uniqs, Alist) :- !, - origs(Nons, Uniqs, Alist). -preds(Precedes, Nons, Uniqs, [[precedes|Sexprs]|Alist]) :- + origs(Nons, Pens, Uniqs, Alist). +preds(Precedes, Nons, Pens, Uniqs, [[precedes|Sexprs]|Alist]) :- edges(Sexprs, Precedes), - origs(Nons, Uniqs, Alist). + origs(Nons, Pens, Uniqs, Alist). strands_to_sexprs([], Alist, Alist). strands_to_sexprs([Strand|Strands], Alist, [Sexpr|Sexprs]) :- @@ -322,11 +326,11 @@ role_to_sexpr(Role, Sexpr), roles_to_sexprs(Roles, Sexprs). -role_to_sexpr(r(Name, Decls, Trace, Nons, Uniqs), +role_to_sexpr(r(Name, Decls, Trace, Nons, Pens, Uniqs), [defrole, Name, [vars|Vars], [trace|Strace]|Alist]) :- decls(Vars, Decls), traces_to_sexprs(Trace, Strace), - origs(Nons, Uniqs, Alist). + origs(Nons, Pens, Uniqs, Alist). traces_to_sexprs([], []). traces_to_sexprs([send(Term)|Trace], [[send, Sterm]|Straces]) :- @@ -336,12 +340,19 @@ term_to_sexpr(Term, Sterm), traces_to_sexprs(Trace, Straces). -origs([], Uniqs, Alist) :- +origs([], Pens, Uniqs, Alist) :- !, - uniq_origs(Uniqs, Alist). -origs(Nons, Uniqs, [['non-orig'|Snons]|Alist]) :- + pen_uniq_origs(Pens, Uniqs, Alist). +origs(Nons, Pens, Uniqs, [['non-orig'|Snons]|Alist]) :- terms_to_sexprs(Nons, Snons), + pen_uniq_origs(Pens, Uniqs, Alist). + +pen_uniq_origs([], Uniqs, Alist) :- + !, uniq_origs(Uniqs, Alist). +pen_uniq_origs(Pens, Uniqs, [['pen-non-orig'|Spens]|Alist]) :- + terms_to_sexprs(Pens, Spens), + uniq_origs(Uniqs, Alist). uniq_origs([], []) :- !. uniq_origs(Uniqs, [['uniq-orig'|Suniqs]]) :- @@ -354,8 +365,6 @@ term_to_sexpr(Term, Term) :- atom(Term). -term_to_sexpr(Term, Term) :- - string(Term). term_to_sexpr(cat(Term1, Term2), [cat, Sterm1|Sterms]) :- term_to_sexpr(Term1, Sterm1), term_to_sexprs(Term2, Sterms). diff --git a/src/cpsa2svg b/src/cpsa2svg --- a/src/cpsa2svg +++ b/src/cpsa2svg @@ -1,8 +1,8 @@ #! /bin/sh -# Generates an SVG diagram from CPSA preskeletons +# Generates an SVG diagram from CPSA skeletons -# This program converts the preskeletons in the input into an SVG +# This program converts the skeletons in the input into an SVG # diagram using Scheme and the GraphVis program dot. Terms are # displayed as tooltips in the diagram. @@ -51,7 +51,7 @@ done SCRIPT=' -;;; Converts the preskeletons in the input into GraphViz dot format. +;;; Converts the skeletons in the input into GraphViz dot format. ;;; Terms are displayed as tooltips, so this output is usually ;;; converted to SVG. @@ -66,7 +66,7 @@ (let ((input (get))) ; Read input (show-all (car input) (cdr input)))) ; Process in -;;; Get the list of preskeletons and the protocols as an alist +;;; Get the list of skeletons and the protocols as an alist (define (get) (let loop ((prots '\''()) (skels '\''())) (let ((x (read))) diff --git a/src/cpsaops.scm b/src/cpsaops.scm --- a/src/cpsaops.scm +++ b/src/cpsaops.scm @@ -3,7 +3,7 @@ !# ;;; For an R6RS script, add an import statement. -;; This program simply extracts the operation form in a preskeleton +;; This program simply extracts the operation form in a skeleton ;; and prints it. (define (consume form) (let ((op (skel-assq 'operation form))) diff --git a/src/cpsaperm.scm b/src/cpsaperm.scm new file mode 100644 --- /dev/null +++ b/src/cpsaperm.scm @@ -0,0 +1,193 @@ +#!/usr/bin/guile \ +-e main -s +!# +(use-modules (ice-9 pretty-print)) +;;; For an R6RS script, add an import statement. + +;;; Synopsis: renumber strands in skeletons + +;;; A permutation of length n is represented as a list of natural +;;; numbers that contains all the numbers less than n. + +;;; This program renumbers all the skeletons in a file that have the +;;; same number of strands as is the length of the permutation. +;;; Everything else is passed through unchanged. + +;;; Usage: cpsaperm [-h] [-o FILE] FILE INT... +;;; where INT... specifies a permutation. +;;; Use - in place of FILE for the standard port + +;;; Example: cpsaperm -o out.txt in.txt 1 0 +;;; Swaps the strands in skeletons with two strands. + +;;; This program does not check that the given permutation is in fact +;;; a valid permutation, so be sure to check your output carefully. +;;; Make sure your permutation has no repeats. + +;;; John D. Ramsdell -- October 2012 + +;;; Create a function that applies a permutation to a form +(define (apply-perm perm) + (let ((n (length perm))) + (lambda (form) + (let ((skel (parse-skel form))) + (cond ((not skel) form) ; Ignore non-skeletons + ;; Ignore skeletons with the wrong number of strands + ((not (= n (length (skel-strands skel)))) form) + (else + (let ((skel (apply-perm-to-skel perm skel))) + `(defskeleton + ,(skel-protocol skel) + ,(skel-vars skel) + ,@(append (skel-strands skel) (skel-alist skel)))))))))) + +;;; A skeleton is represented as list with the following fields. + +(define (skel-protocol skel) (car skel)) +(define (skel-vars skel) (cadr skel)) +(define (skel-strands skel) (caddr skel)) +(define (skel-alist skel) (cdddr skel)) +(define (make-skel protocol vars strands alist) + (cons protocol (cons vars (cons strands alist)))) + +;;; Creates a skeleton structure or returns #f on error. +(define (parse-skel form) + (and (skel? form) + (let loop ((body (cdddr form)) (strands '())) + (cond ((null? body) + (make-skel (cadr form) (caddr form) + (reverse strands) body)) + ((or (eq? 'defstrand (caar body)) + (eq? 'deflistener (caar body))) + (loop (cdr body) (cons (car body) strands))) + (else + (make-skel (cadr form) (caddr form) + (reverse strands) body)))))) + +;;; Is form a defskeleton + +(define (skel? form) + (and (list? form) + (<= 4 (length form)) + (eq? 'defskeleton (car form)) + (alist? (cddr form)))) + +(define (alist? form) ; Is form a list of pairs? + (or (null? form) + (and (pair? form) + (pair? (car form)) + (alist? (cdr form))))) + +;;; To apply a permutation to a skeleton, permute the strands and the +;;; node orderings. +(define (apply-perm-to-skel perm skel) + (let ((strands (skel-strands skel))) + (make-skel + (skel-protocol skel) + (skel-vars skel) + (map (lambda (index) + (list-ref strands index)) + perm) + (map (apply-perm-to-alist perm) (skel-alist skel))))) + +;;; Apply a permutation to the node orderings +(define (apply-perm-to-alist perm) + (lambda (entry) + (if (eq? (car entry) 'precedes) + (cons (car entry) + (map (apply-perm-to-pair perm) (cdr entry))) + entry))) + +(define (apply-perm-to-pair perm) + (lambda (ordered-pair) + (if (and (list? ordered-pair) (= 2 (length ordered-pair))) + (list (apply-perm-to-node perm (car ordered-pair)) + (apply-perm-to-node perm (cadr ordered-pair))) + ordered-pair))) + +(define (apply-perm-to-node perm node) + (if (and (list? node) (= 2 (length node))) + (list (list-ref perm (car node)) (cadr node)) + node)) + +;;; The main driver loop and command-line processing + +;;; The main loop calls the transformer on each S-expression read from +;;; the current input. + +(define (filter perm) + (let ((transformer (apply-perm perm))) + (lambda () + (do ((form (read) (read))) + ((eof-object? form)) + (pretty-print (transformer form)))))) + +;;; A file description is #f for the standard port, or a file name +;;; that is a non-empty string that does not start with hyphen. + +(define (file-description? file) + (or (not file) + (and (> (string-length file) 0) + (not (char=? #\- (string-ref file 0)))))) + +;;; After command-line processing, this routine opens files as needed. + +(define (go input output perm) + (let ((thunk (filter perm))) + (cond ((not (file-description? input)) + (display-error "bad input file name")) + ((not (file-description? output)) + (display-error "bad output file name")) + (input + (with-input-from-file input + (lambda () + (if output + (with-output-to-file output thunk) + (thunk))))) + (output + (with-output-to-file output thunk)) + (else + (thunk))))) + +;;; Parse command-line arguments and pass the result to the go function. + +(define (main args) + (let loop ((args (cdr args)) (output #f)) + (cond ((null? args) ; No input file specified + (display-error "bad args")) + ((string=? (car args) "-h") + (display-help)) ; Print help message + ((string=? (car args) "-o") + (if (null? (cdr args)) + (display-error "bad args") + (loop (cddr args) (cadr args)))) ; Found an output file + ((string=? (car args) "-") + (check-perm #f output (cdr args))) + (else ; Found input file + (check-perm (car args) output (cdr args)))))) + +;;; Make sure a permutation is a list of non-negative integers less +;;; that the length of the permutation. +(define (check-perm input output args) + (let ((n (length args))) + (let loop ((args args) (perm '())) + (if (null? args) + (go input output (reverse perm)) + (let ((index (string->number (car args)))) + (if (and (integer? index) + (not (negative? index)) + (< index n)) + (loop (cdr args) (cons index perm)) + (display-error "bad permutation"))))))) + +(define (display-help) + (display-error "cpsaperm [-h] [-o FILE] FILE INT...") + (display-error "where INT... specifies a permutation.") + (display-error "Use - as FILE for the standard input.")) + +(define (display-error obj) + (display obj (current-error-port)) + (newline (current-error-port))) + +;;; For an R6RS script, add the following: +;;; (main (command-line)) diff --git a/src/perm.pl b/src/perm.pl new file mode 100644 --- /dev/null +++ b/src/perm.pl @@ -0,0 +1,69 @@ +% -*- mode: prolog -*- + +%% Renumber strands in skeletons + +%% Known to work in SWI-Prolog, but not with GNU Prolog. + +%% Copyright (c) 2012 The MITRE Corporation +%% +%% This program is free software: you can redistribute it and/or +%% modify it under the terms of the BSD License as published by the +%% University of California. + +:- module(perm, [cpsa_permute/3]). + +:- use_module(cpsa). + +%% PERMUTE STRANDS + +%% A permutation of length n is represented as a list of natural +%% numbers that contains all the numbers less than n. + +%% This program renumbers all the skeletons in a file that have the +%% same number of strands as is the length of the permutation. +%% Everything else is passed through unchanged. + +%% For example, to swap the strands in skeletons with two strands in +%% in.txt and put the output into out.txt, type: +%% +%% perm: cpsa_permute([1,0], 'in.txt', 'out.txt'). + +%% This program does not check that the given permutation is in fact a +%% valid permutation, so be sure to check your output carefully. + +cpsa_permute(Perm, InFile, OutFile) :- + cpsa:cpsa(InFile, Cpsas), + cpsa_permute_all(Perm, Cpsas, OutCpsas), + cpsa:cpsas_to_sexprs(OutCpsas, Sexpr), + open(OutFile, write, Stream), + cpsa:cpsa_sexprs_pp(Stream, Sexpr), + close(Stream). + +cpsa_permute_all(_, [], []). +cpsa_permute_all(Perm, [Cpsa|Cpsas], [OutCpsa|OutCpsas]) :- + cpsa_permute_skel(Perm, Cpsa, OutCpsa), + cpsa_permute_all(Perm, Cpsas, OutCpsas). + +cpsa_permute_skel(Perm, k(Prot, Decls, Strands, Precedes, Nons, Pens, Uniqs), + k(Prot, Decls, OutStrands, OutPrecedes, Nons, Pens, Uniqs)) :- + perm_list(Perm, Strands, OutStrands), + perm_precedes(Perm, Precedes, OutPrecedes), + !. +% If above fails, simply copy the input to the output and don't fail. +cpsa_permute_skel(_, Cpsa, Cpsa). + +%% Apply a permutation to a list. +perm_list([], _, []). +perm_list([Index|Indices], List, [Value|Rest]) :- + nth0(Index, List, Value), + perm_list(Indices, List, Rest). + +%% Apply a permutation to a list of pairs of nodes. +perm_precedes(_, [], []). +perm_precedes(Perm, [(N0, N1)|Precedes], [(OutN0, OutN1)|OutPrecedes]) :- + perm_node(Perm, N0, OutN0), + perm_node(Perm, N1, OutN1), + perm_precedes(Perm, Precedes, OutPrecedes). + +perm_node(Perm, (S, I), (OutS, I)) :- + nth0(S, Perm, OutS). diff --git a/src/sexpr.pl b/src/sexpr.pl --- a/src/sexpr.pl +++ b/src/sexpr.pl @@ -4,10 +4,10 @@ %% generates pretty printer trees for S-expressions for use with the %% exports of the pretty printer module pp. -%% Known to work in SWI-Prolog, but not with GNU Prolog. The program -%% makes use of the non-standard atomic data type string to represent -%% strings in S-expressions. Atoms and integers in S-expressions are -%% mapped to Prolog standard atoms and numbers. +%% Known to work in SWI-Prolog, but not with GNU Prolog. Atoms and +%% integers in S-expressions are mapped to Prolog atoms and numbers in +%% the obvious way. Strings in S-expressions are mapped into Prolog +%% atoms that include the opening and closing quote. %% Copyright (c) 2009 The MITRE Corporation %% @@ -71,9 +71,9 @@ sexpr_number(C, S). sexpr(S) --> - sexpr_string_start, + sexpr_string_start(C), !, - sexpr_string(S). + sexpr_string(C, S). sexpr(S) --> sexpr_symbol(S). @@ -107,23 +107,23 @@ sexpr_digit(C), sexpr_digits(L). -% Parse a string minus the opening quote. +% Parse a string with the opening and closing quote. -sexpr_string(S) --> +sexpr_string(C, S) --> sexpr_string_rest(L), - { string_to_list(S, L) }. + { atom_codes(S, [C|L]) }. sexpr_string_rest(L) --> - sexpr_string_start, + sexpr_string_start(C), !, - { L = [] }. + { L = [C] }. sexpr_string_rest([C|L]) --> [C], sexpr_string_rest(L). -sexpr_string_start --> - sexpr_quote. +sexpr_string_start(C) --> + sexpr_quote(C). % Symbols @@ -183,7 +183,7 @@ [C], { code_type(C, digit) }. -sexpr_quote --> +sexpr_quote(C) --> [C], { sexpr_token(C, quote) }. @@ -316,14 +316,6 @@ atom_to_pretty([], Pretty) :- !, pp:atm('()', Pretty). -atom_to_pretty(Thing, Pretty) :- - string(Thing), - !, - atom_codes('"', Quote), - string_to_list(Thing, Codes), - append(Quote, Codes, X), - append(X, Quote, String), - pp:atm(String, Pretty). atom_to_pretty(Thing, Pretty) :- atomic(Thing), pp:atm(Thing, Pretty).