diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,32 @@ +2012-02-01 John D. Ramsdell + + * 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 + + * 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 + + * 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 * src/CPSA/Graph/SVG.hs (tooltip): Display tool tips with @@ -5,6 +34,8 @@ xlink:title='MESSAGE'>... 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 * tst/deorig_mesg.scm (deorig-mesg): Added an example showing @@ -378,12 +409,12 @@ 2010-10-02 John D. Ramsdell * src/CPSA/Lib/Algebra.hs: Added heldBy to support - Diffie-Hellman. + Diffie-Hellman. 2010-09-23 John D. Ramsdell * 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 @@ -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 * 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 @@ -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 @@ -623,7 +654,7 @@ 2010-01-07 John D. Ramsdell - * 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 * 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 * src/CPSA/Lib/Cohort.hs (mgus): Added a filter that removes @@ -760,7 +791,7 @@ 2009-08-03 John D. Ramsdell - * 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 @@ -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 - * src/CPSA/Graph/LaTeXView.hs (latexView): + * src/CPSA/Graph/LaTeXView.hs (latexView): 2009-06-23 John D. Ramsdell @@ -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 * 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 - + * cpsa.cabal (Version): Tagged as version 1.3.2. 2008-11-30 John D. Ramsdell - + * 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 * 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 * src/CPSA/Lib/Strand.hs (Gist): Created a data structure designed @@ -1319,7 +1350,7 @@ 2008-08-11 John D. Ramsdell * 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 - * src/CPSA/Basic/Main.hs: Re-enabled indeterminates + * src/CPSA/Basic/Main.hs: Re-enabled indeterminates 2008-02-27 John D. Ramsdell diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -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 diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -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. diff --git a/doc/Makefile b/doc/Makefile --- a/doc/Makefile +++ b/doc/Makefile @@ -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) diff --git a/doc/README b/doc/README --- a/doc/README +++ b/doc/README @@ -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 diff --git a/doc/SimpleDiffieHellman.hs b/doc/SimpleDiffieHellman.hs new file mode 100644 --- /dev/null +++ b/doc/SimpleDiffieHellman.hs @@ -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 diff --git a/doc/cpsa.bib b/doc/cpsa.bib --- a/doc/cpsa.bib +++ b/doc/cpsa.bib @@ -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 = {}, diff --git a/doc/cpsadesign.pdf b/doc/cpsadesign.pdf Binary files a/doc/cpsadesign.pdf and b/doc/cpsadesign.pdf differ diff --git a/doc/cpsadesign.tex b/doc/cpsadesign.tex --- a/doc/cpsadesign.tex +++ b/doc/cpsadesign.tex @@ -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} diff --git a/doc/cpsaoverview.pdf b/doc/cpsaoverview.pdf Binary files a/doc/cpsaoverview.pdf and b/doc/cpsaoverview.pdf differ diff --git a/doc/cpsaprimer.pdf b/doc/cpsaprimer.pdf Binary files a/doc/cpsaprimer.pdf and b/doc/cpsaprimer.pdf differ diff --git a/doc/cpsaprimer.tex b/doc/cpsaprimer.tex --- a/doc/cpsaprimer.tex +++ b/doc/cpsaprimer.tex @@ -1,7 +1,6 @@ \documentclass[12pt]{article} \usepackage{amssymb} \usepackage{amsmath} -\usepackage{amsthm} \usepackage{url} \usepackage{graphicx} \usepackage{makeidx} diff --git a/doc/cpsasdha.pdf b/doc/cpsasdha.pdf new file mode 100644 Binary files /dev/null and b/doc/cpsasdha.pdf differ diff --git a/doc/cpsasdha.tex b/doc/cpsasdha.tex new file mode 100644 --- /dev/null +++ b/doc/cpsasdha.tex @@ -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} diff --git a/doc/cpsaspec.pdf b/doc/cpsaspec.pdf Binary files a/doc/cpsaspec.pdf and b/doc/cpsaspec.pdf differ diff --git a/doc/cpsaspec.tex b/doc/cpsaspec.tex --- a/doc/cpsaspec.tex +++ b/doc/cpsaspec.tex @@ -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 diff --git a/doc/dhke.scm b/doc/dhke.scm new file mode 100644 --- /dev/null +++ b/doc/dhke.scm @@ -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))) diff --git a/doc/macros.tex b/doc/macros.tex --- a/doc/macros.tex +++ b/doc/macros.tex @@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}} -\newcommand{\version}{2.2.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 diff --git a/src/CPSA/Basic/Algebra.hs b/src/CPSA/Basic/Algebra.hs --- a/src/CPSA/Basic/Algebra.hs +++ b/src/CPSA/Basic/Algebra.hs @@ -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 [] diff --git a/src/CPSA/DiffieHellman/Algebra.hs b/src/CPSA/DiffieHellman/Algebra.hs --- a/src/CPSA/DiffieHellman/Algebra.hs +++ b/src/CPSA/DiffieHellman/Algebra.hs @@ -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 diff --git a/src/CPSA/Lib/Algebra.hs b/src/CPSA/Lib/Algebra.hs --- a/src/CPSA/Lib/Algebra.hs +++ b/src/CPSA/Lib/Algebra.hs @@ -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 diff --git a/src/CPSA/Lib/Cohort.hs b/src/CPSA/Lib/Cohort.hs --- a/src/CPSA/Lib/Cohort.hs +++ b/src/CPSA/Lib/Cohort.hs @@ -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 diff --git a/src/CPSA/Lib/Notation.hs b/src/CPSA/Lib/Notation.hs --- a/src/CPSA/Lib/Notation.hs +++ b/src/CPSA/Lib/Notation.hs @@ -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" = diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs --- a/src/CPSA/Lib/Strand.hs +++ b/src/CPSA/Lib/Strand.hs @@ -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] -> diff --git a/src/CPSA/SimpleDiffieHellman/Algebra.hs b/src/CPSA/SimpleDiffieHellman/Algebra.hs --- a/src/CPSA/SimpleDiffieHellman/Algebra.hs +++ b/src/CPSA/SimpleDiffieHellman/Algebra.hs @@ -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 [] diff --git a/tst/DH_hack.tst b/tst/DH_hack.tst --- a/tst/DH_hack.tst +++ b/tst/DH_hack.tst @@ -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") diff --git a/tst/blanchet.tst b/tst/blanchet.tst --- a/tst/blanchet.tst +++ b/tst/blanchet.tst @@ -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 diff --git a/tst/completeness-test.tst b/tst/completeness-test.tst --- a/tst/completeness-test.tst +++ b/tst/completeness-test.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol completeness-test basic diff --git a/tst/crushing.tst b/tst/crushing.tst --- a/tst/crushing.tst +++ b/tst/crushing.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol crushing basic diff --git a/tst/dass_simple.tst b/tst/dass_simple.tst --- a/tst/dass_simple.tst +++ b/tst/dass_simple.tst @@ -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 diff --git a/tst/denning-sacco.tst b/tst/denning-sacco.tst --- a/tst/denning-sacco.tst +++ b/tst/denning-sacco.tst @@ -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 diff --git a/tst/deorig_contract.tst b/tst/deorig_contract.tst --- a/tst/deorig_contract.tst +++ b/tst/deorig_contract.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol deorig-contract basic diff --git a/tst/deorig_mesg.tst b/tst/deorig_mesg.tst --- a/tst/deorig_mesg.tst +++ b/tst/deorig_mesg.tst @@ -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 diff --git a/tst/deorig_simple.tst b/tst/deorig_simple.tst --- a/tst/deorig_simple.tst +++ b/tst/deorig_simple.tst @@ -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 diff --git a/tst/dh_cert.tst b/tst/dh_cert.tst --- a/tst/dh_cert.tst +++ b/tst/dh_cert.tst @@ -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 diff --git a/tst/dhke.tst b/tst/dhke.tst --- a/tst/dhke.tst +++ b/tst/dhke.tst @@ -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))))) diff --git a/tst/dy.tst b/tst/dy.tst --- a/tst/dy.tst +++ b/tst/dy.tst @@ -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 diff --git a/tst/encsig.tst b/tst/encsig.tst --- a/tst/encsig.tst +++ b/tst/encsig.tst @@ -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 diff --git a/tst/epmo-hash.tst b/tst/epmo-hash.tst --- a/tst/epmo-hash.tst +++ b/tst/epmo-hash.tst @@ -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 diff --git a/tst/epmo-key-hash.tst b/tst/epmo-key-hash.tst --- a/tst/epmo-key-hash.tst +++ b/tst/epmo-key-hash.tst @@ -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 diff --git a/tst/epmo.tst b/tst/epmo.tst --- a/tst/epmo.tst +++ b/tst/epmo.tst @@ -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 diff --git a/tst/epmo_acctnum-key-hash.tst b/tst/epmo_acctnum-key-hash.tst --- a/tst/epmo_acctnum-key-hash.tst +++ b/tst/epmo_acctnum-key-hash.tst @@ -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") diff --git a/tst/epmo_acctnum.tst b/tst/epmo_acctnum.tst --- a/tst/epmo_acctnum.tst +++ b/tst/epmo_acctnum.tst @@ -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") diff --git a/tst/ffgg.tst b/tst/ffgg.tst --- a/tst/ffgg.tst +++ b/tst/ffgg.tst @@ -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 diff --git a/tst/fragile_pruning.tst b/tst/fragile_pruning.tst --- a/tst/fragile_pruning.tst +++ b/tst/fragile_pruning.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol fragile_pruning basic diff --git a/tst/hashtest-key-hash.tst b/tst/hashtest-key-hash.tst --- a/tst/hashtest-key-hash.tst +++ b/tst/hashtest-key-hash.tst @@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol hashtest basic diff --git a/tst/hashtest.tst b/tst/hashtest.tst --- a/tst/hashtest.tst +++ b/tst/hashtest.tst @@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol hashtest basic diff --git a/tst/isoreject.tst b/tst/isoreject.tst --- a/tst/isoreject.tst +++ b/tst/isoreject.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol isoreject basic diff --git a/tst/kelly1.tst b/tst/kelly1.tst --- a/tst/kelly1.tst +++ b/tst/kelly1.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol kelly1 basic diff --git a/tst/kerberos.tst b/tst/kerberos.tst --- a/tst/kerberos.tst +++ b/tst/kerberos.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol kerberos basic diff --git a/tst/mass.tst b/tst/mass.tst --- a/tst/mass.tst +++ b/tst/mass.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol mass basic diff --git a/tst/mass2.tst b/tst/mass2.tst --- a/tst/mass2.tst +++ b/tst/mass2.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol mass2 basic diff --git a/tst/missing_contraction.tst b/tst/missing_contraction.tst --- a/tst/missing_contraction.tst +++ b/tst/missing_contraction.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol missing-contraction basic diff --git a/tst/neuman-stubblebine-reauth.tst b/tst/neuman-stubblebine-reauth.tst --- a/tst/neuman-stubblebine-reauth.tst +++ b/tst/neuman-stubblebine-reauth.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol neuman-stubblebine-reauth basic diff --git a/tst/neuman-stubblebine.tst b/tst/neuman-stubblebine.tst --- a/tst/neuman-stubblebine.tst +++ b/tst/neuman-stubblebine.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol neuman-stubblebine basic diff --git a/tst/no_contraction.tst b/tst/no_contraction.tst --- a/tst/no_contraction.tst +++ b/tst/no_contraction.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol no-contraction basic diff --git a/tst/non_transforming.tst b/tst/non_transforming.tst --- a/tst/non_transforming.tst +++ b/tst/non_transforming.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol non_transforming basic diff --git a/tst/nonaug-prune.tst b/tst/nonaug-prune.tst --- a/tst/nonaug-prune.tst +++ b/tst/nonaug-prune.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol nonaug-prune basic diff --git a/tst/ns.tst b/tst/ns.tst --- a/tst/ns.tst +++ b/tst/ns.tst @@ -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 diff --git a/tst/nsl3.tst b/tst/nsl3.tst --- a/tst/nsl3.tst +++ b/tst/nsl3.tst @@ -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 diff --git a/tst/nsl4cm1.tst b/tst/nsl4cm1.tst --- a/tst/nsl4cm1.tst +++ b/tst/nsl4cm1.tst @@ -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 diff --git a/tst/nslsk.tst b/tst/nslsk.tst --- a/tst/nslsk.tst +++ b/tst/nslsk.tst @@ -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 diff --git a/tst/or.tst b/tst/or.tst --- a/tst/or.tst +++ b/tst/or.tst @@ -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 diff --git a/tst/pca.scm b/tst/pca.scm --- a/tst/pca.scm +++ b/tst/pca.scm @@ -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 diff --git a/tst/pca.tst b/tst/pca.tst --- a/tst/pca.tst +++ b/tst/pca.tst @@ -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 diff --git a/tst/pkinit.tst b/tst/pkinit.tst --- a/tst/pkinit.tst +++ b/tst/pkinit.tst @@ -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 diff --git a/tst/print.tst b/tst/print.tst --- a/tst/print.tst +++ b/tst/print.tst @@ -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 diff --git a/tst/pruning1.tst b/tst/pruning1.tst --- a/tst/pruning1.tst +++ b/tst/pruning1.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol prune basic diff --git a/tst/sigenc.tst b/tst/sigenc.tst --- a/tst/sigenc.tst +++ b/tst/sigenc.tst @@ -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 diff --git a/tst/sorted_epmo_acctnum.tst b/tst/sorted_epmo_acctnum.tst --- a/tst/sorted_epmo_acctnum.tst +++ b/tst/sorted_epmo_acctnum.tst @@ -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") diff --git a/tst/targetterms2.tst b/tst/targetterms2.tst --- a/tst/targetterms2.tst +++ b/tst/targetterms2.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol targetterms2 basic diff --git a/tst/targetterms6.tst b/tst/targetterms6.tst --- a/tst/targetterms6.tst +++ b/tst/targetterms6.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol targetterms6 basic diff --git a/tst/targetterms8.tst b/tst/targetterms8.tst --- a/tst/targetterms8.tst +++ b/tst/targetterms8.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol targetterms8 basic diff --git a/tst/timestamping.scm b/tst/timestamping.scm new file mode 100644 --- /dev/null +++ b/tst/timestamping.scm @@ -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))) diff --git a/tst/timestamping.tst b/tst/timestamping.tst new file mode 100644 --- /dev/null +++ b/tst/timestamping.tst @@ -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") diff --git a/tst/tor.tst b/tst/tor.tst --- a/tst/tor.tst +++ b/tst/tor.tst @@ -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 diff --git a/tst/uncarried_keys.tst b/tst/uncarried_keys.tst --- a/tst/uncarried_keys.tst +++ b/tst/uncarried_keys.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol uncarried-keys basic diff --git a/tst/uo.tst b/tst/uo.tst --- a/tst/uo.tst +++ b/tst/uo.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol uniq-orig basic diff --git a/tst/wang-hash.tst b/tst/wang-hash.tst --- a/tst/wang-hash.tst +++ b/tst/wang-hash.tst @@ -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") diff --git a/tst/wang-key-hash.tst b/tst/wang-key-hash.tst --- a/tst/wang-key-hash.tst +++ b/tst/wang-key-hash.tst @@ -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") diff --git a/tst/weird.tst b/tst/weird.tst --- a/tst/weird.tst +++ b/tst/weird.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol weird basic diff --git a/tst/wide-mouth-frog.tst b/tst/wide-mouth-frog.tst --- a/tst/wide-mouth-frog.tst +++ b/tst/wide-mouth-frog.tst @@ -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 diff --git a/tst/wonthull.tst b/tst/wonthull.tst --- a/tst/wonthull.tst +++ b/tst/wonthull.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol wonthull basic diff --git a/tst/wonthull2.tst b/tst/wonthull2.tst --- a/tst/wonthull2.tst +++ b/tst/wonthull2.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol wonthull2 basic diff --git a/tst/wonthull3.tst b/tst/wonthull3.tst --- a/tst/wonthull3.tst +++ b/tst/wonthull3.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.6") +(comment "CPSA 2.2.7") (comment "All input read") (defprotocol wonthull3 basic diff --git a/tst/woolam.tst b/tst/woolam.tst --- a/tst/woolam.tst +++ b/tst/woolam.tst @@ -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 diff --git a/tst/yahalom-6.3.6.tst b/tst/yahalom-6.3.6.tst --- a/tst/yahalom-6.3.6.tst +++ b/tst/yahalom-6.3.6.tst @@ -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 diff --git a/tst/yahalom.tst b/tst/yahalom.tst --- a/tst/yahalom.tst +++ b/tst/yahalom.tst @@ -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