packages feed

cpsa 2.2.6 → 2.2.7

raw patch · 88 files changed

+2016/−472 lines, 88 filesbinary-added

Files

ChangeLog view
@@ -1,3 +1,32 @@+2012-02-01  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Version):  Tagged as version 2.2.7.++	* doc/cpsasdha.tex: Added a document describing the current+	implementation of a Diffie-Hellman algebra.++2012-01-25  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/*/Algebra.hs (encryptions): Used the C preprocessor to+	all support for GHC 6.x while eliminating the annoying warnings+	because Data.Map.foldWithKey has been deprecated in newer versions+	of GHC.++	* src/CPSA/Lib/Algebra.hs (encryptions): Changed the signature so+	that an encryption returned by this function may have more than+	one key used to prepare it as in the case of Diffie-Hellman+	algebras.++2011-12-20  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Basic/Algebra.hs (match): Handle algebra equation with+	the rule match(invk(t), t', env) -> match(t, invk(t'), env) when+	t' is not of the form invk(t").  Corrects a missing case in+	previous algorithm.++	* src/CPSA/Lib/Notation.hs (mesg): Print (hash a b ... z)+	as #(a, b, ..., z).+ 2011-12-09  John D. Ramsdell  <ramsdell@mitre.org>  	* src/CPSA/Graph/SVG.hs (tooltip): Display tool tips with@@ -5,6 +34,8 @@ 	xlink:title='MESSAGE'>...</a> so that tool tips work in Firefox 	and Chrome again. +	* cpsa.cabal (Version):  Tagged as version 2.2.6.+ 2011-11-18  John D. Ramsdell  <ramsdell@mitre.org>  	* tst/deorig_mesg.scm (deorig-mesg):  Added an example showing@@ -378,12 +409,12 @@ 2010-10-02  John D. Ramsdell  <ramsdell@mitre.org>  	* src/CPSA/Lib/Algebra.hs: Added heldBy to support-	Diffie-Hellman. +	Diffie-Hellman.  2010-09-23  John D. Ramsdell  <ramsdell@mitre.org>  	* src/CPSA/Lib/Notation.hs (mesg): Use [x,y,..]k instead of-	E(k;x,y,...). +	E(k;x,y,...).  2010-09-17  John D. Ramsdell  <ramsdell@mitre.org> @@ -396,13 +427,13 @@  	* src/CPSA/Graph/Tree.hs (assemble): To handle incomplete outputs, 	assemble ignores unavailable seen children instead of signaling an-	error. +	error.  2010-08-24  John D. Ramsdell  <ramsdell@mitre.org>  	* src/CPSA/Lib/Strand.hs (augCollapses): Pruning is now performed 	only after augmentation, and only when the augmented strand is-	involved. +	involved.  2010-08-12  John D. Ramsdell  <ramsdell@mitre.org> @@ -470,7 +501,7 @@ 	* cpsa.cabal (Version): Tagged as version 2.0.5.  	* doc/cpsatheory.tex: Added theory document on authentication-	tests. +	tests.  2010-06-11  John D. Ramsdell  <ramsdell@mitre.org> @@ -623,7 +654,7 @@  2010-01-07  John D. Ramsdell  <ramsdell@mitre.org> -	* src/CPSA/Lib/Strand.hs (copresentVertices): Fixed a bug, and now +	* src/CPSA/Lib/Strand.hs (copresentVertices): Fixed a bug, and now 	contractions with ordering codes works, when 	Cohort.useContractionsWithOrdering is True. @@ -684,7 +715,7 @@ 2009-10-14  John D. Ramsdell  <ramsdell@mitre.org>  	* src/preskel.sh: Added a script to change defpreskeleton to-	defskeleton. +	defskeleton.  	* src/CPSA/Lib/Loader.hs (loadSExpr): Changed defpreskeleton 	keyword to defskeleton.@@ -727,7 +758,7 @@ 	* src/CPSA/Diffie-Hellman/Algebra.hs:  Added a module for 	analyzing protocols that use Diffie-Hellman.  Its unifier and 	matcher make use of fresh variable generation.-	+ 2009-09-16  John D. Ramsdell  <ramsdell@mitre.org>  	* src/CPSA/Lib/Cohort.hs (mgus): Added a filter that removes@@ -760,7 +791,7 @@  2009-08-03  John D. Ramsdell  <ramsdell@mitre.org> -	* src/CPSA/Basic/Algebra.hs:  Added labeled named akey operations +	* src/CPSA/Basic/Algebra.hs:  Added labeled named akey operations 	(pubk STRING ID) and (privk STRING ID).  2009-08-02  John D. Ramsdell  <ramsdell@mitre.org>@@ -774,7 +805,7 @@  	* src/CPSA/Lib/Strand.hs (permutations): Reversed the order in 	which strands are matched, and found a big performance-	improvement. +	improvement.  	* src/CPSA/Lib/Loader.hs (loadRole): Unused variables in a role 	are now silently dropped instead of causing an error message.@@ -801,7 +832,7 @@  2009-07-01  John D. Ramsdell  <ramsdell@mitre.org> -	* src/CPSA/Graph/LaTeXView.hs (latexView): +	* src/CPSA/Graph/LaTeXView.hs (latexView):  2009-06-23  John D. Ramsdell  <ramsdell@mitre.org> @@ -906,7 +937,7 @@ 	* src/CPSA/Lib/Strand.hs (collapse): Added the collapse operation 	which applies to a shape.  It attempts to unify pairs of strands 	and searches for shapes starting from the results.-	+ 	* src/CPSA/Shapes/Shapes.hs (shapes): Reduced memory requirements 	by use of shape notes and added support for output in which a 	shape is a descendent of a shape.@@ -960,7 +991,7 @@ 2009-04-18  John D. Ramsdell  <ramsdell@mitre.org>  	* src/CPSA/Basic/Algebra.hs (IdMap): Use Data.Map Id Term for-	substitutions instead of association lists. +	substitutions instead of association lists.  	* src/CPSA/Basic/Algebra.hs (loadVar): Removed sort "term" as a 	synonym for "mesg".@@ -1101,11 +1132,11 @@ 	format to expanded format.  2008-12-01  John D. Ramsdell  <ramsdell@mitre.org>-	+ 	* cpsa.cabal (Version): Tagged as version 1.3.2.  2008-11-30  John D. Ramsdell  <ramsdell@mitre.org>-	+ 	* src/CPSA/Lib/Strand.hs (roleOrigCheck): Added new well-formed 	preskeleton check.  Every uniquely originating role term mapped by 	an instance must be mapped to a term that originates on the@@ -1137,7 +1168,7 @@  	* src/CPSA/Lib/Cohort.hs (addListeners):  Listeners are now added 	only for the decryption keys of the top most encryptions in the-	escape set.  This fixes a bug caused by adding listeners for +	escape set.  This fixes a bug caused by adding listeners for 	decryption keys of internal encryptions in the escape set.  	* src/CPSA/Lib/Algebra.hs (decryptionKey):  Changed the name from@@ -1239,7 +1270,7 @@ 	* src/CPSA/Lib/Cohort.hs (transformingNode): The fix on the 22th 	wasn't right, it unified on all outgoing terms.  The function now 	unifies an outgoing term only when it is a transforming node.-	+ 2008-09-24  John D. Ramsdell  <ramsdell@mitre.org>  	* src/CPSA/*/*.hs:  Loading works with all monads.  With this@@ -1264,7 +1295,7 @@ 	which should be defined when Control.Parallel is available.  	* src/CPSA/*/*.hs:  A major code clean up was completed.-	+ 2008-09-17  John D. Ramsdell  <ramsdell@mitre.org>  	* src/CPSA/Lib/Strand.hs (Gist): Created a data structure designed@@ -1319,7 +1350,7 @@ 2008-08-11  John D. Ramsdell  <ramsdell@mitre.org>  	* tst/Makefile: Changed the file extensions to be consistent with-	the ones used in doc/cpsa.mk. +	the ones used in doc/cpsa.mk.  	* src/CPSA/Basic/Loader.hs: Added tags as non-atomic terms, and 	removed tagged concatenation.@@ -1428,7 +1459,7 @@  2008-04-30  Joshua D. Guttman  <guttman@mitre.org> -	* src/CPSA/Basic/Main.hs: Re-enabled indeterminates +	* src/CPSA/Basic/Main.hs: Re-enabled indeterminates  2008-02-27  John D. Ramsdell  <ramsdell@mitre.org>
NEWS view
@@ -1,5 +1,24 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.2.7++** A bug in the matcher in each algebra was repaired+   There was a missing case involving asymmetric key inverse that+   caused an erroneous matching failure.++** Compiler warnings eliminated+   The C preprocessor is now used to eliminate the warning that+   the use of Data.Map.foldWithKey is deprecated while preserving the+   ability to compile CPSA using GHC 6.x.++** Diffie-Hellman algebra bug fixed+   CPSA produces two listeners for the term (exp (exp (gen) x) y),+   instead of one as it used to.  Test case tst/dhke.scm shows the bug+   has been fixed.++** Diffie-Hellman algebra documentation added+   The document titled "Simple Diffie-Hellman Algebra" is in cpsasdha.pdf.+    * Changes in version 2.2.6  ** SVG tooltips work once again
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:			cpsa-Version:		2.2.6+Version:		2.2.7 Maintainer:		ramsdell@mitre.org Cabal-Version:		>= 1.6 License:		BSD3@@ -44,16 +44,16 @@ Build-Type:		Simple Data-Files:    index.html cpsauser.html cpsa.mk Make.hs cpsaprimer.pdf-   cpsaoverview.pdf cpsaspec.pdf cpsadesign.pdf ffgg.scm ns.scm or.scm-   woolam.scm yahalom.scm+   cpsaoverview.pdf cpsaspec.pdf cpsadesign.pdf cpsasdha.pdf+   ffgg.scm ns.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   doc/cpsaspec.tex doc/cpsadesign.tex doc/cpsaoverview.tex-  doc/cpsadiagrams.mp doc/strands.mp doc/cmstrands.mp doc/carriers.mp-  doc/termtree.mp doc/cpsa.bib doc/SDAG.lhs doc/cpsaspec.pdf-  doc/cpsadesign.pdf+  doc/cpsasdha.tex doc/cpsadiagrams.mp doc/strands.mp doc/cmstrands.mp+  doc/carriers.mp doc/termtree.mp doc/cpsa.bib doc/SDAG.lhs+  doc/SimpleDiffieHellman.hs   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@@ -102,7 +102,7 @@   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/DH_hack.scm tst/DH_hack.tst tst/timestamping.scm tst/timestamping.tst  -- Algebra implementations must import CPSA.Lib.CPSA. -- Tools may additionally import CPSA.Lib.Entry.
doc/Makefile view
@@ -9,10 +9,11 @@  SHELL = /bin/sh -DESIGN = cpsadesign PRIMER = cpsaprimer-SPEC = cpsaspec OVERVIEW = cpsaoverview+DESIGN = cpsadesign+SPEC = cpsaspec+SDHA = cpsasdha BIB = cpsa  TEX_SRCS = macros.tex bcasyntax.tex@@ -30,7 +31,7 @@ %.ind:	%.idx 	makeindex $* -all:	$(PRIMER).pdf $(OVERVIEW).pdf $(DESIGN).pdf $(SPEC).pdf+all:	$(PRIMER).pdf $(OVERVIEW).pdf $(DESIGN).pdf $(SPEC).pdf $(SDHA).pdf  $(PRIMER).pdf:	$(MP_SRCS:.mp=-0.mps) $(TEX_SRCS) \ 		 $(PRIMER).tex $(PRIMER).bbl@@ -54,8 +55,12 @@ 	if test -f $(SPEC).idx; then $(MAKE) $(SPEC).ind; fi 	pdflatex $(SPEC).tex +$(SDHA).pdf: $(SDHA).tex $(SDHA).bbl+	if test ! -f $(SDHA).aux; then pdflatex $(SDHA).tex; fi+	pdflatex $(SDHA).tex+ CLEAN_FILES := $(PRIMER).pdf $(OVERVIEW).pdf \-		$(DESIGN).pdf $(SPEC).pdf \+		$(DESIGN).pdf $(SPEC).pdf $(SDHA).pdf \ 	$(wildcard *.log *.aux *.toc *.mps *.mpx) \ 	$(wildcard *.bbl *.blg *.ind *.idx *.ilg *.out)
doc/README view
@@ -11,6 +11,8 @@  * cpsadesign.pdf: CPSA Design, a description of implementation choices +* cpsasdha.pdf: Simple Diffie-Hellman Algebra+ To build the documentation, you need Metapost and XY-pic.  On Linux, Metapost is supplied via the package texlive-metapost, and XY-pic is supplied in package texlive-pictures.  On some older versions of
+ doc/SimpleDiffieHellman.hs view
@@ -0,0 +1,212 @@+-- Unification and matching in a simple Diffie-Hellman algebra++module SimpleDiffieHellman where++-- Equational unification and matching in an algebra with the+-- following equation is used to analyze protocols that make use of+-- the Diffie-Hellman problem.+--+--      exp(exp(x, y), z) = exp(exp(x, z), y)+--+-- The module shows how to perform the unification and matching.++import Char(isDigit, isAlpha)++-- TERMS++-- Variables are just integers so that it is easy to freshly generate+-- them.++type Var = Int++data Term                       -- A term is+    = V Var                     -- a variable, or a+    | F String [Term]           -- function symbol and a list of terms++-- Equality modulo the equation: exp(exp(x, y), z) = exp(exp(x, z), y).+instance Eq Term where+    (V x) == (V y) = x == y+    (F "exp" [F "exp" [x, y], z]) == (F "exp" [F "exp" [x', y'], z']) =+         x == x' && y == y' && z == z' ||+         x == x' && y == z' && z == y'+    (F sym ts) == (F sym' ts') = sym == sym' && ts == ts'+    _ == _ = False++-- SUBSTITUTIONS++-- A substitution is a map from variables to terms+type Subst = [(Var, Term)]++-- Apply a substitution to a term+subst :: Subst -> Term -> Term+subst s (V x) =+    case chase s (V x) of+      V y -> V y+      t -> subst s t+subst s (F sym ts) =+    F sym (map (subst s) ts)++-- A substitution may contain an equivalence class of variables.  The+-- chase function finds the canonical representitive of the+-- equivalence class.+chase :: Subst -> Term -> Term+chase s (V x) =+    case lookup x s of+      Nothing -> V x+      Just t -> chase s t+chase _ t = t++-- UNIFICATION++-- This is the entry point+unify :: Term -> Term -> [Subst]+unify t t' =+    unify0 t t' []++-- Chase variables to start unifying two terms+unify0 :: Term -> Term -> Subst -> [Subst]+unify0 t t' s =+    unify1 (chase s t) (chase s t') s++-- Unification by case analysis+unify1 :: Term -> Term -> Subst -> [Subst]+unify1 (V x) (V y) s            -- Unify two variables+    | x == y = [s]              -- Nothing to do+    | x < y = [(y, V x) : s]    -- Substitute larger variable+    | otherwise = [(x, V y) : s] -- in preference to a smaller one+unify1 (V x) t s+    | occurs x t = []           -- Fail when x is in t+    | otherwise = [(x, t) : s]+unify1 t t'@(V _) s =+    unify1 t' t s+-- Unify using the Diffie-Hellman equation.+-- To make unification tractable, one makes use of the equation+-- exp(exp(gen(), x), y) = exp(exp(gen(), y), x).+unify1 (F "exp" ts@[u, v]) (F "exp" ts'@[u', v']) s =+    unifyList ts ts' s ++     -- Ordinary unification+    -- Add an instances of the equation, and unify on both sides+    do+      s' <- unifyList ts left s+      unifyList ts' right s'+    where+      -- Generate a fresh variable by looking at the variables in use+      var = nextVar ([u, v,  u', v'] ++ terms s) -- Include  substitution+      var' = var + 1                -- Generate another variable+      left = [F "exp" [F "gen" [], V var], V var'] -- One side of equation+      right = [F "exp" [F "gen" [], V var'], V var] -- And the other+unify1 (F sym ts) (F sym' ts') s -- Unify ordinary compound terms+    | sym /= sym' = []           -- Fail on symbol clash+    | otherwise = unifyList ts ts' s++unifyList :: [Term] -> [Term] -> Subst -> [Subst]+unifyList [] [] s = [s]+unifyList (t:ts) (t':ts') s =+    do+      s <- unify0 t t' s+      unifyList ts ts' s+unifyList _ _ _ = []++-- Find next unused variable in a list of terms+nextVar :: [Term] -> Var+nextVar [] = 0+nextVar ts =+    maximum (map nextVariable ts)+    where+      nextVariable (V x) = x + 1+      nextVariable (F _ ts) = nextVar ts++-- Returns the terms in a substitution.+terms :: Subst -> [Term]+terms s =+    [ t' |+      (x, t) <- s,+      t' <- [V x, t] ]++-- Does variable x occur in term t?+occurs :: Var -> Term -> Bool+occurs x (V y) = x == y+occurs x (F _ ts) = any (occurs x) ts++-- MATCHING++-- This is the entry point+match :: Term -> Term -> [Subst]+match t t' =+    match0 t t' []++-- Matching by case analysis+match0 :: Term -> Term -> Subst -> [Subst]+match0 (V x) t s =+    case lookup x s of+      Nothing -> [(x, t) : s]+      Just t' -> if t == t' then [s] else []+-- Match using the Diffie-Hellman equation+match0 (F "exp" [x, y]) (F "exp" [F "exp" [x', y'], z']) s =+    matchList [x, y] [F "exp" [x', y'], z'] s +++    matchList [x, y] [F "exp" [x', z'], y'] s+match0 (F sym ts) (F sym' ts') s+    | sym /= sym' = []+    | otherwise = matchList ts ts' s+match0 _ _ _ = []++matchList :: [Term] -> [Term] -> Subst -> [Subst]+matchList [] [] s = [s]+matchList (t:ts) (t':ts') s =+    do+      s <- match0 t t' s+      matchList ts ts' s+matchList _ _ _ = []++-- TERM ORDERING++instance Ord Term where+    compare (V x) (V y) = compare x y+    compare (F "exp" [F "exp" [x, y], z])+            (F "exp" [F "exp" [x', y'], z']) =+        case (compare y z, compare y' z') of+          (GT, GT) -> compare [F "exp" [x, z], y] [F "exp" [x', z'], y']+          (GT, _) -> compare [F "exp" [x, z], y] [F "exp" [x', y'], z']+          (_, GT) -> compare [F "exp" [x, y], z] [F "exp" [x', z'], y']+          _ -> compare [F "exp" [x, y], z] [F "exp" [x', y'], z']+    compare (F sym ts) (F sym' ts') =+        case compare sym sym' of+          EQ -> compare ts ts'+          c -> c+    compare (V _) (F _ _) = LT+    compare (F _ _) (V _) = GT++-- TERM INPUT++instance Read Term where+    readsPrec _ s =+        readTerm s+        where+          readTerm s =+              [(V $ read (c:cs), t) | (c:cs, t) <- lex s,+                                      isDigit c] +++              [(F (c:cs) ts, v)     | (c:cs, t) <- lex s,+                                      isAlpha c,+                                      ("(", u) <- lex t,+                                      (ts, v) <- readArgs u]+          readArgs s =+              [([], t)              | (")", t) <- lex s] +++              [(x:xs, u)            | (x, t) <- reads s,+                                      (xs, u) <- readRest t]+          readRest s =+              [([], t)              | (")", t) <- lex s] +++              [(x:xs, v)            | (",", t) <- lex s,+                                      (x, u) <- reads t,+                                      (xs, v) <- readRest u]++-- TERM OUTPUT++instance Show Term where+    showsPrec _ (V x) =+        shows x+    showsPrec _ (F sym ts) =+        showString sym . showChar '(' . showArgs ts+        where+          showArgs [] = showChar ')'+          showArgs (x:xs) = shows x . showRest xs+          showRest [] = showChar ')'+          showRest (x:xs) = showChar ',' . shows x . showRest xs
doc/cpsa.bib view
@@ -132,30 +132,12 @@     year = 1983 } -@Manual{cpsatheory11,+@TechReport{cpsatheory11,   title = 	 {Completeness of {CPSA}},-  OPTkey = 	 {},   author = 	 {Moses D.~Liskov and Paul D.~Rowe and F.~Javier Thayer},-  organization = {The MITRE Corporation},-  OPTaddress = 	 {},-  OPTedition = 	 {},-  OPTmonth = 	 {},+  institution = {The MITRE Corporation},   year = 	 2011,-  OPTannote = 	 {}-}--@Manual{cpsatheory10,-  title = 	 {{CPSA} Theory},-  OPTkey = 	 {},-  author = 	 {Moses D.~Liskov and John D.~Ramsdell and Paul D.~Rowe},-  organization = {The MITRE Corporation},-  OPTaddress = 	 {},-  OPTedition = 	 {},-  OPTmonth = 	 {},-  year = 	 2010,-  note = 	 {In \url{http://hackage.haskell.org/package/cpsa} source-    distribution, \texttt{doc} directory},-  OPTannote = 	 {}+  number = 	 {MTR110479}, }  @Manual{cpsaspec09,@@ -205,6 +187,20 @@   title = 	 {{CPSA} Overview},   OPTkey = 	 {},   author = 	 {John D.~Ramsdell and Joshua D.~Guttman},+  organization = {The MITRE Corporation},+  OPTaddress = 	 {},+  OPTedition = 	 {},+  OPTmonth = 	 {},+  year = 	 2009,+  note = 	 {In \url{http://hackage.haskell.org/package/cpsa} source+    distribution, \texttt{doc} directory},+  OPTannote = 	 {}+}++@Manual{cpsauser09,+  title = 	 {{CPSA} User Guide},+  OPTkey = 	 {},+  author = 	 {John D.~Ramsdell},   organization = {The MITRE Corporation},   OPTaddress = 	 {},   OPTedition = 	 {},
doc/cpsadesign.pdf view

binary file changed (203140 → 203126 bytes)

doc/cpsadesign.tex view
@@ -1212,10 +1212,9 @@ \\\qquad\mbox{if }\lnot\cn{bound}(x, \ell)\mbox{ then }(x,t)\cons\ell \\\qquad\mbox{else if } \cn{lookup}(x,\ell)= t\mbox{ then }\ell \\\qquad\mbox{else raise failure}-\\\cn{match}(\ell,\cn{invk}(x),\cn{pubk}(y)) =-\cn{match}(\ell, x, \cn{invk}(\cn{pubk}(y)))\hfill(!) \\\cn{match}(\ell,f(t,\ldots),f(t',\ldots)) = \cn{match\_list}(\ell,\seq{t,\ldots},\seq{t',\ldots})+\\\cn{match}(\ell,\cn{invk}(t),t') = \cn{match}(\ell,t,\cn{invk}(t'))\hfill(!) \\\cn{match}(\ell,t,t') =\mbox{raise failure} \\ \\\cn{bound}(x,\seq{})=\cn{false}
doc/cpsaoverview.pdf view

binary file changed (75802 → 75612 bytes)

doc/cpsaprimer.pdf view

binary file changed (186031 → 186155 bytes)

doc/cpsaprimer.tex view
@@ -1,7 +1,6 @@ \documentclass[12pt]{article} \usepackage{amssymb} \usepackage{amsmath}-\usepackage{amsthm} \usepackage{url} \usepackage{graphicx} \usepackage{makeidx}
+ doc/cpsasdha.pdf view

binary file changed (absent → 130005 bytes)

+ doc/cpsasdha.tex view
@@ -0,0 +1,477 @@+\documentclass[12pt]{article}+\usepackage{url}+\usepackage{amssymb}+\usepackage{amsmath}+\input{macros}++\title{Simple Diffie-Hellman Algebra}+\author{John D. Ramsdell\\+  The MITRE Corporation\\ CPSA Version \version}++\hyphenation{pre-skel-e-ton}+\hyphenation{pro-to-skel-e-ton}+\hyphenation{pro-to-role}++\newcommand{\sdha}{\textsc{sdha}}+\newcommand{\gen}{\ensuremath{\cn{g}}}+\newcommand{\svars}{\fn{Vars}}+\newcommand{\sdom}{\fn{Dom}}+\newcommand{\sran}{\fn{Ran}}+\newcommand{\alga}{\alg{A}}+\newcommand{\base}{\ensuremath{\mathfrak B}}+\newcommand{\carpos}{\fn{carpos}}+\newcommand{\tr}{\ensuremath{\mathfrak C}}+\newcommand{\evt}{\fn{evt}}+\newcommand{\mesg}{\fn{mesg}}+\newcommand{\role}{\mathsf{r}}+\newcommand{\rl}{\fn{rl}}+\newcommand{\skel}{\mathsf{k}}+\newcommand{\nodes}{\fn{nodes}}+\newcommand{\lsn}{\fn{lsn}}+\newcommand{\pubmsg}{\mathbf{P}}+\newcommand{\excl}{\mathbf{X}}+\newcommand{\transpred}{\mathbf{T}}+\newcommand{\init}{\fn{init}}+\newcommand{\resp}{\fn{resp}}++\begin{document}+\maketitle+\cpsacopying++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+difficult to implement such an algebra within the current {\cpsa}+framework without significant revisions to {\cpsa}.++This paper describes a simple Diffie-Hellman algebra in which the+exponent is not an Abelian group.  Instead, the algebra only captures+the commutative law of exponents.  The algebra requires few changes to+the basic formalism used by {\cpsa}~\cite{cpsaspec09}.  An atom that+originates in a trace need not be carried as long as it is in an+exponent of something carried.  Similarly, in a skeleton, an atom+assumed to be uniquely originating need not be carried as long as it+is in an exponent of something carried. (See Section~\ref{sec:strand+  spaces}).++The trade-off for ease of implementation is a loss of coverage.+Protocols that make use of the associativity or the inverses of+exponents cannot be correctly analyzed using this algebra.  In+particular, group Diffie-Hellman protocols typically cannot be+handled.  {\cpsa} with the simple Diffie-Hellman algebra can analyze+restricted Diffie-Hellman protocols, such as the basic Diffie-Hellman+Key Exchange Protocol.  This protocol serves as an example in this+paper.++$$\begin{array}{r@{{}:{}}l}+A\to B&\enc{\mbox{``i''}, \gen^x}{a^{-1}}\\+B\to A&(\enc{\gen^y}{b^{-1}}, \enc{a, b}{\gen^{xy}})\\+A\to B&\enc{\mbox{``i''}, a, b}{\gen^{xy}}+\end{array}$$+Alice~($A$) freshly generates an exponent~$x$, signs the exponentiated+value with her private uncompromised asymmetric key $a^{-1}$, and+sends it to Bob~($B$).  Bob freshly generates an exponent~$y$, signs+the exponentiated value with his private uncompromised asymmetric key+$b^{-1}$, and sends it to Alice along with the public signing keys+encrypted with the newly generated symmetric key~$\gen^{xy}$.  Alice+confirms the symmetric key by signing the public keys too.  Alice+ensures her messages cannot be confused with Bob's by adding the tag+constant ``i'' within her signed data.++\begin{figure}+\begingroup\footnotesize+\begin{verbatim}+(herald "Diffie-Hellman Key Exchange" (algebra diffie-hellman))++(defprotocol dhke diffie-hellman+  (defrole init (vars (a b akey) (x y expn))+    (trace+     (send (enc "i" (exp (gen) x) (invk a)))+     (recv (cat (enc (exp (gen) y) (invk b))+                (enc a b (exp (exp (gen) y) x))))+     (send (enc "i" a b (exp (exp (gen) y) x))))+    (uniq-orig  x))+  (defrole resp (vars (a b akey) (x y expn))+    (trace+     (recv (enc "i" (exp (gen) x) (invk a)))+     (send (cat (enc (exp (gen) y) (invk b))+                (enc a b (exp (exp (gen) x) y))))+     (recv (enc "i" a b (exp (exp (gen) x) y))))+    (uniq-orig y)))++(defskeleton dhke (vars (a b akey))+  (defstrand resp 3 (a a) (b b))+  (non-orig (invk a) (invk b)))++ (defskeleton dhke (vars (a b akey))+   (defstrand init 2 (a a) (b b))+   (non-orig (invk a) (invk b)))+\end{verbatim}+\endgroup+\caption{Diffie-Hellman Key Exchange {\cpsa} Input}\label{fig:dhke}+\end{figure}++The protocol in {\cpsa} syntax is presented in Figure~\ref{fig:dhke}.+{\cpsa} concludes there is key agreement from the perspective of both+Alice and Bob using this input.  Notice that $\gen^{xy}$ is written+\texttt{(exp (exp (gen) x) y)}.  There is no multiplication is this+algebra, and $\gen^{xy}$ is more accurately written as $(\gen^x)^y$.++\section{Order-Sorted Message Algebra}\label{sec:order-sorted mesg algs}++{\cpsa} models a message as an equivalence class of terms over a+signature.  In particular, {\cpsa} uses order-sorted quotient term+algebras~\cite{GoguenMeseguer92} for message algebras.  This formalism+enables the use of well-known algorithms for unification and matching+in the presence of equations~\cite[Chapter~8]{RobinsonVoronkov01}+while providing a sort system for classifying messages.++{\cpsa} provides a Diffie-Hellman algebra that extends the Basic+Crypto Algebra with two new sorts, \texttt{base} and \texttt{expn},+and two new operations, \texttt{(gen)}, a constant of sort+\texttt{base} for exponentiation, and \texttt{(exp $G$ $X$)}, the+exponentiation operation~\cite{cpsauser09}.++\begin{figure}+$$\begin{array}{ll@{{}\colon{}}ll}+\mbox{Sorts:}&\multicolumn{3}{l}{\mbox{$\top$, \srt{D}, \srt{A}, \srt{S}, and \srt{E}}}\\+\mbox{Subsorts:}&\multicolumn{3}{l}{\mbox{$\srt{D}<\top$,+$\srt{A}<\top$, $\srt{S}<\top$, and $\srt{E}<\top$}}\\+\mbox{Base Sorts:}&\multicolumn{3}{l}{\mbox{\srt{D}, \srt{A}, and \srt{E} (\srt{S} and+$\top$ omitted)}}\\+\mbox{Operations:}&(\cdot,\cdot)&\top\times\top\to\top& \mbox{Pairing}\\+&\enc{\cdot}{(\cdot)}&\top\times\srt{S}\to\top& \mbox{Symmetric encryption}\\+&\enc{\cdot}{(\cdot)}&\top\times\srt{A}\to\top& \mbox{Asymmetric encryption}\\+&\mbox{``\ldots''}&\top&\mbox{Tag constants}\\+&(\cdot)^{-1}&\srt{S}\to\srt{S}& \mbox{Symmetric key inverse}\\+&(\cdot)^{-1}&\srt{A}\to\srt{A}& \mbox{Asymmetric key inverse}\\+&\gen&\srt{S}&\mbox{Generator}\\+&{(\cdot)}^{(\cdot)}&\srt{S}\times\srt{E}\to\srt{S}&\mbox{Exponentiation}\\+\mbox{Equations:}&\multicolumn{3}{l}{(a^{-1})^{-1}\approx a\qquad+  s^{-1}\approx s\qquad (h^x)^y\approx (h^y)^x}\\+&\multicolumn{3}{l}{\mbox{where $a\colon\srt{A}$, $s,h\colon\srt{S}$, and $x,y\colon\srt{E}$}}+\end{array}$$+\caption{Simple Diffie-Hellman Algebra Signature and+  Equations}\label{fig:dh signature}+\end{figure}++This paper presents a very simple message algebra for analyzing+protocols using Diffie-Hellman, called the Simple Diffie-Hellman+Algebra (\sdha), that suffices for this document.  There are five+{\sdha} sorts: $\top$, the sort of all messages, and sorts for+data~(\srt{D}), asymmetric keys~(\srt{A}), symmetric keys~(\srt{S}),+and exponents~(\srt{E}).  Every symmetric key is a message (written+$\srt{S}<\top$), and so forth for the other non-$\top$ sorts.  The+operations used to form terms are given by the signature in+Figure~\ref{fig:dh signature}.  Notice that the encryption and key+inverse operations are overloaded.++There are two equations in {\sdha} associated with key inverse.  For+asymmetric key $a\colon\srt{A}$, $(a^{-1})^{-1}\approx a$, and for+symmetric key $s\colon\srt{S}$, $s^{-1}\approx s$.  The equation for+exponentiation is $(h^x)^y\approx (h^y)^x$, where $h\colon\srt{S}$ and+$x,y\colon\srt{E}$.  Unification and matching in this algebra produce a+finite number of most general unifiers, that is, the unification type+is finitary.  For example, $\{x\mapsto u,y\mapsto v\}$ and $\{x\mapsto+\gen^v,u\mapsto \gen^y\}$ unify $x^y$ and $u^v$.  Unification is+finitary because of an approximation.  To unify $a^{xy}$ and~$b^{wz}$,+we unify $a^{xy}$ with~$\gen^{uv}$ and $\gen^{vu}$ with~$b^{wz}$,+where~$u$ and~$v$ are freshly generated variables.  In other words,+for the purpose of unification only, the equation for exponentiation+is $(\gen^x)^y\approx (\gen^y)^x$.  Expository Haskell code for+unification and matching with just the equation for exponentiation is+presented in Appendix~\ref{sec:haskell}.++Origination assumption in roles and skeletons can only be applied to a+subset of the messages of an algebra---the atoms.  In {\sdha},+asymmetric keys and exponents are atoms, but symmetric keys are not.+(Similarly, in the implemented Diffie-Hellman algebra, messages of+sort \texttt{base} are not atoms.)++A message~$t_0$ is \emph{carried by}~$t_1$, written $t_0\sqsubseteq+t_1$ if~$t_0$ can be derived from~$t_1$ given the right set of keys,+that is $\sqsubseteq$ is the smallest reflexive, transitive relation+such that $t_0\sqsubseteq t_0$, $t_0\sqsubseteq (t_0, t_1)$,+$t_1\sqsubseteq (t_0, t_1)$, and $t_0\sqsubseteq\enc{t_0}{t_1}$.++The introduction of the Diffie-Hellman algebra requires a new relation+on messages.  A message~$t_0$ is \emph{held by}~$t_1$, written+$t_0\preceq t_1$ iff $t_1$ carries $t_0$ or $t_1$ is in the exponent+of a carried term.  That is $\preceq$ is the smallest reflexive,+transitive relation such that $t_0\preceq t_0$, $t_0\preceq (t_0,+t_1)$, $t_1\preceq (t_0, t_1)$, $t_0\preceq\enc{t_0}{t_1}$,+$t_1\preceq t_0^{t_1}$.++\section{Strand Spaces}\label{sec:strand spaces}++A run of a protocol is viewed as an exchange of messages by a finite+set of local sessions of the protocol.  Each local session is called a+\emph{strand}~\cite{ThayerEtal99}.  The behavior of a strand, its+\emph{trace}, is a non-empty sequence of messaging events.  An+\emph{event} is either a message transmission or a reception.  In the+Basic Crypto Algebra, a message originates in a trace if it is carried+by some event and the first event in which it is carried is a+transmission.  For Diffie-Hellman, a message \emph{originates} in a+trace if it is held by some event and the first event in which it is+held is a transmission.++A similar change was made for skeletons.  An atom assumed to be+uniquely originating need only be held by some term within a skeleton,+it no longer must be carried.++\section{Derivable Messages}\label{sec:pen deriv mesgs}++Suppose~$T$ is a set of messages.  Let $\to$ be a reduction relation+on sets of messages defined as follows:+$$\begin{array}{r@{{}\to{}}ll}+\{(t_0,t_1)\}\cup T&\{t_0,t_1\}\cup T\\+\{\enc{t_0}{t_1}\}\cup T&\{t_0,\enc{t_0}{t_1}\}\cup T+&\mbox{if $t_1^{-1}\in D(T)$ and $t_0\notin T$}+\end{array}$$+The minimum decryption set~$M(T)$ is the normal form of relation~$\to$,+i.e.\ $T\to^\ast M(T)$ and there is no~$T'$ such that $M(T)\to T'$.++A message~$t$ is \emph{derivable} from~$T$, iff $t\in D(T)$, where+$$\begin{array}{r@{{}={}}l}+D^0&M(T)\\+D^{n+1}&\left\{\begin{array}{c@{{}\mid{}}l}+(x,y)&x,y\in D^n\\+\enc{x}{y}&x,y\in D^n,y\colon\srt{A}\lor y\colon\srt{S}\\+x^y& x,y\in D^n, x\colon\srt{S}, y\colon\srt{E}+\end{array}\right\}\\+D(T)&\bigcup_{n\in\nat}D^n+\end{array}$$++\section{Conclusion}++In this algebra, one cannot analyze group Diffie-Hellman protocols, as+they make use of the associativity of exponents.  On the other hand,+this algebra appears to allow the analysis of the basic Diffie-Hellman+Key Exchange.  In terms of implementation, allowances have to be made+for the fact that unification may produce more than one most general+unifier.++\bibliography{cpsa}+\bibliographystyle{plain}++\appendix++\section{Unification and Matching in Haskell}\label{sec:haskell}++\begingroup\footnotesize+\begin{verbatim}+-- Unification and matching in a simple Diffie-Hellman algebra++module SimpleDiffieHellman where++-- Equational unification and matching in an algebra with the+-- following equation is used to analyze protocols that make use of+-- the Diffie-Hellman problem.+--+--      exp(exp(x, y), z) = exp(exp(x, z), y)+--+-- The module shows how to perform the unification and matching.++import Char(isDigit, isAlpha)++-- TERMS++-- Variables are just integers so that it is easy to freshly generate+-- them.++type Var = Int++data Term                       -- A term is+    = V Var                     -- a variable, or a+    | F String [Term]           -- function symbol and a list of terms++-- Equality modulo the equation: exp(exp(x, y), z) = exp(exp(x, z), y).+instance Eq Term where+    (V x) == (V y) = x == y+    (F "exp" [F "exp" [x, y], z]) == (F "exp" [F "exp" [x', y'], z']) =+         x == x' && y == y' && z == z' ||+         x == x' && y == z' && z == y'+    (F sym ts) == (F sym' ts') = sym == sym' && ts == ts'+    _ == _ = False++-- SUBSTITUTIONS++-- A substitution is a map from variables to terms+type Subst = [(Var, Term)]++-- Apply a substitution to a term+subst :: Subst -> Term -> Term+subst s (V x) =+    case chase s (V x) of+      V y -> V y+      t -> subst s t+subst s (F sym ts) =+    F sym (map (subst s) ts)++-- A substitution may contain an equivalence class of variables.  The+-- chase function finds the canonical representitive of the+-- equivalence class.+chase :: Subst -> Term -> Term+chase s (V x) =+    case lookup x s of+      Nothing -> V x+      Just t -> chase s t+chase _ t = t++-- UNIFICATION++-- This is the entry point+unify :: Term -> Term -> [Subst]+unify t t' =+    unify0 t t' []++-- Chase variables to start unifying two terms+unify0 :: Term -> Term -> Subst -> [Subst]+unify0 t t' s =+    unify1 (chase s t) (chase s t') s++-- Unification by case analysis+unify1 :: Term -> Term -> Subst -> [Subst]+unify1 (V x) (V y) s            -- Unify two variables+    | x == y = [s]              -- Nothing to do+    | x < y = [(y, V x) : s]    -- Substitute larger variable+    | otherwise = [(x, V y) : s] -- in preference to a smaller one+unify1 (V x) t s+    | occurs x t = []           -- Fail when x is in t+    | otherwise = [(x, t) : s]+unify1 t t'@(V _) s =+    unify1 t' t s+-- Unify using the Diffie-Hellman equation.+-- To make unification tractable, one makes use of the equation+-- exp(exp(gen(), x), y) = exp(exp(gen(), y), x).+unify1 (F "exp" ts@[u, v]) (F "exp" ts'@[u', v']) s =+    unifyList ts ts' s ++     -- Ordinary unification+    -- Add an instances of the equation, and unify on both sides+    do+      s' <- unifyList ts left s+      unifyList ts' right s'+    where+      -- Generate a fresh variable by looking at the variables in use+      var = nextVar ([u, v,  u', v'] ++ terms s) -- Include  substitution+      var' = var + 1                -- Generate another variable+      left = [F "exp" [F "gen" [], V var], V var'] -- One side of equation+      right = [F "exp" [F "gen" [], V var'], V var] -- And the other+unify1 (F sym ts) (F sym' ts') s -- Unify ordinary compound terms+    | sym /= sym' = []           -- Fail on symbol clash+    | otherwise = unifyList ts ts' s++unifyList :: [Term] -> [Term] -> Subst -> [Subst]+unifyList [] [] s = [s]+unifyList (t:ts) (t':ts') s =+    do+      s <- unify0 t t' s+      unifyList ts ts' s+unifyList _ _ _ = []++-- Find next unused variable in a list of terms+nextVar :: [Term] -> Var+nextVar [] = 0+nextVar ts =+    maximum (map nextVariable ts)+    where+      nextVariable (V x) = x + 1+      nextVariable (F _ ts) = nextVar ts++-- Returns the terms in a substitution.+terms :: Subst -> [Term]+terms s =+    [ t' |+      (x, t) <- s,+      t' <- [V x, t] ]++-- Does variable x occur in term t?+occurs :: Var -> Term -> Bool+occurs x (V y) = x == y+occurs x (F _ ts) = any (occurs x) ts++-- MATCHING++-- This is the entry point+match :: Term -> Term -> [Subst]+match t t' =+    match0 t t' []++-- Matching by case analysis+match0 :: Term -> Term -> Subst -> [Subst]+match0 (V x) t s =+    case lookup x s of+      Nothing -> [(x, t) : s]+      Just t' -> if t == t' then [s] else []+-- Match using the Diffie-Hellman equation+match0 (F "exp" [x, y]) (F "exp" [F "exp" [x', y'], z']) s =+    matchList [x, y] [F "exp" [x', y'], z'] s +++    matchList [x, y] [F "exp" [x', z'], y'] s+match0 (F sym ts) (F sym' ts') s+    | sym /= sym' = []+    | otherwise = matchList ts ts' s+match0 _ _ _ = []++matchList :: [Term] -> [Term] -> Subst -> [Subst]+matchList [] [] s = [s]+matchList (t:ts) (t':ts') s =+    do+      s <- match0 t t' s+      matchList ts ts' s+matchList _ _ _ = []++-- TERM ORDERING++instance Ord Term where+    compare (V x) (V y) = compare x y+    compare (F "exp" [F "exp" [x, y], z])+            (F "exp" [F "exp" [x', y'], z']) =+        case (compare y z, compare y' z') of+          (GT, GT) -> compare [F "exp" [x, z], y] [F "exp" [x', z'], y']+          (GT, _) -> compare [F "exp" [x, z], y] [F "exp" [x', y'], z']+          (_, GT) -> compare [F "exp" [x, y], z] [F "exp" [x', z'], y']+          _ -> compare [F "exp" [x, y], z] [F "exp" [x', y'], z']+    compare (F sym ts) (F sym' ts') =+        case compare sym sym' of+          EQ -> compare ts ts'+          c -> c+    compare (V _) (F _ _) = LT+    compare (F _ _) (V _) = GT++-- TERM INPUT++instance Read Term where+    readsPrec _ s =+        readTerm s+        where+          readTerm s =+              [(V $ read (c:cs), t) | (c:cs, t) <- lex s,+                                      isDigit c] +++              [(F (c:cs) ts, v)     | (c:cs, t) <- lex s,+                                      isAlpha c,+                                      ("(", u) <- lex t,+                                      (ts, v) <- readArgs u]+          readArgs s =+              [([], t)              | (")", t) <- lex s] +++              [(x:xs, u)            | (x, t) <- reads s,+                                      (xs, u) <- readRest t]+          readRest s =+              [([], t)              | (")", t) <- lex s] +++              [(x:xs, v)            | (",", t) <- lex s,+                                      (x, u) <- reads t,+                                      (xs, v) <- readRest u]++-- TERM OUTPUT++instance Show Term where+    showsPrec _ (V x) =+        shows x+    showsPrec _ (F sym ts) =+        showString sym . showChar '(' . showArgs ts+        where+          showArgs [] = showChar ')'+          showArgs (x:xs) = shows x . showRest xs+          showRest [] = showChar ')'+          showRest (x:xs) = showChar ',' . shows x . showRest xs+\end{verbatim}+\endgroup+\end{document}
doc/cpsaspec.pdf view

binary file changed (330274 → 330270 bytes)

doc/cpsaspec.tex view
@@ -1157,8 +1157,8 @@ a~$k$ such that $k_0\reduction{\ops{S}_\sigma}k\reduction{\ops{C}_{s,s'}}k_1$, there is a homomorphism from~$k_0$ to~$k_1$, and if-$(s,p)\kprec{k_0}(s'',p'')$ then $(s',p')\kprec{k_0}(s'',p'')$, and if-$(s'',p'')\kprec{k_0}(s,p)$ then $(s'',p'')\kprec{k_0}(s',p')$.  For+$(s,p)\kprec{k_0}(s'',p'')$ then $(s',p)\kprec{k_0}(s'',p'')$, and if+$(s'',p'')\kprec{k_0}(s,p)$ then $(s'',p'')\kprec{k_0}(s',p)$.  For the setwise pruning reduction, $\{k_0\}\setreduction{\ops{P}_s}\{k_1\mid k_0\reduction{\ops{P}_s}k_1\}$, when there is a $k_1$ such that
+ doc/dhke.scm view
@@ -0,0 +1,29 @@+(herald "Diffie-Hellman Key Exchange" (algebra diffie-hellman))++;; The Diffie-Hellman problem is given (exp (gen) x), and (exp (gen)+;; y), compute the value of (exp (exp (gen) x) y) which is also (exp+;; (exp (gen) y) x).++(defprotocol dhke diffie-hellman+  (defrole init (vars (a b akey) (x y expn))+    (trace+     (send (enc "i" (exp (gen) x) (invk a)))+     (recv (cat (enc (exp (gen) y) (invk b))+		(enc a b (exp (exp (gen) y) x))))+     (send (enc "i" a b (exp (exp (gen) y) x))))+    (uniq-orig  x))+  (defrole resp (vars (a b akey) (x y expn))+    (trace+     (recv (enc "i" (exp (gen) x) (invk a)))+     (send (cat (enc (exp (gen) y) (invk b))+		(enc a b (exp (exp (gen) x) y))))+     (recv (enc "i" a b (exp (exp (gen) x) y))))+    (uniq-orig y)))++(defskeleton dhke (vars (a b akey))+  (defstrand resp 3 (a a) (b b))+  (non-orig (invk a) (invk b)))++ (defskeleton dhke (vars (a b akey))+   (defstrand init 2 (a a) (b b))+   (non-orig (invk a) (invk b)))
doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.2.6}+\newcommand{\version}{2.2.7} \newcommand{\cpsacopying}{\begingroup   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The     MITRE Corporation.  Permission to copy without fee all or part of
src/CPSA/Basic/Algebra.hs view
@@ -10,7 +10,7 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiParamTypeClasses, CPP #-}  module CPSA.Basic.Algebra (name, origin) where @@ -24,6 +24,14 @@ import qualified CPSA.Lib.CPSA as C import CPSA.Lib.CPSA (SExpr(..), Pos, annotation) +-- Preserve the ability to use GHC 6.x+foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b+#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700+foldrWithKey = M.foldWithKey+#else+foldrWithKey = M.foldrWithKey+#endif+ name :: String name = "basic" @@ -342,16 +350,16 @@ -- Extracts every encryption that is carried by a term along with its -- encryption key.  Note that a hash is treated as a kind of -- encryption in which the term that is hashed is the encryption key.-encryptions :: Term -> [(Term, Term)]+encryptions :: Term -> [(Term, [Term])] encryptions t =     reverse $ loop t []     where       loop (F Cat [t, t']) acc =           loop t' (loop t acc)       loop t@(F Enc [t', t'']) acc =-          loop t' (adjoin (t, t'') acc)+          loop t' (adjoin (t, [t'']) acc)       loop t@(F Hash [t']) acc =-          adjoin (t, t') acc+          adjoin (t, [t']) acc       loop _ acc = acc       adjoin x xs           | x `elem` xs = xs@@ -727,13 +735,10 @@       Nothing -> Just $ Env $ M.insert x t r       Just t' -> if t == t' then Just $ Env r else Nothing match (C c) (C c') r = if c == c' then Just r else Nothing-match (F Invk [I x]) (F Pubk [I y]) r =-    match (I x) (F Invk [F Pubk [I y]]) r-match (F Invk [I x]) (F Pubk [C c, I y]) r =-    match (I x) (F Invk [F Pubk [C c, I y]]) r match (F s u) (F s' u') r     | s == s' = matchLists u u' r-    | otherwise = Nothing+match (F Invk [t]) t' r =+    match t (F Invk [t']) r match _ _ _ = Nothing  matchLists :: [Term] -> [Term] -> Env -> Maybe Env@@ -744,11 +749,11 @@  -- Does every varible in ts not occur in the domain of e? -- Trivial bindings in e are ignored.-idempotentEnvFor :: Env -> [Term] -> Bool-idempotentEnvFor (Env r) ts =+identityEnvFor :: Env -> [Term] -> Bool+identityEnvFor (Env r) ts =     all (allId $ flip S.notMember dom) ts     where-      dom = M.foldWithKey f S.empty r -- The domain of r+      dom = foldrWithKey f S.empty r -- The domain of r       f x (I y) dom           | x == y = dom        -- Ignore trivial bindings           | otherwise = S.insert x dom@@ -805,8 +810,8 @@    instantiate = instantiate    match t t' (g, e) =        maybe [] (\e -> [(g, e)]) $ match t t' e-   idempotentEnvFor (g, e) ts =-       if idempotentEnvFor e ts then+   identityEnvFor (g, e) ts =+       if identityEnvFor e ts then            [(g, e)]        else            []
src/CPSA/DiffieHellman/Algebra.hs view
@@ -14,7 +14,7 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiParamTypeClasses, CPP #-}  module CPSA.DiffieHellman.Algebra (name, origin) where @@ -29,6 +29,14 @@ import CPSA.Lib.CPSA (SExpr(..), Pos, annotation) import qualified CPSA.DiffieHellman.IntLinEq as I +-- Preserve the ability to use GHC 6.x+foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b+#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700+foldrWithKey = M.foldWithKey+#else+foldrWithKey = M.foldrWithKey+#endif+ {-- Debugging support import System.IO.Unsafe @@ -144,7 +152,7 @@  mul :: Group -> Group -> Group mul t t' =-    M.foldWithKey f t' t       -- Fold over the mappings in t+    foldrWithKey f t' t         -- Fold over the mappings in t     where       f x c t =                 -- Alter the mapping of           M.alter (g c) x t     -- variable x in t@@ -567,16 +575,16 @@  -- Extracts every encryption that is carried by a term along with its -- encryption key.-encryptions :: Term -> [(Term, Term)]+encryptions :: Term -> [(Term, [Term])] encryptions t =     reverse $ loop t []     where       loop (F Cat [t, t']) acc =           loop t' (loop t acc)       loop t@(F Enc [t', t'']) acc =-          loop t' (adjoin (t, t'') acc)+          loop t' (adjoin (t, [t'']) acc)       loop t@(F Base [F Exp [_, t'']]) acc =-          adjoin (t, t'') acc+          adjoin (t, [t'']) acc       loop _ acc = acc       adjoin x xs           | x `elem` xs = xs@@ -839,7 +847,7 @@  groupSubst :: IdMap -> Group -> Group groupSubst subst t =-    M.foldWithKey f M.empty t+    foldrWithKey f M.empty t     where       f x n t =           mul (expg (groupLookup subst x) n) t@@ -1105,15 +1113,12 @@       Nothing -> Just (g, Env (v, M.insert x t r))       Just t' -> if t == t' then Just (g, Env (v, r)) else Nothing match (C c) (C c') r = if c == c' then Just r else Nothing-match (F Invk [I x]) (F Pubk [I y]) r =-    match (I x) (F Invk [F Pubk [I y]]) r-match (F Invk [I x]) (F Pubk [C c, I y]) r =-    match (I x) (F Invk [F Pubk [C c, I y]]) r match (F Exp [t0, G t1]) (F Exp [t0', G t1']) r       = matchExp t0 t1 t0' t1' r match (F s u) (F s' u') r     | s == s' = matchLists u u' r-    | otherwise = Nothing+match (F Invk [t]) t' r =+    match t (F Invk [t']) r match (G t) (G t') (g, Env (v, r)) =     do       let (t0, t0') = merge t t' r@@ -1206,8 +1211,8 @@  -- Does every varible in ts not occur in the domain of e? -- Trivial bindings in e are ignored.-idempotentEnvFor :: GenEnv -> [Term] -> Maybe GenEnv-idempotentEnvFor ge ts =+identityEnvFor :: GenEnv -> [Term] -> Maybe GenEnv+identityEnvFor ge ts =     let env@(_, Env (_, r)) = nonTrivialEnv ge in     if all (allId $ flip S.notMember $ M.keysSet r) ts then         Just env@@ -1253,7 +1258,7 @@ -- Specialize an environment by mapping the generated variables to one. specialize :: Env -> Env specialize (Env (v, r)) =-    Env (S.empty, M.foldWithKey f M.empty r)+    Env (S.empty, foldrWithKey f M.empty r)     where       f x t r = M.insert x (instantiate special t) r       -- Environment mapping generated variables to one@@ -1299,7 +1304,7 @@ matchRenaming :: GenEnv -> Bool matchRenaming (gen, Env (v, e)) =     nonGrp S.empty (M.elems e) &&-    groupMatchRenaming v gen (M.foldWithKey grp M.empty e)+    groupMatchRenaming v gen (foldrWithKey grp M.empty e)     where       nonGrp _ [] = True       nonGrp s (I x:e) =@@ -1334,7 +1339,7 @@    emptyEnv = emptyEnv    instantiate = instantiate    match t t' e = maybe [] (: []) $ match t t' e-   idempotentEnvFor e ts = maybe [] (: []) $ idempotentEnvFor e ts+   identityEnvFor e ts = maybe [] (: []) $ identityEnvFor e ts    specialize = specialize    substitution = substitution    reify = reify
src/CPSA/Lib/Algebra.hs view
@@ -70,10 +70,10 @@     buildable :: Set t -> Set t -> t -> Bool      -- encryptions term returns a list of encryptions carried by the-    -- term, each with the key used to prepare it, with duplicates+    -- term, each with the keys used to prepare it, with duplicates     -- eliminated.  Encryptions that occur in other encryption are     -- later in the list.-    encryptions :: t -> [(t,t)]+    encryptions :: t -> [(t,[t])]      -- protectors derivable target source returns Nothing if target is     -- carried by the source outside of an encryption, where derivable@@ -163,9 +163,9 @@     emptyEnv :: e     instantiate :: e -> t -> t     match :: t -> t -> (g, e) -> [(g, e)]-    -- Can environment be refined so it is idempotent when applied to-    -- some terms?-    idempotentEnvFor :: (g, e) -> [t] -> [(g, e)]+    -- Can environment be refined so it is the identity when applied+    -- to some terms?+    identityEnvFor :: (g, e) -> [t] -> [(g, e)]     -- specialize an environment by eliminating generated variables.     specialize :: e -> e     -- Cast an environment into a substitution
src/CPSA/Lib/Cohort.hs view
@@ -132,12 +132,12 @@ -- 2. for some t in outpred(k', phi(v)), t' is not carried only within --    T in t, or ----- 2a. targetterms(t', T) \ sigma(targetterms(t, esc(k, v, t)) /= empty+-- 3. targetterms(t', T) \ sigma(targetterms(t, esc(k, v, t)) /= empty --    and there are variables in k's protocol that are not atoms, or ----- 3. the decryption key for an element of T is derivable, or+-- 4. the decryption key for an element of T is derivable, or ----- 4. t' is an encryption and the encryption key for t' is derivable.+-- 5. t' is an encryption and the encryption key for t' is derivable. -- -- Haskell variables: -- ct     = t@@ -147,19 +147,19 @@ -- k      = k -- (s, p) = v and n -- subst  = sigma-solved :: Algebra t p g s e c => t -> p -> Maybe t -> Set t ->+solved :: Algebra t p g s e c => t -> p -> [t] -> Set t ->           Preskel t p g s e c -> Node -> s -> Bool-solved ct pos ek escape k (s, p) subst =+solved ct pos eks escape k (s, p) subst =     -- Condition 1     isAncestorInSet escape' t pos ||     -- Condition 2     any (not . carriedOnlyWithin ct' escape') (S.toList ts) ||-    -- Condition 2a.-    not (varsAllAtoms (protocol k)) && not (S.null targetTermsDiff) ||     -- Condition 3-    any (maybe False (derivable a ts) . decryptionKey) (S.toList escape') ||+    not (varsAllAtoms (protocol k)) && not (S.null targetTermsDiff) ||     -- Condition 4-    maybe False (derivable a ts) ek+    any (maybe False (derivable a ts) . decryptionKey) (S.toList escape') ||+    -- Condition 5+    any (derivable a ts) eks     where       v = vertex k (s, p)       -- Look up vertex in k       t = evt id err (event v)  -- Term at v@@ -172,10 +172,10 @@       ts = S.map (evtTerm . event) vs -- Outbound predecessors       (a, _) = avoid k -maybeSolved :: Algebra t p g s e c => t -> p -> Maybe t -> Set t ->+maybeSolved :: Algebra t p g s e c => t -> p -> [t] -> Set t ->                Preskel t p g s e c -> Node -> s -> Bool-maybeSolved ct pos ek escape k n subst =-    not useSolvedFilter || solved ct pos ek escape k n subst+maybeSolved ct pos eks escape k n subst =+    not useSolvedFilter || solved ct pos eks escape k n subst  data Mode = Mode     { noGeneralization :: Bool,@@ -260,7 +260,7 @@     loop cts     where       loop [] = error ("Cohort.testNode missing test at " ++ show n)-      loop ((ct, ek) : cts) =+      loop ((ct, eks) : cts) =           case escapeSet ts derivable ct of             Nothing -> loop cts             Just escape ->@@ -269,17 +269,19 @@                   places [] = loop cts -- Find position at which                   places (p : ps)      -- ct has escaped                       | isAncestorInSet escape t p = places ps-                      | otherwise = solveNode mode k ct p ek n t escape+                      | otherwise = solveNode mode k ct p eks n t escape       cts =                     -- Potential critical messages           if nonceFirstOrder mode then               map f (filter (flip heldBy t) u) ++-              map g (filter h (encryptions t))+              filter g (map h (encryptions t))           else-              map g (filter h (encryptions t)) +++              filter g (map h (encryptions t)) ++               map f (filter (flip heldBy t) u)-      f ct = (ct, Nothing)-      g (ct, ek) = (ct, Just ek)-      h (_, ek) = not (derivable ek)+      f ct = (ct, [])           -- A nonce tests has no eks+      g (_, []) = False         -- An encryption test must have+      g _ = True                -- at least one non-derivable key+      -- Dump derivable encryption keys+      h (ct, eks) = (ct, filter (not . derivable) eks)  -- Compute the escape set escapeSet :: Algebra t p g s e c => Set t ->@@ -306,27 +308,27 @@ -- ct = t @ pos -- t  = msg(k, n) solveNode :: Algebra t p g s e c => Mode -> Preskel t p g s e c ->-             t -> p -> Maybe t -> Node -> t -> Set t ->+             t -> p -> [t] -> Node -> t -> Set t ->              [Preskel t p g s e c]-solveNode mode k ct pos ek n t escape =+solveNode mode k ct pos eks n t escape =     cons ++ augs ++ lsns     where-      cons = contractions k ct pos ek n t escape cause-      augs = augmentations (addDisplacements mode) k ct pos ek n escape cause-      lsns = addListeners k ct pos ek n t escape cause-      cause = Cause (dir ek) n ct escape+      cons = contractions k ct pos eks n t escape cause+      augs = augmentations (addDisplacements mode) k ct pos eks n escape cause+      lsns = addListeners k ct pos eks n t escape cause+      cause = Cause (dir eks) n ct escape  -- Contractions  -- Contract the critical message at the given position. contractions :: Algebra t p g s e c => Preskel t p g s e c ->-                t -> p -> Maybe t -> Node -> t -> Set t ->+                t -> p -> [t] -> Node -> t -> Set t ->                 Cause t p g s e c -> [Preskel t p g s e c]-contractions k ct pos ek n t escape cause =+contractions k ct pos eks n t escape cause =     [ k | let anc = ancestors t pos,           subst <- mgus $ solve escape anc (gen k, emptySubst),           (k, n, subst') <- contract k n cause subst,-          maybeSolved ct pos ek escape k n subst' ]+          maybeSolved ct pos eks escape k n subst' ]  solve :: Algebra t p g s e c => Set t -> [t] -> (g, s) -> [(g, s)] solve escape ancestors subst =@@ -369,29 +371,29 @@           | otherwise = loop substs (subst : acc)       f subst subst' = moreGeneral subst' subst -dir :: Maybe a -> Direction-dir Nothing = Nonce+dir :: [a] -> Direction+dir [] = Nonce dir _ = Encryption  -- Augmentations  augmentations :: Algebra t p g s e c => Bool -> Preskel t p g s e c ->-                t -> p -> Maybe t -> Node -> Set t ->+                t -> p -> [t] -> Node -> Set t ->                 Cause t p g s e c -> [Preskel t p g s e c]-augmentations displacement k ct pos ek n escape cause =+augmentations displacement k ct pos eks n escape cause =     [ k' | r <- roles (protocol k),-           k' <- roleAugs displacement k ct pos ek n escape cause targets r ]+           k' <- roleAugs displacement k ct pos eks n escape cause targets r ]     where       targets = S.toList (targetTerms ct escape)  roleAugs :: Algebra t p g s e c => Bool -> Preskel t p g s e c ->-            t -> p -> Maybe t -> Node -> Set t -> Cause t p g s e c ->+            t -> p -> [t] -> Node -> Set t -> Cause t p g s e c ->             [t] -> Role t p g s e c -> [Preskel t p g s e c]-roleAugs displacement k ct pos ek n escape cause targets role =+roleAugs displacement k ct pos eks n escape cause targets role =     [ k' | (subst', inst) <- transformingNode ct escape targets role subst,            (k', n', subst'') <-                augment displacement k n cause role subst' inst,-           maybeSolved ct pos ek escape k' n' subst'' ]+           maybeSolved ct pos eks escape k' n' subst'' ]     where       subst = cloneRoleVars (gen k) role @@ -506,19 +508,19 @@ -- Listener augmentations  addListeners :: Algebra t p g s e c => Preskel t p g s e c ->-                t -> p -> Maybe t -> Node -> t -> Set t ->+                t -> p -> [t] -> Node -> t -> Set t ->                 Cause t p g s e c -> [Preskel t p g s e c]-addListeners k ct pos ek n t escape cause =-    [ k' | t' <- filter (/= t) (S.toList (escapeKeys ek escape)),+addListeners k ct pos eks n t escape cause =+    [ k' | t' <- filter (/= t) (S.toList (escapeKeys eks escape)),            (k', n', subst) <- addListener k n cause t',-           maybeSolved ct pos ek escape k' n' subst ]+           maybeSolved ct pos eks escape k' n' subst ] -escapeKeys :: Algebra t p g s e c => Maybe t -> Set t -> Set t-escapeKeys ek escape =-    S.fold f e escape+escapeKeys :: Algebra t p g s e c => [t] -> Set t -> Set t+escapeKeys eks escape =+    S.fold f es escape     where       f e s = maybe s (flip S.insert s) (decryptionKey e)-      e = maybe S.empty S.singleton ek+      es = S.fromList eks  -- Maximize a realized skeleton if possible
src/CPSA/Lib/Notation.hs view
@@ -155,6 +155,7 @@  -- (enc a b ... z) => [a, b, ...]z -- (cat a b ... z) => (a, b, ..., z)+-- (hash a b .. z) => #(a, b, ..., z) -- (pubk a) => K(a) -- (invk a) => I(a) -- (privk a) => I(K(a))@@ -170,6 +171,8 @@ mesg indent (L _ (S _ name : xs))      | name == "cat" =          fun indent "" args+     | name == "hash" =+         fun indent "#" args      | name == "pubk" =          fun indent "K" args      | name == "invk" =
src/CPSA/Lib/Strand.hs view
@@ -6,10 +6,6 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -{-# LANGUAGE CPP #-}---- #define EXPERIMENTAL- module CPSA.Lib.Strand (Instance, mkInstance, bldInstance, mkListener,     role, env, trace, height, listenerTerm, Sid, Node, mkPreskel,     firstSkeleton, Pair, Preskel, gen, protocol, insts, orderings,@@ -68,21 +64,29 @@       f (x, t) = (displayTerm (context domain) x,                   displayTerm (context range) t)       context ts = addToContext emptyContext ts++-- Also see showst --}  -- Compile time switches for expermentation. +-- Enable thinning, else use pruning.+useThinning :: Bool+useThinning = False -- True++-- Do not do multistrand thinning.+useSingleStrandThinning :: Bool+useSingleStrandThinning = False -- True++-- Don't use de-origination without thinning although you may want to+-- use thinning without de-origination.+useDeOrigination :: Bool+useDeOrigination = useThinning -- False+ -- Sanity check: ensure no role variable occurs in a skeleton. useCheckVars :: Bool useCheckVars = False -useThinning :: Bool-#if defined EXPERIMENTAL-useThinning = True -- False-#else-useThinning = False -- True-#endif- usePruningDuringCollapsing :: Bool usePruningDuringCollapsing = False -- True @@ -101,13 +105,6 @@ useNoOrigPreservation :: Bool useNoOrigPreservation = False -- True -useDeOrigination :: Bool-#if defined EXPERIMENTAL-useDeOrigination = True -- False-#else-useDeOrigination = False -- True-#endif- -- Instances and Strand Identifiers  -- An Instance is an instance of a role, in the sense that each@@ -226,10 +223,9 @@  listenerTerm :: Algebra t p g s e c => Instance t p g s e c -> Maybe t listenerTerm inst =-    if "" /= rname (role inst) then-        Nothing                 -- Not a listener strand-    else-        Just $ evtTerm (trace inst !! 0)+    case rname (role inst) of+      "" -> Just $ evtTerm (trace inst !! 0) -- Get first term in trace+      _ -> Nothing              -- Not a listener strand  -- Nodes, Pairs, and Graphs @@ -280,9 +276,9 @@     compare n0 n1 = compare (strand n0, pos n0) (strand n1, pos n1)  instance Show (GraphNode e i) where-    showsPrec _ n = let (s, p) = graphNode n in+    showsPrec _ n = let (s, i') = graphNode n in                     showChar '(' . shows s . showString ", " .-                    shows p . showChar ')'+                    shows i' . showChar ')'  -- The node of a vertex graphNode :: GraphNode e i -> Node@@ -319,12 +315,12 @@                   pos <- nats (height (inst strand)) ] |                 (sid, strand) <- zip [0..] strands ]       preds n = map getNode (entry n)-      getNode (s, p) = nodes !! s !! p+      getNode (s, i) = nodes !! s !! i       getEdge (n0, n1) = (getNode n0, getNode n1)       entry n = enrich n [ n0 | (n0, n1) <- pairs, n1 == n ]       -- add strand succession edges-      enrich (s, p) ns-          | p > 0 = (s, p - 1) : ns+      enrich (s, i) ns+          | i > 0 = (s, i - 1) : ns           | otherwise = ns  -- Does start node precede end node?@@ -513,8 +509,8 @@  vertex  :: Algebra t p g s e c => Preskel t p g s e c -> Node ->            Vertex t p g s e c-vertex k (s, p) =-    nodes (strands k !! s) !! p+vertex k (s, i) =+    nodes (strands k !! s) !! i  originationNodes :: Algebra t p g s e c => [Strand t p g s e c] ->                     t -> (t, [Node])@@ -646,7 +642,7 @@           | pos < height (inst strand) =               case lookup (instantiate (env $ inst strand) ru) (korig k) of                 Nothing -> True     -- role term not mapped-                Just ns -> any (\(s, p)-> sid strand == s && p == pos) ns+                Just ns -> any (\(s, i)-> sid strand == s && i == pos) ns           | otherwise = True  -- Isomorphism Check@@ -942,9 +938,9 @@     loop [] orderings     where       loop acc [] = [acc]-      loop acc (p@((s0, p0), (s1, p1)) : ps)+      loop acc (p@((s0, i0), (s1, i1)) : ps)           | s0 /= s1 = loop (p : acc) ps-          | p0 < p1 = loop acc ps+          | i0 < i1 = loop acc ps           | otherwise = [] normalizeOrderings False orderings =     [filter (\ ((s0, _), (s1, _)) -> s0 /= s1) orderings]@@ -953,6 +949,42 @@ updateProb mapping prob =     map (mapping !!) prob +-- Purge a strand.  Used by thinning.  The same as pruning except+-- edges to the purged strand are forwarded as a first step.+purge :: Algebra t p g s e c => PRS t p g s e c ->+            Sid -> Sid -> [PRS t p g s e c]+purge (k0, k, n, phi, hsubst) s s' =+    do+      let perm = updatePerm s s' (strandids k)+      orderings' <- normalizeOrderings False+                    (permuteOrderings perm +                     (forward s (orderings k))) -- Pruning difference+      let k' =+              newPreskel+              (gen k)+              (protocol k)+              (deleteNth s (insts k))+              orderings'+              (knon k)+              (kunique k)+              (operation k)+              (updateProb perm (prob k))+              (pov k)+      k'' <- wellFormedPreskel k'+      return (k0, k'', permuteNode perm n, map (perm !!) phi, hsubst)++-- Forward orderings from strand s+forward :: Sid -> [Pair] -> [Pair]+forward s orderings =+    concatMap f orderings+    where+      f p@((s0, i0), (s1, i1))+          | s0 == s = [((s2, i2), (s1, i1)) | -- Forward here+                       ((s2, i2), (s3, i3)) <- orderings,+                       s3 == s0 && i0 >= i3]+          | s1 == s = []        -- Dump edges to strand s+          | otherwise = [p]     -- Pass thru other edges+ -- Hulling or Ensuring Unique Origination  -- This is the starting point of the Preskeleton Reduction System@@ -964,10 +996,10 @@       -- No uniques originate on more than one strand       loop [] = enrich prune prs       -- Found a pair that needs hulling-      loop ((u, (s, p) : (s', p') : _) : _)+      loop ((u, (s, i) : (s', i') : _) : _)           |  useDeOrigination =               hullByCompressing prune prs s s' ++-              hullByDeOrigination prune prs u (s, p) (s', p')+              hullByDeOrigination prune prs u (s, i) (s', i')           | otherwise =               hullByCompressing prune prs s s'       loop(_ : orig) = loop orig@@ -1014,17 +1046,17 @@  hullByDeOrigination :: Algebra t p g s e c => Bool -> PRS t p g s e c ->                        t -> Node -> Node -> [PRS t p g s e c]-hullByDeOrigination  prune prs u (s, p) (s', p') =+hullByDeOrigination  prune prs u (s, i) (s', i') =     do-      subst <- deOrig (skel prs) u (s, p) ++ deOrig (skel prs) u (s', p')+      subst <- deOrig (skel prs) u (s, i) ++ deOrig (skel prs) u (s', i')       prs <- ksubst False prs subst       hull prune prs  deOrig :: Algebra t p g s e c => Preskel t p g s e c -> t -> Node -> [(g, s)]-deOrig k u (s, p) =+deOrig k u (s, i) =     [ (g, s) |       let tr = trace $ strandInst k s,-      e <- take p tr,+      e <- take i tr,       t <- inbnd e,       subterm <- S.toList $ foldCarriedTerms (flip S.insert) S.empty t,       (g, s) <- unify u subterm (gen k, emptySubst),@@ -1141,8 +1173,8 @@              (trace (strandInst k s))              (trace (strandInst k s'))              (gen k, emptyEnv)-      (gen', env') <- idempotentEnvFor env-                      (concatMap (tterms . trace) $ deleteNth s $ insts k)+      let ts = concatMap (tterms . trace) $ deleteNth s $ insts k+      (gen', env') <- identityEnvFor env ts       case matchRenaming (gen', env') of         True -> return ()         False -> fail ""@@ -1176,6 +1208,8 @@       matchTraces c c' e matchTraces _ _ _ = [] +-- Make sure a substitution does not take a unique out of the set of+-- uniques, and the same for nons. origCheck :: Algebra t p g s e c => Preskel t p g s e c -> e -> Bool origCheck k env =     check (kunique k) && check (knon k)@@ -1185,6 +1219,8 @@       pred set item =           elem (instantiate env item) set +-- Ensure that if (s, p) precedes (s", p"), then (s', p) precedes (s", p")+-- and if (s", p") precedes (s, p), then (s", p") precedes (s', p) precedesCheck :: Algebra t p g s e c => Preskel t p g s e c ->                  Sid -> Sid -> Edge t p g s e c -> Bool precedesCheck k s s' (gn0, gn1)@@ -1192,6 +1228,7 @@     | s == sid (strand gn1) = graphPrecedes gn0 (vertex k (s', pos gn1))     | otherwise = True +-- Experiment strictPrecedesCheck :: Sid -> Sid -> [Pair] -> Bool strictPrecedesCheck s s' pairs =     all (flip elem pairs) before &&@@ -1204,6 +1241,7 @@                  ((s0, i0), n1) <- pairs,                  s0 == s ] +-- Another experiment unboundCheck :: Algebra t p g s e c => Preskel t p g s e c ->               Sid -> Sid -> e -> Bool unboundCheck k s s' env =@@ -1229,36 +1267,49 @@  -- Thinning -#if defined EXPERIMENTAL thin :: Algebra t p g s e c => PRS t p g s e c -> [PRS t p g s e c] thin prs =     thinStrands prs [] $ reverse ss     where                       -- Remove strands in image of POV       ss = filter (\s -> notElem s (prob $ skel prs)) (strandids $ skel prs) +-- Takes a skeleton, a list of pairs of strands that matched, and a+-- list of strands yet to be analyzed, and produces the result of+-- skeletonization.  It first tries single pair thinning, and during+-- that process collects potential multistrand thinning pairs.  Once+-- there are no more unanalyzed strands, it tries multistrand+-- thinning. thinStrands :: Algebra t p g s e c => PRS t p g s e c ->                [(Sid, Sid)] -> [Sid] -> [PRS t p g s e c]-thinStrands prs ps [] =-    case multiPairs ps of+thinStrands prs ps [] =         -- All strands analyzied+    case multiPairs ps of       -- Generate multipairs       [] -> reduce prs-      mps -> thinMany prs mps+      mps -> thinMany prs mps   -- Try multistrand thinning thinStrands prs ps (s:ss) =   thinStrandPairs prs ps s ss ss +-- This loop tries pairs of strands.  Takes a skeleton, a list of+-- pairs of strands that matched but did not thin, a strand to be+-- eliminated, a list of strands to be used in the outer loop+-- (thinStrands), and a list of strands to be considered for matching,+-- and produces the result of skeletonization. thinStrandPairs :: Algebra t p g s e c => PRS t p g s e c -> [(Sid, Sid)] ->                    Sid -> [Sid] -> [Sid] -> [PRS t p g s e c] thinStrandPairs prs ps _ ss [] =   thinStrands prs ps ss thinStrandPairs prs ps s ss (s':ss') =   case thinStrand prs s s' of-    Nothing -> thinStrandPairs prs ps s ss ss' -- Try next pair-    -- Try next pair saving this pair+    -- Try next pair, there was no match+    Nothing -> thinStrandPairs prs ps s ss ss'+    -- Try next pair, there was a match so save this pair     Just [] -> thinStrandPairs prs ((s, s'):ps) s ss ss'-    Just prss ->                -- Success+    Just prss ->                -- Success at single strand thinning       do         prs <- prss-        thin prs+        thin prs                -- Restart from the beginning +-- Try thinning s with s'.  If there was no match, return Nothing,+-- else return Just the list of results. thinStrand :: Algebra t p g s e c => PRS t p g s e c ->               Sid -> Sid -> Maybe [PRS t p g s e c] thinStrand prs s s' =@@ -1267,24 +1318,32 @@       [] -> Nothing       ges ->           Just $ do-            (gen, env) <- ges+            e <- ges+            (gen, env) <- thinStrandCheck k s e             [ prs' | prs <- ksubst False prs (gen, substitution env),-                     prs' <- compress False prs s s',-                     prs'' <- compress False prs s' s,+                     prs' <- purge prs s s',+                     prs'' <- purge prs s' s,                      gist (skel prs') == gist (skel prs'')] +-- See if two strands match. thinStrandMatch :: Algebra t p g s e c => Preskel t p g s e c ->                    Sid -> Sid -> (g, e) -> [(g, e)]-thinStrandMatch k s s' env0 =+thinStrandMatch k s s' env =   do     let i = strandInst k s     let i' = strandInst k s'     case height i /= height i' of       True -> fail ""       False -> return ()-    env <- matchTraces (trace i) (trace i') env0-    (gen', env') <- idempotentEnvFor env-                    (concatMap (tterms . trace) $ deleteNth s $ insts k)+    matchTraces (trace i) (trace i') env++-- Do the identity, renaming, and origination check.+thinStrandCheck :: Algebra t p g s e c => Preskel t p g s e c ->+                   Sid -> (g, e) -> [(g, e)]+thinStrandCheck k s env =+  do+    let ts = concatMap (tterms . trace) $ deleteNth s $ insts k+    (gen', env') <- identityEnvFor env ts     case matchRenaming (gen', env') of       True -> return ()       False -> fail ""@@ -1292,25 +1351,32 @@       True -> return (gen', env')       False -> fail "" +-- Multistrand thinning++-- Generate all candidate pairings multiPairs :: [(Sid, Sid)] ->  [[(Sid, Sid)]]+multiPairs _ | useSingleStrandThinning = [] multiPairs ps = filter atLeastTwo $ thinOne ps +-- List is of length at least two. atLeastTwo :: [a] -> Bool atLeastTwo (_:_:_) = True atLeastTwo _ = False  thinOne :: [(Sid, Sid)] -> [[(Sid, Sid)]] thinOne [] = []-thinOne (s:ss) =-    thinTwo s ss ++ thinOne ss+thinOne (p:ps) =+    thinTwo p ps ++ thinOne ps +-- Construct possible pairs that include (s, s'). thinTwo :: (Sid, Sid) -> [(Sid, Sid)] -> [[(Sid, Sid)]]-thinTwo (s, s') ss =-    [(s, s')] : [(s, s') : ss' | ss' <- thinOne (filter (diff (s, s')) ss)]-    where+thinTwo (s, s') ps =+    [(s, s')] : [(s, s') : ps' | ps' <- thinOne (filter (diff (s, s')) ps)]+    where                       -- filter out pairs with seen strands       diff (s0, s1) (s2, s3) =           s0 /= s2 && s0 /= s3 && s1 /= s2 && s1 /= s3 +-- Try all multistrand pairings until one succeeds. thinMany :: Algebra t p g s e c => PRS t p g s e c ->             [[(Sid, Sid)]] -> [PRS t p g s e c] thinMany prs [] = reduce prs@@ -1336,14 +1402,33 @@ thinManyMatch :: Algebra t p g s e c => Preskel t p g s e c ->                 [(Sid, Sid)] -> [(g, e)] thinManyMatch k ps =-    foldM (\e (s, s') -> thinStrandMatch k s s' e) (gen k, emptyEnv) ps+    do+      let f e (s, s') = thinStrandMatch k s s' e+      env <- foldM f (gen k, emptyEnv) ps+      let ss = concatMap (\(s, s') -> [s, s']) ps+      let ts = concatMap (tterms . trace) $ deleteMany ss $ insts k+      (gen', env') <- identityEnvFor env ts+      case matchRenaming (gen', env') of+        True -> return ()+        False -> fail ""+      case origCheck k env' of+        True -> return (gen', env')+        False -> fail "" +deleteMany :: [Int] -> [a] -> [a]+deleteMany nums xs =+    loop 0 xs+    where+      loop _ [] = []+      loop n (x:xs) | elem n nums = loop (n + 1) xs+                    | otherwise = x : loop (n + 1) xs+ compressMany :: Algebra t p g s e c => PRS t p g s e c ->                 [(Sid, Sid)] -> [PRS t p g s e c] compressMany prs [] = [prs] compressMany prs ((s, s'):ps) =     do-      prs' <- compress False prs s s'+      prs' <- purge prs s s'       compressMany prs' (map (updatePairs s s') ps)  swap :: [(a, a)] -> [(a, a)]@@ -1353,57 +1438,7 @@ updatePairs :: Sid -> Sid -> (Sid, Sid) -> (Sid, Sid) updatePairs old new (s, s') =     (updateStrand old new s, updateStrand old new s')-#else-thin :: Algebra t p g s e c => PRS t p g s e c -> [PRS t p g s e c]-thin prs =-    thinStrands prs $ reverse ss-    where                       -- Remove strands in image of POV-      ss = filter (\s -> notElem s (prob $ skel prs)) (strandids $ skel prs) -thinStrands :: Algebra t p g s e c => PRS t p g s e c ->-               [Sid] -> [PRS t p g s e c]-thinStrands prs [] =-  reduce prs-thinStrands prs (s:ss) =-  thinStrandPairs prs s ss ss--thinStrandPairs :: Algebra t p g s e c => PRS t p g s e c ->-                   Sid -> [Sid] -> [Sid] -> [PRS t p g s e c]-thinStrandPairs prs _ ss [] =-  thinStrands prs ss-thinStrandPairs prs s ss (s':ss') =-  case thinStrand prs s s' of-    [] -> thinStrandPairs prs s ss ss' -- Try next pair-    prss ->                           -- Success-      do-        prs <- prss-        thin prs--thinStrand :: Algebra t p g s e c => PRS t p g s e c ->-              Sid -> Sid -> [PRS t p g s e c]-thinStrand prs s s' =-  do-    let k = skel prs-    let i = strandInst k s-    let i' = strandInst k s'-    case height i /= height i' of-      True -> fail ""-      False -> return ()-    env <- matchTraces (trace i) (trace i') (gen k, emptyEnv)-    (gen', env') <- idempotentEnvFor env-                    (concatMap (tterms . trace) $ deleteNth s $ insts k)-    case matchRenaming (gen', env') of-      True -> return ()-      False -> fail ""-    case origCheck k env' of-      True -> return ()-      False -> fail ""-    [ prs' | prs <- ksubst False prs (gen', substitution env'),-             prs' <- compress False prs s s',-             prs'' <- compress False prs s' s,-             gist (skel prs') == gist (skel prs'')]-#endif- -- Transitive Reduction  -- An edge is essential if its removal eliminates all paths from its@@ -1718,21 +1753,21 @@       deleteOrdering (n0@(s0, _), n1@(s1, _))           | s == s0 || s == s1 = []           | otherwise = [(adjust n0, adjust n1)]-      adjust n@(s', p')-          | s' > s = (s' - 1, p')+      adjust n@(s', i')+          | s' > s = (s' - 1, i')           | otherwise = n  -- Update orderings when a strand is shortened (p > 0) shortenOrderings :: Node -> [Pair] -> [Pair]-shortenOrderings (s, p) ps =+shortenOrderings (s, i) ps =     do       pair <- ps       shortenOrdering pair     where-      shortenOrdering (n0@(s0, p0), n1@(s1, p1))-          | s == s0 && p <= p0 = []-          | s == s1 && p <= p1 = []-          | otherwise = [(n0, n1)]+      shortenOrdering p@((s0, i0), (s1, i1))+          | s == s0 && i <= i0 = []+          | s == s1 && i <= i1 = []+          | otherwise = [p]  deleteNodeRest :: Algebra t p g s e c => Preskel t p g s e c ->                   g -> Node -> [Instance t p g s e c] -> [Pair] ->
src/CPSA/SimpleDiffieHellman/Algebra.hs view
@@ -15,7 +15,7 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiParamTypeClasses, CPP #-}  module CPSA.SimpleDiffieHellman.Algebra (name, origin) where @@ -29,6 +29,14 @@ import qualified CPSA.Lib.CPSA as C import CPSA.Lib.CPSA (SExpr(..), Pos, annotation) +-- Preserve the ability to use GHC 6.x+foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b+#if defined __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ < 700+foldrWithKey = M.foldWithKey+#else+foldrWithKey = M.foldrWithKey+#endif+ name :: String name = "diffie-hellman" @@ -69,6 +77,8 @@ -- -- Subsorts: text, data, name, skey, akey, base, expn < mesg --+-- Note that both mesg and base are not base sorts.+-- -- Operations: --   cat : mesg X mesg -> mesg               Pairing --   enc : mesg X mesg -> mesg               Encryption@@ -316,7 +326,7 @@ isAtom :: Term -> Bool isAtom (I _) = False isAtom (C _) = False-isAtom (F s _) =+isAtom (F s _) =                -- Note Base is not a base sort!     s == Text || s == Data || s == Name ||     s == Skey || s == Akey || s == Expn @@ -464,22 +474,20 @@ -- encryption key.  Note that a hash is treated as a kind of -- encryption in which the term that is hashed is the encryption key. -- (This needs more work.)-encryptions :: Term -> [(Term, Term)]+encryptions :: Term -> [(Term, [Term])] encryptions t =     reverse $ loop t []     where       loop (F Cat [t, t']) acc =           loop t' (loop t acc)       loop t@(F Enc [t', t'']) acc =-          loop t' (adjoin (t, t'') acc)+          loop t' (adjoin (t, [t'']) acc)       loop t@(F Hash [t']) acc =-          adjoin (t, t') acc-      loop t@(F Base [F Exp [F Exp [t', t''], t''']]) acc =-          adjoin (e, F Expn [t'']) (adjoin (t, F Expn [t''']) acc)-          where-            e = F Base [F Exp [F Exp [t', t'''], t'']]+          adjoin (t, [t']) acc+      loop t@(F Base [F Exp [F Exp [_, t'], t'']]) acc =+          adjoin (t, [F Expn [t'], F Expn [t'']]) acc       loop t@(F Base [F Exp [t', t'']]) acc =-          loop (F Base [t']) (adjoin (t, F Expn [t'']) acc)+          loop (F Base [t']) (adjoin (t, [F Expn [t'']]) acc)       loop _ acc = acc       adjoin x xs           | x `elem` xs = xs@@ -895,16 +903,13 @@       Nothing -> [(g, Env $ M.insert x t r)]       Just t' -> if t == t' then [(g, Env r)] else [] match (C c) (C c') r = if c == c' then [r] else []-match (F Invk [I x]) (F Pubk [I y]) r =-    match (I x) (F Invk [F Pubk [I y]]) r-match (F Invk [I x]) (F Pubk [C c, I y]) r =-    match (I x) (F Invk [F Pubk [C c, I y]]) r match (F Exp [x, y]) (F Exp [F Exp [u, v], w]) r =     matchLists [x, y] [F Exp [u, v], w] r ++     matchLists [x, y] [F Exp [u, w], v] r match (F s u) (F s' u') r     | s == s' = matchLists u u' r-    | otherwise = []+match (F Invk [t]) t' r =+    match t (F Invk [t']) r match _ _ _ = []  matchLists :: [Term] -> [Term] -> GenEnv -> [GenEnv]@@ -917,11 +922,11 @@  -- Does every varible in ts not occur in the domain of e? -- Trivial bindings in e are ignored.-idempotentEnvFor :: Env -> [Term] -> Bool-idempotentEnvFor (Env r) ts =+identityEnvFor :: Env -> [Term] -> Bool+identityEnvFor (Env r) ts =     all (allId $ flip S.notMember dom) ts     where-      dom = M.foldWithKey f S.empty r -- The domain of r+      dom = foldrWithKey f S.empty r -- The domain of r       f x (I y) dom           | x == y = dom        -- Ignore trivial bindings           | otherwise = S.insert x dom@@ -981,8 +986,8 @@    emptyEnv = emptyEnv    instantiate = instantiate    match = match-   idempotentEnvFor (g, e) ts =-       if idempotentEnvFor e ts then+   identityEnvFor (g, e) ts =+       if identityEnvFor e ts then            [(g, e)]        else            []
tst/DH_hack.tst view
@@ -1,6 +1,6 @@ (herald "DH Hack" (bound 15)) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read") (comment "Strand count bounded at 15")
tst/blanchet.tst view
@@ -1,7 +1,7 @@ (herald "Blanchet's Simple Example Protocol"   (comment "There is a flaw in this protocol by design")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol blanchet basic
tst/completeness-test.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol completeness-test basic
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol crushing basic
tst/dass_simple.tst view
@@ -1,6 +1,6 @@ (herald "Distributed Authentication Security Service Protocol Variants") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol dass-simple basic
tst/denning-sacco.tst view
@@ -1,6 +1,6 @@ (herald "Denning-Sacco Protocol") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol denning-sacco basic
tst/deorig_contract.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol deorig-contract basic
tst/deorig_mesg.tst view
@@ -1,6 +1,6 @@ (herald deorig-mesg) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol deorig-mesg basic
tst/deorig_simple.tst view
@@ -1,6 +1,6 @@ (herald deorig-simple) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol deorig-simple basic
tst/dh_cert.tst view
@@ -1,6 +1,6 @@ (herald "Diffie-Hellman with Certificate" (algebra diffie-hellman)) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol dh-cert diffie-hellman@@ -569,7 +569,7 @@   (label 7)   (parent 4)   (unrealized (3 0))-  (comment "1 in cohort - 1 not yet seen"))+  (comment "2 in cohort - 2 not yet seen"))  (defskeleton dh-cert   (vars (ca a b name) (gy base) (as-ltv bs-ltv expn))@@ -610,7 +610,7 @@       (send (cat (exp (gen) as-ltv) (exp gy as-ltv)))))   (label 8)   (parent 5)-  (seen 13)+  (seen 14)   (unrealized (2 0))   (comment "5 in cohort - 2 not yet seen")) @@ -652,7 +652,7 @@       (send (cat (exp (gen) x) (exp gy as-ltv)))))   (label 9)   (parent 5)-  (seen 13 15)+  (seen 14 16)   (unrealized (2 0))   (comment "5 in cohort - 2 not yet seen")) @@ -831,6 +831,96 @@   (comment "empty cohort"))  (defskeleton dh-cert+  (vars (ca a b name) (as-ltv bs-ltv x y expn))+  (defstrand init 4 (a a) (b b) (ca ca) (gB (exp (gen) bs-ltv))+    (gy (exp (gen) y)) (as-ltv as-ltv) (bs-ltv bs-ltv) (x x))+  (defstrand resp 4 (a a) (b b) (ca ca) (gA (exp (gen) as-ltv))+    (gx (exp (gen) x)) (bs-ltv bs-ltv) (as-ltv as-ltv) (y y))+  (deflistener+    (enc "hash"+      (cat (exp (exp (gen) bs-ltv) x) (exp (exp (gen) as-ltv) y))))+  (deflistener+    (cat (exp (exp (gen) bs-ltv) x) (exp (exp (gen) as-ltv) y)))+  (deflistener x)+  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((1 1) (3 0))+    ((1 3) (0 3)) ((2 1) (1 2)) ((3 1) (2 0)) ((4 1) (3 0)))+  (non-orig (privk ca))+  (uniq-orig as-ltv bs-ltv x y)+  (operation encryption-test (added-listener x)+    (exp (exp (gen) bs-ltv) x) (3 0))+  (traces+    ((send+       (cat (exp (gen) as-ltv)+         (enc "cert" a (exp (gen) as-ltv) (privk "certify" ca))+         (exp (gen) x)))+      (recv+        (cat (exp (gen) bs-ltv)+          (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca))+          (exp (gen) y)))+      (send+        (enc "tag1"+          (cat (exp (gen) as-ltv)+            (enc "cert" a (exp (gen) as-ltv) (privk "certify" ca))+            (exp (gen) x)) (exp (gen) bs-ltv)+          (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca))+          (exp (gen) y)+          (enc "hash"+            (cat (exp (exp (gen) bs-ltv) x)+              (exp (exp (gen) as-ltv) y)))))+      (recv+        (enc "tag2"+          (cat (exp (gen) as-ltv)+            (enc "cert" a (exp (gen) as-ltv) (privk "certify" ca))+            (exp (gen) x)) (exp (gen) bs-ltv)+          (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca))+          (exp (gen) y)+          (enc "hash"+            (cat (exp (exp (gen) bs-ltv) x)+              (exp (exp (gen) as-ltv) y))))))+    ((recv+       (cat (exp (gen) as-ltv)+         (enc "cert" a (exp (gen) as-ltv) (privk "certify" ca))+         (exp (gen) x)))+      (send+        (cat (exp (gen) bs-ltv)+          (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca))+          (exp (gen) y)))+      (recv+        (enc "tag1"+          (cat (exp (gen) as-ltv)+            (enc "cert" a (exp (gen) as-ltv) (privk "certify" ca))+            (exp (gen) x)) (exp (gen) bs-ltv)+          (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca))+          (exp (gen) y)+          (enc "hash"+            (cat (exp (exp (gen) bs-ltv) x)+              (exp (exp (gen) as-ltv) y)))))+      (send+        (enc "tag2"+          (cat (exp (gen) as-ltv)+            (enc "cert" a (exp (gen) as-ltv) (privk "certify" ca))+            (exp (gen) x)) (exp (gen) bs-ltv)+          (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca))+          (exp (gen) y)+          (enc "hash"+            (cat (exp (exp (gen) bs-ltv) x)+              (exp (exp (gen) as-ltv) y))))))+    ((recv+       (enc "hash"+         (cat (exp (exp (gen) bs-ltv) x) (exp (exp (gen) as-ltv) y))))+      (send+        (enc "hash"+          (cat (exp (exp (gen) bs-ltv) x) (exp (exp (gen) as-ltv) y)))))+    ((recv (cat (exp (exp (gen) bs-ltv) x) (exp (exp (gen) as-ltv) y)))+      (send+        (cat (exp (exp (gen) bs-ltv) x) (exp (exp (gen) as-ltv) y))))+    ((recv x) (send x)))+  (label 13)+  (parent 7)+  (unrealized (3 0) (4 0))+  (comment "empty cohort"))++(defskeleton dh-cert   (vars (ca a b name) (as-ltv bs-ltv expn))   (defstrand init 4 (a a) (b b) (ca ca) (gB (gen)) (gy (gen))     (as-ltv as-ltv) (bs-ltv bs-ltv) (x as-ltv))@@ -867,7 +957,7 @@       (send (enc "hash" (cat (exp (gen) as-ltv) (exp (gen) as-ltv)))))     ((recv (cat (exp (gen) as-ltv) (exp (gen) as-ltv)))       (send (cat (exp (gen) as-ltv) (exp (gen) as-ltv)))))-  (label 13)+  (label 14)   (parent 8)   (unrealized)   (comment "1 in cohort - 1 not yet seen"))@@ -911,7 +1001,7 @@     ((recv (cat (exp (gen) as-ltv) (exp gy as-ltv)))       (send (cat (exp (gen) as-ltv) (exp gy as-ltv))))     ((recv as-ltv) (send as-ltv)))-  (label 14)+  (label 15)   (parent 8)   (unrealized (3 0))   (comment "empty cohort"))@@ -953,7 +1043,7 @@       (send (enc "hash" (cat (exp (gen) x) (exp (gen) as-ltv)))))     ((recv (cat (exp (gen) x) (exp (gen) as-ltv)))       (send (cat (exp (gen) x) (exp (gen) as-ltv)))))-  (label 15)+  (label 16)   (parent 9)   (unrealized)   (comment "1 in cohort - 1 not yet seen"))@@ -997,7 +1087,7 @@     ((recv (cat (exp (gen) x) (exp gy as-ltv)))       (send (cat (exp (gen) x) (exp gy as-ltv))))     ((recv as-ltv) (send as-ltv)))-  (label 16)+  (label 17)   (parent 9)   (unrealized (3 0))   (comment "empty cohort"))@@ -1038,7 +1128,7 @@           (enc "hash"             (cat (exp (exp (gen) bs-ltv) x)               (exp (exp (gen) as-ltv) y)))))))-  (label 17)+  (label 18)   (parent 11)   (unrealized)   (origs (as-ltv (0 0)) (x (0 0)))@@ -1077,8 +1167,8 @@           (enc "hash" (cat (exp (gen) as-ltv) (exp (gen) as-ltv))))))     ((recv (cat (exp (gen) as-ltv) (exp (gen) as-ltv)))       (send (cat (exp (gen) as-ltv) (exp (gen) as-ltv)))))-  (label 18)-  (parent 13)+  (label 19)+  (parent 14)   (unrealized)   (comment "1 in cohort - 1 not yet seen")) @@ -1115,8 +1205,8 @@           (enc "hash" (cat (exp (gen) x) (exp (gen) as-ltv))))))     ((recv (cat (exp (gen) x) (exp (gen) as-ltv)))       (send (cat (exp (gen) x) (exp (gen) as-ltv)))))-  (label 19)-  (parent 15)+  (label 20)+  (parent 16)   (unrealized)   (comment "1 in cohort - 1 not yet seen")) @@ -1156,8 +1246,8 @@           (enc "hash"             (cat (exp (exp (gen) bs-ltv) x)               (exp (exp (gen) as-ltv) y)))))))-  (label 20)-  (parent 17)+  (label 21)+  (parent 18)   (unrealized)   (shape)   (maps@@ -1195,9 +1285,9 @@             (exp (gen) as-ltv)) (gen)           (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca)) (gen)           (enc "hash" (cat (exp (gen) as-ltv) (exp (gen) as-ltv)))))))-  (label 21)-  (parent 18)-  (seen 22)+  (label 22)+  (parent 19)+  (seen 23)   (unrealized)   (origs (as-ltv (0 0)))   (comment "1 in cohort - 0 not yet seen"))@@ -1231,8 +1321,8 @@             (exp (gen) x)) (gen)           (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca)) (gen)           (enc "hash" (cat (exp (gen) x) (exp (gen) as-ltv)))))))-  (label 22)-  (parent 19)+  (label 23)+  (parent 20)   (unrealized)   (shape)   (maps@@ -1325,7 +1415,7 @@           (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca))           (exp (gen) y)           (enc "hash" (cat (exp gx bs-ltv) (exp gA y)))))))-  (label 23)+  (label 24)   (unrealized (0 2))   (origs (y (0 1)) (bs-ltv (0 1)))   (comment "2 in cohort - 2 not yet seen"))@@ -1396,8 +1486,8 @@           (enc "hash"             (cat (exp (exp (gen) bs-ltv) x)               (exp (exp (gen) as-ltv) y)))))))-  (label 24)-  (parent 23)+  (label 25)+  (parent 24)   (unrealized)   (comment "1 in cohort - 1 not yet seen")) @@ -1439,8 +1529,8 @@           (exp (gen) y) (enc "hash" (cat (exp gx bs-ltv) (exp gA y))))))     ((recv (enc "hash" (cat (exp gx bs-ltv) (exp gA y))))       (send (enc "hash" (cat (exp gx bs-ltv) (exp gA y))))))-  (label 25)-  (parent 23)+  (label 26)+  (parent 24)   (unrealized (1 0))   (comment "1 in cohort - 1 not yet seen")) @@ -1480,8 +1570,8 @@           (enc "hash"             (cat (exp (exp (gen) bs-ltv) x)               (exp (exp (gen) as-ltv) y)))))))-  (label 26)-  (parent 24)+  (label 27)+  (parent 25)   (unrealized)   (origs (y (0 1)) (bs-ltv (0 1)))   (comment "1 in cohort - 1 not yet seen"))@@ -1522,9 +1612,9 @@       (send (enc "hash" (cat (exp gx bs-ltv) (exp gA y)))))     ((recv (cat (exp gx bs-ltv) (exp gA y)))       (send (cat (exp gx bs-ltv) (exp gA y)))))-  (label 27)-  (parent 25)-  (seen 29 30)+  (label 28)+  (parent 26)+  (seen 30 31)   (unrealized (2 0))   (comment "5 in cohort - 3 not yet seen")) @@ -1564,8 +1654,8 @@           (enc "hash"             (cat (exp (exp (gen) bs-ltv) x)               (exp (exp (gen) as-ltv) y)))))))-  (label 28)-  (parent 26)+  (label 29)+  (parent 27)   (unrealized)   (origs (y (0 1)) (bs-ltv (0 1)))   (comment "1 in cohort - 1 not yet seen"))@@ -1607,9 +1697,9 @@       (send (enc "hash" (cat (exp (gen) bs-ltv) (exp gA y)))))     ((recv (cat (exp (gen) bs-ltv) (exp gA y)))       (send (cat (exp (gen) bs-ltv) (exp gA y)))))-  (label 29)-  (parent 27)-  (seen 33 34)+  (label 30)+  (parent 28)+  (seen 34 35)   (unrealized (2 0))   (comment "5 in cohort - 3 not yet seen")) @@ -1650,9 +1740,9 @@       (send (enc "hash" (cat (exp (gen) bs-ltv) (exp gA bs-ltv)))))     ((recv (cat (exp (gen) bs-ltv) (exp gA bs-ltv)))       (send (cat (exp (gen) bs-ltv) (exp gA bs-ltv)))))-  (label 30)-  (parent 27)-  (seen 33)+  (label 31)+  (parent 28)+  (seen 34)   (unrealized (2 0))   (comment "5 in cohort - 1 not yet seen")) @@ -1693,8 +1783,8 @@     ((recv (cat (exp gx bs-ltv) (exp gA y)))       (send (cat (exp gx bs-ltv) (exp gA y))))     ((recv bs-ltv) (send bs-ltv)))-  (label 31)-  (parent 27)+  (label 32)+  (parent 28)   (unrealized (2 0) (3 0))   (comment "empty cohort")) @@ -1734,8 +1824,8 @@           (enc "hash"             (cat (exp (exp (gen) bs-ltv) x)               (exp (exp (gen) as-ltv) y)))))))-  (label 32)-  (parent 28)+  (label 33)+  (parent 29)   (unrealized)   (origs (y (0 1)) (bs-ltv (0 1)))   (comment "1 in cohort - 1 not yet seen"))@@ -1779,8 +1869,8 @@       (send (enc "hash" (cat (exp (gen) bs-ltv) (exp (gen) bs-ltv)))))     ((recv (cat (exp (gen) bs-ltv) (exp (gen) bs-ltv)))       (send (cat (exp (gen) bs-ltv) (exp (gen) bs-ltv)))))-  (label 33)-  (parent 29)+  (label 34)+  (parent 30)   (unrealized)   (comment "1 in cohort - 1 not yet seen")) @@ -1822,8 +1912,8 @@       (send (enc "hash" (cat (exp (gen) bs-ltv) (exp (gen) y)))))     ((recv (cat (exp (gen) bs-ltv) (exp (gen) y)))       (send (cat (exp (gen) bs-ltv) (exp (gen) y)))))-  (label 34)-  (parent 29)+  (label 35)+  (parent 30)   (unrealized)   (comment "1 in cohort - 1 not yet seen")) @@ -1864,8 +1954,8 @@       (send (enc "hash" (cat (exp (gen) bs-ltv) (exp gA y)))))     ((recv (cat (exp (gen) bs-ltv) (exp gA y)))       (send (cat (exp (gen) bs-ltv) (exp gA y)))) ((recv y) (send y)))-  (label 35)-  (parent 29)+  (label 36)+  (parent 30)   (unrealized (3 0))   (comment "empty cohort")) @@ -1908,8 +1998,8 @@     ((recv (cat (exp (gen) bs-ltv) (exp gA bs-ltv)))       (send (cat (exp (gen) bs-ltv) (exp gA bs-ltv))))     ((recv bs-ltv) (send bs-ltv)))-  (label 36)-  (parent 30)+  (label 37)+  (parent 31)   (unrealized (3 0))   (comment "empty cohort")) @@ -1949,8 +2039,8 @@           (enc "hash"             (cat (exp (exp (gen) bs-ltv) x)               (exp (exp (gen) as-ltv) y)))))))-  (label 37)-  (parent 32)+  (label 38)+  (parent 33)   (unrealized)   (shape)   (maps@@ -1994,8 +2084,8 @@           (enc "hash" (cat (exp (gen) bs-ltv) (exp (gen) bs-ltv))))))     ((recv (cat (exp (gen) bs-ltv) (exp (gen) bs-ltv)))       (send (cat (exp (gen) bs-ltv) (exp (gen) bs-ltv)))))-  (label 38)-  (parent 33)+  (label 39)+  (parent 34)   (unrealized)   (comment "1 in cohort - 1 not yet seen")) @@ -2034,8 +2124,8 @@           (enc "hash" (cat (exp (gen) bs-ltv) (exp (gen) y))))))     ((recv (cat (exp (gen) bs-ltv) (exp (gen) y)))       (send (cat (exp (gen) bs-ltv) (exp (gen) y)))))-  (label 39)-  (parent 34)+  (label 40)+  (parent 35)   (unrealized)   (comment "1 in cohort - 1 not yet seen")) @@ -2070,9 +2160,9 @@           (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca))           (exp (gen) bs-ltv)           (enc "hash" (cat (exp (gen) bs-ltv) (exp (gen) bs-ltv)))))))-  (label 40)-  (parent 38)-  (seen 41)+  (label 41)+  (parent 39)+  (seen 42)   (unrealized)   (origs (bs-ltv (0 1)))   (comment "1 in cohort - 0 not yet seen"))@@ -2108,8 +2198,8 @@           (enc "cert" b (exp (gen) bs-ltv) (privk "certify" ca))           (exp (gen) y)           (enc "hash" (cat (exp (gen) bs-ltv) (exp (gen) y)))))))-  (label 41)-  (parent 39)+  (label 42)+  (parent 40)   (unrealized)   (shape)   (maps
tst/dhke.tst view
@@ -1,6 +1,6 @@ (herald "Diffie-Hellman Key Exchange" (algebra diffie-hellman)) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol dhke diffie-hellman@@ -107,13 +107,39 @@   (label 3)   (parent 1)   (unrealized (2 0))-  (comment "1 in cohort - 1 not yet seen"))+  (comment "2 in cohort - 2 not yet seen"))  (defskeleton dhke   (vars (a b name) (x y expn))   (defstrand resp 3 (a a) (b b) (x x) (y y))   (defstrand init 1 (a a) (x x))   (deflistener (exp (exp (gen) x) y))+  (deflistener x)+  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 1) (0 2))+    ((3 1) (2 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig x y)+  (operation encryption-test (added-listener x) (exp (exp (gen) x) y)+    (2 0))+  (traces+    ((recv (enc "i" (exp (gen) x) (privk a)))+      (send+        (cat (enc (exp (gen) y) (privk b))+          (enc a b (exp (exp (gen) x) y))))+      (recv (enc "i" a b (exp (exp (gen) x) y))))+    ((send (enc "i" (exp (gen) x) (privk a))))+    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+    ((recv x) (send x)))+  (label 4)+  (parent 3)+  (unrealized (3 0))+  (comment "empty cohort"))++(defskeleton dhke+  (vars (a b name) (x y expn))+  (defstrand resp 3 (a a) (b b) (x x) (y y))+  (defstrand init 1 (a a) (x x))+  (deflistener (exp (exp (gen) x) y))   (deflistener y)   (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((2 1) (0 2)) ((3 1) (2 0)))   (non-orig (privk a) (privk b))@@ -129,7 +155,7 @@     ((send (enc "i" (exp (gen) x) (privk a))))     ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))     ((recv y) (send y)))-  (label 4)+  (label 5)   (parent 3)   (unrealized (3 0))   (comment "empty cohort"))@@ -164,7 +190,7 @@       (recv         (cat (enc (exp (gen) y) (privk b))           (enc a b (exp (exp (gen) x) y))))))-  (label 5)+  (label 6)   (unrealized (0 1))   (origs (x (0 0)))   (comment "1 in cohort - 1 not yet seen"))@@ -187,9 +213,9 @@       (send         (cat (enc (exp (gen) y) (privk b))           (enc a-0 b (exp (exp (gen) y) x-0))))))-  (label 6)-  (parent 5)-  (seen 7)+  (label 7)+  (parent 6)+  (seen 8)   (unrealized (0 1))   (comment "3 in cohort - 2 not yet seen")) @@ -211,8 +237,8 @@       (send         (cat (enc (exp (gen) y) (privk b))           (enc a b (exp (exp (gen) x) y))))))-  (label 7)-  (parent 6)+  (label 8)+  (parent 7)   (unrealized)   (shape)   (maps ((0) ((a a) (b b) (x x) (y y))))@@ -238,10 +264,10 @@         (cat (enc (exp (gen) y) (privk b))           (enc a-0 b (exp (exp (gen) y) x-0)))))     ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y))))-  (label 8)-  (parent 6)+  (label 9)+  (parent 7)   (unrealized (2 0))-  (comment "1 in cohort - 1 not yet seen"))+  (comment "2 in cohort - 2 not yet seen"))  (defskeleton dhke   (vars (a b a-0 name) (x y x-0 expn))@@ -265,11 +291,38 @@           (enc a-0 b (exp (exp (gen) y) x-0)))))     ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))     ((recv x) (send x)))-  (label 9)-  (parent 8)+  (label 10)+  (parent 9)   (unrealized (3 0))   (comment "empty cohort")) +(defskeleton dhke+  (vars (a b a-0 name) (x y x-0 expn))+  (defstrand init 2 (a a) (b b) (x x) (y y))+  (defstrand resp 2 (a a-0) (b b) (x x-0) (y y))+  (deflistener (exp (exp (gen) x) y))+  (deflistener y)+  (precedes ((0 0) (2 0)) ((1 1) (3 0)) ((2 1) (0 1)) ((3 1) (2 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig x y)+  (operation encryption-test (added-listener y) (exp (exp (gen) x) y)+    (2 0))+  (traces+    ((send (enc "i" (exp (gen) x) (privk a)))+      (recv+        (cat (enc (exp (gen) y) (privk b))+          (enc a b (exp (exp (gen) x) y)))))+    ((recv (enc "i" (exp (gen) x-0) (privk a-0)))+      (send+        (cat (enc (exp (gen) y) (privk b))+          (enc a-0 b (exp (exp (gen) y) x-0)))))+    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+    ((recv y) (send y)))+  (label 11)+  (parent 9)+  (unrealized (3 0))+  (comment "empty cohort"))+ (comment "Nothing left to do")  (defprotocol dh-mim diffie-hellman@@ -294,7 +347,7 @@   (traces     ((send (exp (gen) x)) (recv (exp (gen) y))       (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n)))-  (label 10)+  (label 12)   (unrealized (1 0))   (preskeleton)   (comment "Not a skeleton"))@@ -308,8 +361,8 @@   (traces     ((send (exp (gen) x)) (recv (exp (gen) y))       (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n)))-  (label 11)-  (parent 10)+  (label 13)+  (parent 12)   (unrealized)   (shape)   (maps ((0 1) ((n n) (x x) (y y))))@@ -340,7 +393,7 @@     ((recv (enc "i" h (privk a)))       (send (cat (enc (exp (gen) y) (privk b)) (enc a b (exp h y))))       (recv (enc "i" a b (exp h y)))))-  (label 12)+  (label 14)   (unrealized (0 0) (0 2))   (origs (y (0 1)))   (comment "1 in cohort - 1 not yet seen"))@@ -361,9 +414,9 @@           (enc a b (exp (exp (gen) y) x))))       (recv (enc "i" a b (exp (exp (gen) y) x))))     ((send (enc "i" (exp (gen) x) (privk a)))))-  (label 13)-  (parent 12)-  (seen 14)+  (label 15)+  (parent 14)+  (seen 16)   (unrealized (0 2))   (comment "3 in cohort - 2 not yet seen")) @@ -387,8 +440,8 @@         (cat (enc (exp (gen) y) (privk b))           (enc a b (exp (exp (gen) y) x))))       (send (enc "i" a b (exp (exp (gen) y) x)))))-  (label 14)-  (parent 13)+  (label 16)+  (parent 15)   (unrealized)   (shape)   (maps ((0) ((a a) (b b) (h (exp (gen) x)) (y y))))@@ -412,10 +465,10 @@       (recv (enc "i" a b (exp (exp (gen) y) x))))     ((send (enc "i" (exp (gen) x) (privk a))))     ((recv (exp (exp (gen) y) x)) (send (exp (exp (gen) y) x))))-  (label 15)-  (parent 13)+  (label 17)+  (parent 15)   (unrealized (2 0))-  (comment "1 in cohort - 1 not yet seen"))+  (comment "2 in cohort - 2 not yet seen"))  (defskeleton dhke-with-base-vars   (vars (a b name) (y x expn))@@ -437,11 +490,37 @@     ((send (enc "i" (exp (gen) x) (privk a))))     ((recv (exp (exp (gen) y) x)) (send (exp (exp (gen) y) x)))     ((recv y) (send y)))-  (label 16)-  (parent 15)+  (label 18)+  (parent 17)   (unrealized (3 0))   (comment "empty cohort")) +(defskeleton dhke-with-base-vars+  (vars (a b name) (y x expn))+  (defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))+  (defstrand init 1 (a a) (x x))+  (deflistener (exp (exp (gen) y) x))+  (deflistener x)+  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 1) (0 2))+    ((3 1) (2 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig y x)+  (operation encryption-test (added-listener x) (exp (exp (gen) y) x)+    (2 0))+  (traces+    ((recv (enc "i" (exp (gen) x) (privk a)))+      (send+        (cat (enc (exp (gen) y) (privk b))+          (enc a b (exp (exp (gen) y) x))))+      (recv (enc "i" a b (exp (exp (gen) y) x))))+    ((send (enc "i" (exp (gen) x) (privk a))))+    ((recv (exp (exp (gen) y) x)) (send (exp (exp (gen) y) x)))+    ((recv x) (send x)))+  (label 19)+  (parent 17)+  (unrealized (3 0))+  (comment "empty cohort"))+ (comment "Nothing left to do")  (defprotocol dhke-with-base-vars diffie-hellman@@ -466,7 +545,7 @@   (traces     ((send (enc "i" (exp (gen) x) (privk a)))       (recv (cat (enc g (privk b)) (enc a b (exp g x))))))-  (label 17)+  (label 20)   (unrealized (0 1))   (origs (x (0 0)))   (comment "1 in cohort - 1 not yet seen"))@@ -487,9 +566,9 @@           (enc a b (exp (exp (gen) x) y)))))     ((recv (enc "i" h (privk a-0)))       (send (cat (enc (exp (gen) y) (privk b)) (enc a-0 b (exp h y))))))-  (label 18)-  (parent 17)-  (seen 19)+  (label 21)+  (parent 20)+  (seen 22)   (unrealized (0 1))   (comment "3 in cohort - 2 not yet seen")) @@ -511,8 +590,8 @@       (send         (cat (enc (exp (gen) y) (privk b))           (enc a b (exp (exp (gen) x) y))))))-  (label 19)-  (parent 18)+  (label 22)+  (parent 21)   (unrealized)   (shape)   (maps ((0) ((a a) (b b) (g (exp (gen) y)) (x x))))@@ -536,10 +615,10 @@     ((recv (enc "i" h (privk a-0)))       (send (cat (enc (exp (gen) y) (privk b)) (enc a-0 b (exp h y)))))     ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y))))-  (label 20)-  (parent 18)+  (label 23)+  (parent 21)   (unrealized (2 0))-  (comment "1 in cohort - 1 not yet seen"))+  (comment "2 in cohort - 2 not yet seen"))  (defskeleton dhke-with-base-vars   (vars (a b a-0 name) (h base) (x y expn))@@ -561,11 +640,36 @@       (send (cat (enc (exp (gen) y) (privk b)) (enc a-0 b (exp h y)))))     ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))     ((recv x) (send x)))-  (label 21)-  (parent 20)+  (label 24)+  (parent 23)   (unrealized (3 0))   (comment "empty cohort")) +(defskeleton dhke-with-base-vars+  (vars (a b a-0 name) (h base) (x y expn))+  (defstrand init 2 (a a) (b b) (g (exp (gen) y)) (x x))+  (defstrand resp 2 (a a-0) (b b) (h h) (y y))+  (deflistener (exp (exp (gen) x) y))+  (deflistener y)+  (precedes ((0 0) (2 0)) ((1 1) (3 0)) ((2 1) (0 1)) ((3 1) (2 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig x y)+  (operation encryption-test (added-listener y) (exp (exp (gen) x) y)+    (2 0))+  (traces+    ((send (enc "i" (exp (gen) x) (privk a)))+      (recv+        (cat (enc (exp (gen) y) (privk b))+          (enc a b (exp (exp (gen) x) y)))))+    ((recv (enc "i" h (privk a-0)))+      (send (cat (enc (exp (gen) y) (privk b)) (enc a-0 b (exp h y)))))+    ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+    ((recv y) (send y)))+  (label 25)+  (parent 23)+  (unrealized (3 0))+  (comment "empty cohort"))+ (comment "Nothing left to do")  (defprotocol dh-mim-with-base-vars diffie-hellman@@ -587,7 +691,7 @@   (uniq-orig n x y)   (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))     ((recv hx) (send (exp (gen) y)) (recv (enc n (exp hx y)))))-  (label 22)+  (label 26)   (unrealized (1 2))   (preskeleton)   (comment "Not a skeleton"))@@ -600,9 +704,9 @@   (uniq-orig n x y)   (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))     ((recv hx) (send (exp (gen) y)) (recv (enc n (exp hx y)))))-  (label 23)-  (parent 22)-  (seen 24)+  (label 27)+  (parent 26)+  (seen 28)   (unrealized (1 2))   (origs (y (1 1)) (x (0 0)) (n (0 2)))   (comment "3 in cohort - 2 not yet seen"))@@ -620,8 +724,8 @@       (send (enc n (exp (exp (gen) x) y))))     ((recv (exp (gen) x)) (send (exp (gen) y))       (recv (enc n (exp (exp (gen) x) y)))))-  (label 24)-  (parent 23)+  (label 28)+  (parent 27)   (unrealized)   (shape)   (maps@@ -640,9 +744,9 @@   (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))     ((recv hx) (send (exp (gen) y)) (recv (enc n (exp hx y))))     ((recv (exp hx y)) (send (exp hx y))))-  (label 25)-  (parent 23)-  (seen 26)+  (label 29)+  (parent 27)+  (seen 30)   (unrealized (1 2) (2 0))   (comment "3 in cohort - 2 not yet seen")) @@ -657,8 +761,8 @@   (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))     ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y))))     ((recv (exp (gen) y)) (send (exp (gen) y))))-  (label 26)-  (parent 25)+  (label 30)+  (parent 29)   (unrealized (1 2))   (comment "1 in cohort - 1 not yet seen")) @@ -674,8 +778,8 @@   (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))     ((recv hx) (send (exp (gen) y)) (recv (enc n (exp hx y))))     ((recv (exp hx y)) (send (exp hx y))) ((recv y) (send y)))-  (label 27)-  (parent 25)+  (label 31)+  (parent 29)   (unrealized (1 2) (3 0))   (comment "empty cohort")) @@ -694,9 +798,9 @@     ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y))))     ((recv (exp (gen) y)) (send (exp (gen) y)))     ((recv (exp hy x)) (send (exp hy x))))-  (label 28)-  (parent 26)-  (seen 29)+  (label 32)+  (parent 30)+  (seen 33)   (unrealized (3 0))   (comment "3 in cohort - 2 not yet seen")) @@ -715,8 +819,8 @@     ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y))))     ((recv (exp (gen) y)) (send (exp (gen) y)))     ((recv (exp (gen) x)) (send (exp (gen) x))))-  (label 29)-  (parent 28)+  (label 33)+  (parent 32)   (unrealized)   (comment "1 in cohort - 1 not yet seen")) @@ -735,8 +839,8 @@     ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y))))     ((recv (exp (gen) y)) (send (exp (gen) y)))     ((recv (exp hy x)) (send (exp hy x))) ((recv x) (send x)))-  (label 30)-  (parent 28)+  (label 34)+  (parent 32)   (unrealized (4 0))   (comment "empty cohort")) @@ -752,8 +856,8 @@     ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x))))     ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y))))     ((recv (exp (gen) x)) (send (exp (gen) x))))-  (label 31)-  (parent 29)+  (label 35)+  (parent 33)   (unrealized)   (comment "1 in cohort - 1 not yet seen")) @@ -767,8 +871,8 @@   (traces     ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x))))     ((recv (gen)) (send (exp (gen) y)) (recv (enc n (exp (gen) y)))))-  (label 32)-  (parent 31)+  (label 36)+  (parent 35)   (unrealized)   (shape)   (maps ((0 1) ((n n) (x x) (hy (gen)) (y y) (hx (gen)))))@@ -795,7 +899,7 @@   (uniq-orig n x)   (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))     ((recv n) (send n)))-  (label 33)+  (label 37)   (unrealized (1 0))   (preskeleton)   (comment "Not a skeleton"))@@ -808,8 +912,8 @@   (uniq-orig n x)   (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))     ((recv n) (send n)))-  (label 34)-  (parent 33)+  (label 38)+  (parent 37)   (unrealized (1 0))   (origs (x (0 0)) (n (0 2)))   (comment "1 in cohort - 1 not yet seen"))@@ -825,9 +929,9 @@     (enc n (exp hy x)))   (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))     ((recv n) (send n)) ((recv (exp hy x)) (send (exp hy x))))-  (label 35)-  (parent 34)-  (seen 36)+  (label 39)+  (parent 38)+  (seen 40)   (unrealized (2 0))   (comment "3 in cohort - 2 not yet seen")) @@ -842,8 +946,8 @@   (traces     ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x))))     ((recv n) (send n)) ((recv (exp (gen) x)) (send (exp (gen) x))))-  (label 36)-  (parent 35)+  (label 40)+  (parent 39)   (unrealized)   (comment "1 in cohort - 1 not yet seen")) @@ -859,8 +963,8 @@   (traces ((send (exp (gen) x)) (recv hy) (send (enc n (exp hy x))))     ((recv n) (send n)) ((recv (exp hy x)) (send (exp hy x)))     ((recv x) (send x)))-  (label 37)-  (parent 35)+  (label 41)+  (parent 39)   (unrealized (3 0))   (comment "empty cohort")) @@ -874,8 +978,8 @@   (traces     ((send (exp (gen) x)) (recv (gen)) (send (enc n (exp (gen) x))))     ((recv n) (send n)))-  (label 38)-  (parent 36)+  (label 42)+  (parent 40)   (unrealized)   (shape)   (maps ((0 1) ((n n) (x x) (hy (gen)))))
tst/dy.tst view
@@ -1,6 +1,6 @@ (herald "Example 1.3 from 1983 Dolev-Yao Paper") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol dy basic
tst/encsig.tst view
@@ -1,7 +1,7 @@ (herald "Encrypted Signed Message Example"   (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol mult-keys-enc-sig basic
tst/epmo-hash.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing"   (comment "Annotated with trust management formulas")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol epmo basic
tst/epmo-key-hash.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing"   (comment "Annotated with trust management formulas")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol epmo basic
tst/epmo.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol"   (comment "Annotated with trust management formulas")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol epmo basic
tst/epmo_acctnum-key-hash.tst view
@@ -3,7 +3,7 @@   (displacement)   (comment "This version includes account numbers in exchanges")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read") (comment "Displacement disabled")
tst/epmo_acctnum.tst view
@@ -2,7 +2,7 @@   (displacement)   (comment "This version includes account numbers in exchanges")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read") (comment "Displacement disabled")
tst/ffgg.tst view
@@ -1,7 +1,7 @@ (herald "The ffgg Protocol"   (comment "From A Necessarily Parallel Attack by Jon K. Millen")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol ffgg basic
tst/fragile_pruning.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol fragile_pruning basic
tst/hashtest-key-hash.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol hashtest basic
tst/hashtest.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol hashtest basic
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol kerberos basic
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol missing-contraction basic
tst/neuman-stubblebine-reauth.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol neuman-stubblebine-reauth basic
tst/neuman-stubblebine.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol neuman-stubblebine basic
tst/no_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol no-contraction basic
tst/non_transforming.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol non_transforming basic
tst/nonaug-prune.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol nonaug-prune basic
tst/ns.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder Public-Key Protocol Variants") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol ns basic
tst/nsl3.tst view
@@ -1,6 +1,6 @@ (herald "Three Party Needham-Schroeder-Lowe Protocol") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol nsl3 basic
tst/nsl4cm1.tst view
@@ -1,6 +1,6 @@ (herald "Four Party Needham-Schroeder-Lowe Protocol") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol nsl4cm basic
tst/nslsk.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol nslsk basic
tst/or.tst view
@@ -1,7 +1,7 @@ (herald "Otway-Rees Protocol"   (comment "Standard version using variables of sort mesg")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol or basic
tst/pca.scm view
@@ -1,4 +1,4 @@-(herald "Privacy Certificate Authority"+(herald "Privacy Certificate Authority" (bound 15)   (comment "Generation of an Attestation Identity Certificate"))  ;;; PCA generation of AIC, simplified
tst/pca.tst view
@@ -1,8 +1,9 @@-(herald "Privacy Certificate Authority"+(herald "Privacy Certificate Authority" (bound 15)   (comment "Generation of an Attestation Identity Certificate")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")+(comment "Strand count bounded at 15")  (defprotocol pca basic   (defrole tpm
tst/pkinit.tst view
@@ -1,6 +1,6 @@ (herald "Kerberos PK init") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol pkinit basic
tst/print.tst view
@@ -1,7 +1,7 @@ (herald "Print Test"   (comment "See if read forms look like printed ones")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol print-test basic
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol prune basic
tst/sigenc.tst view
@@ -1,7 +1,7 @@ (herald "Signed Encrypted Message Example"   (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol mult-keys-sig-enc basic
tst/sorted_epmo_acctnum.tst view
@@ -4,7 +4,7 @@     "This version uses sorts to avoid confusion"     "between a nonce and other data")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read") (comment "Displacement disabled")
tst/targetterms2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol targetterms8 basic
+ tst/timestamping.scm view
@@ -0,0 +1,46 @@+(herald timestamping-service)++;; Timestamping service as described on Page 76 in Applied+;; Cryptography, Second Edition by Bruce Schneier.++;; This version DOES NOT send the identity of timestamp holder that+;; follows the one sent to the client.  It's a to do.++(defmacro (link)+  (cat alice_1 h_1 t_1 l_1))++(defmacro (timestamp l)+  (enc n alice h alice_1 h_1 t_1 l (privk trent)))++(defprotocol timestamping-service basic+  (defrole client (vars (alice alice_1 trent name)+  			(n data) (h h_1 text) (t_1 l mesg))+    (trace+     (send (cat h alice))+     (recv (timestamp l))))+  (defrole server (vars (alice alice_1 trent name)+			(n data) (h h_1 text) (t_1 l_1 mesg))+    (trace+     (recv (cat (enc (enc (link) (privk trent)) (pubk trent)) h alice))+     (send (cat (timestamp (hash (link)))+		(enc+		 (enc (hash alice h (timestamp (hash (link))) (hash (link)))+		      (privk trent))+		 (pubk trent)))))+    (uniq-orig n))+  (defrole origin (vars (alice alice_1 trent name)+  			(n data) (h h_1 text) (t_1 l_1 text))+    (trace+     (recv (enc (enc n (privk trent)) (pubk trent)))+     (send (enc+	    (enc alice h (timestamp (hash (link))) (hash (link))+		 (privk trent))+	    (pubk trent)))))+  (defrole big-bang (vars (n data) (trent name))+    (trace (send (enc (enc n (privk trent)) (pubk trent))))+    (uniq-orig n)))++(defskeleton timestamping-service+  (vars (trent name) (n_0 data))+  (defstrand client 2 (trent trent))+  (non-orig (privk trent)))
+ tst/timestamping.tst view
@@ -0,0 +1,479 @@+(herald timestamping-service)++(comment "CPSA 2.2.7")+(comment "All input read")++(defprotocol timestamping-service basic+  (defrole client+    (vars (alice alice_1 trent name) (n data) (h h_1 text) (t_1 l mesg))+    (trace (send (cat h alice))+      (recv (enc n alice h alice_1 h_1 t_1 l (privk trent)))))+  (defrole server+    (vars (alice alice_1 trent name) (n data) (h h_1 text)+      (t_1 l_1 mesg))+    (trace+      (recv+        (cat (enc (enc alice_1 h_1 t_1 l_1 (privk trent)) (pubk trent))+          h alice))+      (send+        (cat+          (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+            (privk trent))+          (enc+            (enc+              (hash alice h+                (enc n alice h alice_1 h_1 t_1+                  (hash alice_1 h_1 t_1 l_1) (privk trent))+                (hash alice_1 h_1 t_1 l_1)) (privk trent))+            (pubk trent)))))+    (uniq-orig n))+  (defrole origin+    (vars (alice alice_1 trent name) (n data) (h h_1 t_1 l_1 text))+    (trace (recv (enc (enc n (privk trent)) (pubk trent)))+      (send+        (enc+          (enc alice h+            (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+              (privk trent)) (hash alice_1 h_1 t_1 l_1) (privk trent))+          (pubk trent)))))+  (defrole big-bang+    (vars (n data) (trent name))+    (trace (send (enc (enc n (privk trent)) (pubk trent))))+    (uniq-orig n)))++(defskeleton timestamping-service+  (vars (t_1 l mesg) (h h_1 text) (n data) (trent alice alice_1 name))+  (defstrand client 2 (t_1 t_1) (l l) (h h) (h_1 h_1) (n n)+    (alice alice) (alice_1 alice_1) (trent trent))+  (non-orig (privk trent))+  (traces+    ((send (cat h alice))+      (recv (enc n alice h alice_1 h_1 t_1 l (privk trent)))))+  (label 0)+  (unrealized (0 1))+  (origs)+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton timestamping-service+  (vars (t_1 l_1 mesg) (h h_1 text) (n data) (trent alice alice_1 name))+  (defstrand client 2 (t_1 t_1) (l (hash alice_1 h_1 t_1 l_1)) (h h)+    (h_1 h_1) (n n) (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand server 2 (t_1 t_1) (l_1 l_1) (h h) (h_1 h_1) (n n)+    (alice alice) (alice_1 alice_1) (trent trent))+  (precedes ((1 1) (0 1)))+  (non-orig (privk trent))+  (uniq-orig n)+  (operation encryption-test (added-strand server 2)+    (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+      (privk trent)) (0 1))+  (traces+    ((send (cat h alice))+      (recv+        (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+          (privk trent))))+    ((recv+       (cat (enc (enc alice_1 h_1 t_1 l_1 (privk trent)) (pubk trent)) h+         alice))+      (send+        (cat+          (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+            (privk trent))+          (enc+            (enc+              (hash alice h+                (enc n alice h alice_1 h_1 t_1+                  (hash alice_1 h_1 t_1 l_1) (privk trent))+                (hash alice_1 h_1 t_1 l_1)) (privk trent))+            (pubk trent))))))+  (label 1)+  (parent 0)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton timestamping-service+  (vars (h h_1 t_1 l_1 text) (n data) (trent alice alice_1 name))+  (defstrand client 2 (t_1 t_1) (l (hash alice_1 h_1 t_1 l_1)) (h h)+    (h_1 h_1) (n n) (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand origin 2 (h h) (h_1 h_1) (t_1 t_1) (l_1 l_1) (n n)+    (alice alice) (alice_1 alice_1) (trent trent))+  (precedes ((1 1) (0 1)))+  (non-orig (privk trent))+  (operation encryption-test (added-strand origin 2)+    (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+      (privk trent)) (0 1))+  (traces+    ((send (cat h alice))+      (recv+        (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+          (privk trent))))+    ((recv (enc (enc n (privk trent)) (pubk trent)))+      (send+        (enc+          (enc alice h+            (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+              (privk trent)) (hash alice_1 h_1 t_1 l_1) (privk trent))+          (pubk trent)))))+  (label 2)+  (parent 0)+  (unrealized (0 1) (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton timestamping-service+  (vars (h h_1 h_1-0 t_1 l_1 text) (n n-0 data)+    (trent alice alice_1 alice_1-0 name))+  (defstrand client 2+    (t_1+      (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+        (hash alice_1-0 h_1-0 t_1 l_1) (privk trent)))+    (l+      (hash alice_1 h_1+        (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+          (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+        (hash alice_1-0 h_1-0 t_1 l_1))) (h h) (h_1 h_1) (n n)+    (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand server 2+    (t_1+      (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+        (hash alice_1-0 h_1-0 t_1 l_1) (privk trent)))+    (l_1 (hash alice_1-0 h_1-0 t_1 l_1)) (h h) (h_1 h_1) (n n)+    (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand origin 2 (h h_1) (h_1 h_1-0) (t_1 t_1) (l_1 l_1) (n n-0)+    (alice alice_1) (alice_1 alice_1-0) (trent trent))+  (precedes ((1 1) (0 1)) ((2 1) (1 0)))+  (non-orig (privk trent))+  (uniq-orig n)+  (operation encryption-test (added-strand origin 2)+    (enc alice_1 h_1+      (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+        (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+      (hash alice_1-0 h_1-0 t_1 l_1) (privk trent)) (1 0))+  (traces+    ((send (cat h alice))+      (recv+        (enc n alice h alice_1 h_1+          (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+            (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+          (hash alice_1 h_1+            (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+              (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+            (hash alice_1-0 h_1-0 t_1 l_1)) (privk trent))))+    ((recv+       (cat+         (enc+           (enc alice_1 h_1+             (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+               (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+             (hash alice_1-0 h_1-0 t_1 l_1) (privk trent)) (pubk trent))+         h alice))+      (send+        (cat+          (enc n alice h alice_1 h_1+            (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+              (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+            (hash alice_1 h_1+              (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+                (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+              (hash alice_1-0 h_1-0 t_1 l_1)) (privk trent))+          (enc+            (enc+              (hash alice h+                (enc n alice h alice_1 h_1+                  (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+                    (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+                  (hash alice_1 h_1+                    (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+                      (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+                    (hash alice_1-0 h_1-0 t_1 l_1)) (privk trent))+                (hash alice_1 h_1+                  (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+                    (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+                  (hash alice_1-0 h_1-0 t_1 l_1))) (privk trent))+            (pubk trent)))))+    ((recv (enc (enc n-0 (privk trent)) (pubk trent)))+      (send+        (enc+          (enc alice_1 h_1+            (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+              (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+            (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+          (pubk trent)))))+  (label 3)+  (parent 1)+  (unrealized (2 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton timestamping-service+  (vars (h h_1 t_1 l_1 text) (n data) (trent alice alice_1 name))+  (defstrand client 2 (t_1 t_1) (l (hash alice_1 h_1 t_1 l_1)) (h h)+    (h_1 h_1) (n n) (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand origin 2 (h h) (h_1 h_1) (t_1 t_1) (l_1 l_1) (n n)+    (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand big-bang 1 (n n) (trent trent))+  (precedes ((1 1) (0 1)) ((2 0) (1 0)))+  (non-orig (privk trent))+  (uniq-orig n)+  (operation encryption-test (added-strand big-bang 1)+    (enc n (privk trent)) (1 0))+  (traces+    ((send (cat h alice))+      (recv+        (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+          (privk trent))))+    ((recv (enc (enc n (privk trent)) (pubk trent)))+      (send+        (enc+          (enc alice h+            (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+              (privk trent)) (hash alice_1 h_1 t_1 l_1) (privk trent))+          (pubk trent))))+    ((send (enc (enc n (privk trent)) (pubk trent)))))+  (label 4)+  (parent 2)+  (unrealized (0 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton timestamping-service+  (vars (h h_1 h_1-0 t_1 l_1 text) (n n-0 data)+    (trent alice alice_1 alice_1-0 name))+  (defstrand client 2+    (t_1+      (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+        (hash alice_1-0 h_1-0 t_1 l_1) (privk trent)))+    (l+      (hash alice_1 h_1+        (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+          (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+        (hash alice_1-0 h_1-0 t_1 l_1))) (h h) (h_1 h_1) (n n)+    (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand server 2+    (t_1+      (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+        (hash alice_1-0 h_1-0 t_1 l_1) (privk trent)))+    (l_1 (hash alice_1-0 h_1-0 t_1 l_1)) (h h) (h_1 h_1) (n n)+    (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand origin 2 (h h_1) (h_1 h_1-0) (t_1 t_1) (l_1 l_1) (n n-0)+    (alice alice_1) (alice_1 alice_1-0) (trent trent))+  (defstrand big-bang 1 (n n-0) (trent trent))+  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 0) (2 0)))+  (non-orig (privk trent))+  (uniq-orig n n-0)+  (operation encryption-test (added-strand big-bang 1)+    (enc n-0 (privk trent)) (2 0))+  (traces+    ((send (cat h alice))+      (recv+        (enc n alice h alice_1 h_1+          (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+            (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+          (hash alice_1 h_1+            (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+              (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+            (hash alice_1-0 h_1-0 t_1 l_1)) (privk trent))))+    ((recv+       (cat+         (enc+           (enc alice_1 h_1+             (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+               (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+             (hash alice_1-0 h_1-0 t_1 l_1) (privk trent)) (pubk trent))+         h alice))+      (send+        (cat+          (enc n alice h alice_1 h_1+            (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+              (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+            (hash alice_1 h_1+              (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+                (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+              (hash alice_1-0 h_1-0 t_1 l_1)) (privk trent))+          (enc+            (enc+              (hash alice h+                (enc n alice h alice_1 h_1+                  (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+                    (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+                  (hash alice_1 h_1+                    (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+                      (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+                    (hash alice_1-0 h_1-0 t_1 l_1)) (privk trent))+                (hash alice_1 h_1+                  (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+                    (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+                  (hash alice_1-0 h_1-0 t_1 l_1))) (privk trent))+            (pubk trent)))))+    ((recv (enc (enc n-0 (privk trent)) (pubk trent)))+      (send+        (enc+          (enc alice_1 h_1+            (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+              (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+            (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+          (pubk trent))))+    ((send (enc (enc n-0 (privk trent)) (pubk trent)))))+  (label 5)+  (parent 3)+  (unrealized)+  (shape)+  (maps+    ((0)+      ((trent trent) (alice alice) (alice_1 alice_1) (n n) (h h)+        (h_1 h_1)+        (t_1+          (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+            (hash alice_1-0 h_1-0 t_1 l_1) (privk trent)))+        (l+          (hash alice_1 h_1+            (enc n-0 alice_1 h_1 alice_1-0 h_1-0 t_1+              (hash alice_1-0 h_1-0 t_1 l_1) (privk trent))+            (hash alice_1-0 h_1-0 t_1 l_1))))))+  (origs (n-0 (3 0)) (n (1 1))))++(defskeleton timestamping-service+  (vars (h h_1 t_1 l_1 h-0 text) (n n-0 data)+    (trent alice alice_1 alice-0 name))+  (defstrand client 2 (t_1 t_1) (l (hash alice_1 h_1 t_1 l_1)) (h h)+    (h_1 h_1) (n n) (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand origin 2 (h h) (h_1 h_1) (t_1 t_1) (l_1 l_1) (n n)+    (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand big-bang 1 (n n) (trent trent))+  (defstrand server 2+    (t_1+      (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+        (privk trent))) (l_1 (hash alice_1 h_1 t_1 l_1)) (h h-0) (h_1 h)+    (n n-0) (alice alice-0) (alice_1 alice) (trent trent))+  (precedes ((1 1) (0 1)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 1) (0 1)))+  (non-orig (privk trent))+  (uniq-orig n n-0)+  (operation encryption-test (added-strand server 2)+    (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+      (privk trent)) (0 1)+    (enc+      (enc alice h+        (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+          (privk trent)) (hash alice_1 h_1 t_1 l_1) (privk trent))+      (pubk trent)))+  (traces+    ((send (cat h alice))+      (recv+        (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+          (privk trent))))+    ((recv (enc (enc n (privk trent)) (pubk trent)))+      (send+        (enc+          (enc alice h+            (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+              (privk trent)) (hash alice_1 h_1 t_1 l_1) (privk trent))+          (pubk trent))))+    ((send (enc (enc n (privk trent)) (pubk trent))))+    ((recv+       (cat+         (enc+           (enc alice h+             (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+               (privk trent)) (hash alice_1 h_1 t_1 l_1) (privk trent))+           (pubk trent)) h-0 alice-0))+      (send+        (cat+          (enc n-0 alice-0 h-0 alice h+            (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+              (privk trent))+            (hash alice h+              (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+                (privk trent)) (hash alice_1 h_1 t_1 l_1))+            (privk trent))+          (enc+            (enc+              (hash alice-0 h-0+                (enc n-0 alice-0 h-0 alice h+                  (enc n alice h alice_1 h_1 t_1+                    (hash alice_1 h_1 t_1 l_1) (privk trent))+                  (hash alice h+                    (enc n alice h alice_1 h_1 t_1+                      (hash alice_1 h_1 t_1 l_1) (privk trent))+                    (hash alice_1 h_1 t_1 l_1)) (privk trent))+                (hash alice h+                  (enc n alice h alice_1 h_1 t_1+                    (hash alice_1 h_1 t_1 l_1) (privk trent))+                  (hash alice_1 h_1 t_1 l_1))) (privk trent))+            (pubk trent))))))+  (label 6)+  (parent 4)+  (seen 7)+  (unrealized (3 0))+  (comment "2 in cohort - 1 not yet seen"))++(defskeleton timestamping-service+  (vars (h h_1 t_1 l_1 h-0 text) (n n-0 data)+    (trent alice alice_1 alice-0 name))+  (defstrand client 2 (t_1 t_1) (l (hash alice_1 h_1 t_1 l_1)) (h h)+    (h_1 h_1) (n n) (alice alice) (alice_1 alice_1) (trent trent))+  (defstrand big-bang 1 (n n) (trent trent))+  (defstrand server 2+    (t_1+      (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+        (privk trent))) (l_1 (hash alice_1 h_1 t_1 l_1)) (h h-0) (h_1 h)+    (n n-0) (alice alice-0) (alice_1 alice) (trent trent))+  (defstrand origin 2 (h h) (h_1 h_1) (t_1 t_1) (l_1 l_1) (n n)+    (alice alice) (alice_1 alice_1) (trent trent))+  (precedes ((1 0) (3 0)) ((2 1) (0 1)) ((3 1) (2 0)))+  (non-orig (privk trent))+  (uniq-orig n n-0)+  (operation encryption-test (added-strand origin 2)+    (enc alice h+      (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+        (privk trent)) (hash alice_1 h_1 t_1 l_1) (privk trent)) (3 0))+  (traces+    ((send (cat h alice))+      (recv+        (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+          (privk trent))))+    ((send (enc (enc n (privk trent)) (pubk trent))))+    ((recv+       (cat+         (enc+           (enc alice h+             (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+               (privk trent)) (hash alice_1 h_1 t_1 l_1) (privk trent))+           (pubk trent)) h-0 alice-0))+      (send+        (cat+          (enc n-0 alice-0 h-0 alice h+            (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+              (privk trent))+            (hash alice h+              (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+                (privk trent)) (hash alice_1 h_1 t_1 l_1))+            (privk trent))+          (enc+            (enc+              (hash alice-0 h-0+                (enc n-0 alice-0 h-0 alice h+                  (enc n alice h alice_1 h_1 t_1+                    (hash alice_1 h_1 t_1 l_1) (privk trent))+                  (hash alice h+                    (enc n alice h alice_1 h_1 t_1+                      (hash alice_1 h_1 t_1 l_1) (privk trent))+                    (hash alice_1 h_1 t_1 l_1)) (privk trent))+                (hash alice h+                  (enc n alice h alice_1 h_1 t_1+                    (hash alice_1 h_1 t_1 l_1) (privk trent))+                  (hash alice_1 h_1 t_1 l_1))) (privk trent))+            (pubk trent)))))+    ((recv (enc (enc n (privk trent)) (pubk trent)))+      (send+        (enc+          (enc alice h+            (enc n alice h alice_1 h_1 t_1 (hash alice_1 h_1 t_1 l_1)+              (privk trent)) (hash alice_1 h_1 t_1 l_1) (privk trent))+          (pubk trent)))))+  (label 7)+  (parent 6)+  (unrealized)+  (shape)+  (maps+    ((0)+      ((trent trent) (alice alice) (alice_1 alice_1) (n n) (h h)+        (h_1 h_1) (t_1 t_1) (l (hash alice_1 h_1 t_1 l_1)))))+  (origs (n-0 (2 1)) (n (1 0))))++(comment "Nothing left to do")
tst/tor.tst view
@@ -1,7 +1,7 @@ (herald "Tor Circuit-Level Handshake Protocol" (algebra diffie-hellman)   (comment "Achieves unilateral authentication")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol tor diffie-hellman
tst/uncarried_keys.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol uncarried-keys basic
tst/uo.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol uniq-orig basic
tst/wang-hash.tst view
@@ -1,6 +1,6 @@ (herald "Wang's Fair Exchange Protocol" (bound 10)) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read") (comment "Strand count bounded at 10")
tst/wang-key-hash.tst view
@@ -1,6 +1,6 @@ (herald "Wang's Fair Exchange Protocol" (bound 10)) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read") (comment "Strand count bounded at 10")
tst/weird.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol weird basic
tst/wide-mouth-frog.tst view
@@ -1,7 +1,7 @@ (herald "Wide-Mouth Frog Protocol"   (comment "This protocol has an infinite number of shapes")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol wide-mouth-frog basic
tst/wonthull.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol wonthull basic
tst/wonthull2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol wonthull2 basic
tst/wonthull3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol wonthull3 basic
tst/woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol woolam basic
tst/yahalom-6.3.6.tst view
@@ -4,7 +4,7 @@     "Yahalom Protocol, Section 6.3.6, Page 49")   (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")) -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol yahalom basic
tst/yahalom.tst view
@@ -1,6 +1,6 @@ (herald "Yahalom Protocol Without Forwarding") -(comment "CPSA 2.2.6")+(comment "CPSA 2.2.7") (comment "All input read")  (defprotocol yahalom basic