diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,30 @@ +2011-08-16 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as version 2.2.5. + +2011-08-15 John D. Ramsdell + + * src/cpsa.pl: Changed the internal form so that compound terms + are represented as function symbols applied to terms, not as + S-expressions. + +2011-08-12 John D. Ramsdell + + * doc/*: Updated documentation to reflect support for hashing. + +2011-08-11 Paul Rowe + + * src/CPSA/Basic/Algebra.hs: Added support for hashing. + +2011-07-26 John D. Ramsdell + + * src/CPSA/Lib/Strand.hs (ksubst): Made the flag validate the + first argument. + + * src/CPSA/Lib/Strand.hs (compress): Added a flag validate. When + false, compression does not check for intrastrand orderings that + create cycles. Used in thinning. + 2011-05-18 John D. Ramsdell * cpsa.cabal (Version): Tagged as version 2.2.4. diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,5 +1,13 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.2.5 + +** Support for hashing added + Both the Basic and Diffie-Hellman term algebras have a new function + symbol hash that provides support for hashing. The term (hash X) + is treated as a kind of encryption in which the term X is the + encryption key. + * Changes in version 2.2.4 ** GHC link time option added diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 2.2.4 +Version: 2.2.5 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3 @@ -44,7 +44,8 @@ Build-Type: Simple Data-Files: index.html cpsauser.html cpsa.mk Make.hs cpsaprimer.pdf - cpsaoverview.pdf ffgg.scm ns.scm or.scm woolam.scm yahalom.scm + cpsaoverview.pdf cpsaspec.pdf cpsadesign.pdf ffgg.scm ns.scm or.scm + woolam.scm yahalom.scm Data-Dir: doc Extra-Source-Files: Makefile ChangeLog README NEWS ghci cpsatst setup.bat doc/README @@ -95,7 +96,11 @@ tst/tor.tst tst/dh_cert.scm tst/dh_cert.tst tst/epmo_acctnum-key-hash.scm tst/epmo_acctnum-key-hash.tst tst/epmo-key-hash.scm tst/epmo-key-hash.tst tst/wang.lisp - tst/pkinit.scm tst/pkinit.tst + tst/pkinit.scm tst/pkinit.tst tst/print.scm tst/print.tst + tst/epmo-hash.scm tst/epmo-hash.tst tst/hashtest-key-hash.scm + tst/hashtest-key-hash.tst tst/hashtest.scm tst/hashtest.tst + tst/wang-key-hash.scm tst/wang-key-hash.tst tst/wang-hash.scm + tst/wang-hash.tst -- Algebra implementations must import CPSA.Lib.CPSA. -- Tools may additionally import CPSA.Lib.Entry. diff --git a/doc/README b/doc/README --- a/doc/README +++ b/doc/README @@ -14,11 +14,10 @@ * cpsatheory.pdf: CPSA Theory, the beginnings of a connectness proof of the CPSA algorithm -To build the documentation, the file supp-pdf.tex must be installed. -It is part of the TexLive texmf ConTeXt package. On Linux, the name -of the package is context or texlive-context. The design document and -the specification document require the xy-pic package, which is -included in texlive-pictures. +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 +Linux, you may also have to install texlive-context. If you want to build the documentation from the sources, and you don't have and want to install the cmarrows package for Metapost, comment diff --git a/doc/bcasyntax.tex b/doc/bcasyntax.tex --- a/doc/bcasyntax.tex +++ b/doc/bcasyntax.tex @@ -45,7 +45,7 @@ \\ &$\mid$&$(\sym{pubk}\mbox{ id}\mbox{ string}) \mid(\sym{privk}\mbox{ id}\mbox{ string})$ \\ &$\mid$&$(\sym{ltk}\mbox{ id id})\mid\mbox{string}\mid(\sym{cat}\mbox{ term+})$ -\\ &$\mid$&$(\sym{enc}\mbox{ term+ term})$ +\\ &$\mid$&$(\sym{enc}\mbox{ term+ term})\mid(\sym{hash}\mbox{ term+})$ \\ role-alist&$\leftarrow$&$ (\sym{non-orig}\mbox{ ht-term}\ast)\mbox{ role-alist}$ \\ &$\mid$&$(\sym{uniq-orig}\mbox{ term}\ast)\mbox{ role-alist}\mid\ldots$ diff --git a/doc/cpsa.bib b/doc/cpsa.bib --- a/doc/cpsa.bib +++ b/doc/cpsa.bib @@ -225,11 +225,11 @@ OPTannote = {} } -@unpublished{algimpl, +@unpublished{algimpl11, author = {Moses Liskov and John D. Ramsdell}, title = {Implementing Strand Space Algebras}, - note = {Unpublished manuscript, submitted to {ESORICS} 2011}, - year = 2010 + note = {\url{http://www.ccs.neu.edu/home/ramsdell/papers/algimpl.pdf}}, + year = 2011 } @incollection{ComonLundhMillen10, @@ -270,7 +270,9 @@ publisher = {Springer Berlin / Heidelberg}, issn = {1615-5262}, keyword = {Computer Science}, - pages = {1--19}, + pages = {63-81}, + volume = {10}, + issue = {2}, url = {http://dx.doi.org/10.1007/s10207-011-0124-7}, note = {10.1007/s10207-011-0124-7}, year = {2011} 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 @@ -124,6 +124,8 @@ \begin{tabular}{@{}ll} $\enc{\cdot}{(\cdot)}\colon\dom{mesg}\times\dom{mesg}\rightarrow\dom{mesg}$ &Encryption\\ +$\#\colon\dom{mesg}\rightarrow\dom{mesg}$ +&Hashing\\ $(\cdot,\cdot)\colon\dom{mesg}\times\dom{mesg}\rightarrow\dom{mesg}$ &Pairing\\ ``\ldots''$\colon\dom{mesg}$& Tag constants\\ @@ -165,6 +167,8 @@ \sembrack{\texttt{"}\ldots\texttt{"}}&{}={}&\mbox{``\ldots''}\\ \sembrack{\texttt{(enc~}t_0~\ldots~t_{n-1}~t_n\texttt{)}}&{}={}& \enc{\sembrack{\texttt{(cat~}t_0~\ldots~t_{n-1}\texttt{)}}}{\sembrack{t_n}}\\ +\sembrack{\texttt{(hash~}t_0~\ldots~t_{n-1}\texttt{)}}&{}={}& +\hash{\sembrack{\texttt{(cat~}t_0~\ldots~t_{n-1}\texttt{)}}}\\ \sembrack{\texttt{(cat~}t\texttt{)}}&{}={}&\sembrack{t}\\ \sembrack{\texttt{(cat~}t_0~t_1~\ldots\texttt{)}}&{}={}& (\sembrack{t_0},\sembrack{\texttt{(cat~}t_1~\ldots\texttt{)}}) @@ -296,20 +300,23 @@ \emph{decryption key} function returns the key used to decrypt a term if it is an encryption, otherwise it returns an error indicator. The \emph{encryptions} function returns the set of encryption terms -carried by a term, each one paired with its encryption key. The -penetrator derivable function from the section in the specification of -the same name is in the interface. Given a derivable predicate that -has been specialized with a given set of supported terms and a set of -atoms to avoid, a target term, and a source term, the -\emph{protectors} function returns an error indicator if the target is -carried by the source outside of an encryption, where the derivable -predicate is used to determine if a decryption key can be used to -expose the target. Otherwise, it returns a set of encryptions in the -source that carry the target and have underivable decryption keys. If -two encryptions protect the target, only the outside one is returned. -The inside encryption is the one that is carried by the outside -encryption. Pseudo code for the decryption key and the protectors -functions is in the specification. +carried by a term, each one paired with its encryption key. {\cpsa} +treats a hashed term as if it were an encryption in which the term +that is hashed is the encryption key, so hashes with their content is +also returned by this function. The penetrator derivable function +from the section in the specification of the same name is in the +interface. Given a derivable predicate that has been specialized with +a given set of supported terms and a set of atoms to avoid, a target +term, and a source term, the \emph{protectors} function returns an +error indicator if the target is carried by the source outside of an +encryption, where the derivable predicate is used to determine if a +decryption key can be used to expose the target. Otherwise, it +returns a set of encryptions in the source that carry the target and +have underivable decryption keys. If two encryptions protect the +target, only the outside one is returned. The inside encryption is +the one that is carried by the outside encryption. Pseudo code for +the decryption key and the protectors functions is in the +specification. \chapter{Protocols and Preskeletons}\label{cha:prots and preskels} @@ -1043,7 +1050,8 @@ \cn{ltk}\colon\dom{name}\times\dom{name}\rightarrow\dom{skey}$\\ $\cn{enc}\colon\dom{mesg} \times\dom{mesg}\rightarrow\dom{mesg}\quad -\cn{cat}\colon\dom{mesg} +\cn{hash}\colon\dom{mesg}\rightarrow\dom{mesg}$\\ +$\cn{cat}\colon\dom{mesg} \times\dom{mesg}\rightarrow\dom{mesg}\quad C_i\colon\dom{mesg}$\\[1ex] Axiom: $\cn{invk}(\cn{invk}(x))\approx x$ for $x\colon\dom{akey}$\\ \caption{Basic Crypto Order-Sorted Signature}\label{tab:order-sorted} @@ -1052,10 +1060,11 @@ Terms are constructed from a set $I$ of identifiers\index{identifiers} and a set of functions symbols. The symbols of arity one are -\cn{text}, \cn{data}, \cn{name}, \cn{skey}, \cn{akey}, \cn{pubk}, and -\cn{invk}. The symbols of arity two are \cn{ltk}, \cn{cat}, and -\cn{enc}. The signature is given in Table~\ref{tab:many-sorted}. -Grammar rules define the terms used by this algebra. +\cn{text}, \cn{data}, \cn{name}, \cn{skey}, \cn{akey}, \cn{pubk}, +\cn{invk}, and \cn{hash}. The symbols of arity two are \cn{ltk}, +\cn{cat}, and \cn{enc}. The signature is given in +Table~\ref{tab:many-sorted}. Grammar rules define the terms used by +this algebra. \begin{table} \begin{center} @@ -1066,7 +1075,9 @@ \cn{ltk}\colon\dom{name}\times\dom{name}\rightarrow\dom{skey}$\\ $\cn{enc}\colon\dom{mesg} \times\dom{mesg}\rightarrow\dom{mesg}\quad -\cn{cat}\colon\dom{mesg} +\cn{hash}\colon\dom{mesg} +\rightarrow\dom{mesg}$\\ +$\cn{cat}\colon\dom{mesg} \times\dom{mesg}\rightarrow\dom{mesg}\quad C_i\colon\dom{mesg}$\\ $\cn{name}\colon\dom{name}\rightarrow\dom{mesg}\quad \cn{text}\colon\dom{text}\rightarrow\dom{mesg}\quad @@ -1103,10 +1114,10 @@ The set of terms $T$ is defined as follows. $$ T \leftarrow I \mid B \mid Q \mid \cn{cat}(T, T) \mid \cn{enc}(T, -T)$$ where $Q$ is the set of tags, represented by quoted string -literals. The second argument in \cn{enc} is a term for a key. A -term of the form $x$ is called an indeterminate, and the identifier -occurrence has sort~\dom{mesg}. +T) \mid \cn{hash}(T)$$ where $Q$ is the set of tags, represented by +quoted string literals. The second argument in \cn{enc} is a term for +a key. A term of the form $x$ is called an indeterminate, and the +identifier occurrence has sort~\dom{mesg}. The terms of interest are \index{well-formed term}well-formed. A term is \emph{well-formed} if every occurrence of each identifier has the @@ -1232,6 +1243,8 @@ \begin{tabular}{@{}ll} $\enc{\cdot}{(\cdot)}\colon\dom{mesg}\times\dom{mesg}\rightarrow\dom{mesg}$ &Encryption\\ +$\#\colon\dom{mesg}\rightarrow\dom{mesg}$ +&Hashing\\ $(\cdot,\cdot)\colon\dom{mesg}\times\dom{mesg}\rightarrow\dom{mesg}$ &Pairing\\ ``\ldots''$\colon\dom{mesg}$& Tag constants\\ 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/cpsaoverview.tex b/doc/cpsaoverview.tex --- a/doc/cpsaoverview.tex +++ b/doc/cpsaoverview.tex @@ -38,11 +38,12 @@ construct~\texttt{k}. Non-atomic terms are constructed by applications of encryption -(\texttt{enc}) and pairing (\texttt{cat}), where $n$-ary concatenation -is parsed right-associatively. The second argument of an encryption -is the key. Encryption may also be written in an $n$-ary form where -the last argument is the key and the arguments preceding it are -implicitly concatenated. +(\texttt{enc}), hashing (\texttt{hash}), and pairing (\texttt{cat}), +where $n$-ary concatenation is parsed right-associatively. The second +argument of an encryption is the key. Encryption may also be written +in an $n$-ary form where the last argument is the key and the +arguments preceding it are implicitly concatenated. Hashing also may +written in an $n$-ary form and its arguments are implicitly concatenated. A term carries one of its subterms if the possession of the right set of keys allows the extraction of the subterm. The carries relation is 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 @@ -193,22 +193,27 @@ \texttt{(invk~k)} will be written as $K^{-1}$, and \texttt{(pubk~n)} as $K_{N}$. -The terms in this algebra are freely generated from the atoms, -tags, encryption, and concatenation. A tag is a quoted constant. +The terms in this algebra are freely generated from the atoms, tags, +concatenation, encryption, and hashing. A tag is a quoted constant. +The concatenation of terms~$t$ and~$t'$ is~$t,t'$ in traditional infix +notation and \texttt{(cat $t$ $t'$)} in S-expression syntax. The +comma operator is right associative and \texttt{(cat $a$ $b$ $c$ $d$)} +is equivalent to \texttt{(cat $a$ (cat $b$ (cat $c$ $d$)))}. Given~$t$, the term to be protected, and key term~$k$, the encryption of~$t$ using~$k$ is~$\enc{t}{k}$ in traditional notation and \texttt{(enc $t$ $k$)} in S-expression syntax. The term represents asymmetric encryption when the key is of sort \dom{akey}, otherwise it -represents symmetric encryption. The concatenation of terms~$t$ -and~$t'$ is~$t,t'$ in traditional infix notation and \texttt{(cat $t$ - $t'$)} in S-expression syntax. The comma operator is right -associative and \texttt{(cat $a$ $b$ $c$ $d$)} is equivalent to -\texttt{(cat $a$ (cat $b$ (cat $c$ $d$)))}. Finally, \texttt{(enc $a$ - $b$ $c$ $d$ $k$)} is equivalent to \texttt{(enc (cat $a$ $b$ $c$ - $d$) $k$)}. Figure~\ref{fig:ns responder} on Page~\pageref{fig:ns - responder} contains examples of \textsc{bca} message terms. Also -see \textsc{term} in Table~\ref{tab:syntax}, Appendix~\ref{sec:syntax - reference}. +represents symmetric encryption. Additionally, \texttt{(enc $a$ $b$ + $c$ $d$ $k$)} is equivalent to \texttt{(enc (cat $a$ $b$ $c$ $d$) + $k$)}. Given~$t$, the term to be hashed, its hash is $\hash{t}$ in +traditional notation and \texttt{(hash $t$)} in S-expression syntax. +{\cpsa} treats a hashed term as if it were an encryption in which the +term that is hashed is the encryption key. As with encryption, +\texttt{(hash $a$ $b$ $c$ $d$)} is equivalent to \texttt{hash (cat $a$ + $b$ $c$ $d$))}. Figure~\ref{fig:ns responder} on +Page~\pageref{fig:ns responder} contains examples of \textsc{bca} +message terms. Also see \textsc{term} in Table~\ref{tab:syntax}, +Appendix~\ref{sec:syntax reference}. A message term \emph{carries}\index{carries} a subterm of the message if the possession of the right set of keys allows the extraction of @@ -1123,19 +1128,6 @@ originating data is carried in fields with predictable values, the convention is to use the sort \dom{data} for uniquely originating data, and sort \dom{text} for the other fields. - -Protocols that make use of \index{hashing}hashing can be handled by -encrypting the tag \texttt{"hash"} using the value to be hashed as the -key. If the hash value is a variable of sort \dom{mesg}, a tag must -be added to the key so as to force {\cpsa} to use symmetric -encryption. The following {\cpsa} macro captures the usage pattern. - -\begin{quote} -\begin{verbatim} -(defmacro (hash x) - (enc "hash" (cat "hash" x))) -\end{verbatim} -\end{quote} When looking at the output, try extracting the shapes first. If the shapes only version of the output does not answer your questions, try 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 @@ -50,6 +50,7 @@ \newcommand{\role}{\mathsf{r}} \newcommand{\skel}{\mathsf{k}} \newcommand{\rl}{\fn{rl}} +\newcommand{\inst}{\mathsf{i}} \newcommand{\nodes}{\fn{nodes}} \newcommand{\lsn}{\fn{lsn}} \newcommand{\init}{\fn{init}} @@ -187,6 +188,8 @@ \begin{tabular}{@{}ll} $\enc{\bullet}{(\cdot)}\colon\dom{mesg}\times\dom{mesg}\rightarrow\dom{mesg} $&Encryption\\ +$\hash{(\cdot)}\colon\dom{mesg}\rightarrow\dom{mesg} +$&Hashing\\ $(\bullet,\bullet)\colon\dom{mesg}\times\dom{mesg}\rightarrow\dom{mesg}$ &Pairing\\ ``\ldots''$\colon{}\dom{mesg}$& Tag constants\\ @@ -240,7 +243,8 @@ {}\cup\{\{(t_0,t_1)\mid t_0\in T_0, t_1\in T_1\}\mid T_0\in\alga^n,T_1\in\alga^n\}\\ {}\cup\{\{\enc{t_0}{t_1}\mid t_0\in T_0, t_1\in T_1\}\mid - T_0\in\alga^n,T_1\in\alga^n\} + T_0\in\alga^n,T_1\in\alga^n\}\\ +{}\cup\{\{\hash{t}\mid t\in T\}\mid T\in\alga^n\} \end{array}\\ \alga = \alga_{\dom{mesg}}&\bigcup_{n\in\nat}\alga^n \end{array}$$ @@ -280,12 +284,15 @@ t&\mbox{otherwise.} \end{array}\right.$$ -An important property possessed by the algebra is that for all $T\in\alga$, -if there are any encryptions in $T$ then all members of $T$ are encryptions. -As a result, a message can be identified as representing an encryption -and if it is, decomposed into its plaintext and its decryption key. -This property is a consequence of the fact that equations relate -atoms, not arbitrary messages. A similar property holds for pairs. +An important property possessed by the algebra is that for all +$T\in\alga$, if there are any encryptions in $T$ then all members of +$T$ are encryptions. As a result, a message can be identified as +representing an encryption and if it is, decomposed into its plaintext +and its decryption key. This property is a consequence of the fact +that equations relate atoms, not arbitrary messages. A similar +property holds for pairs and hashes. A hash\index{hash} is treated as +a kind of encryption in which the term that is hashed is the +encryption key. We write $\alga_X$ when it is important to identify the variable set~$X$ that generates the algebra. Given two variable sets~$X$ @@ -470,7 +477,9 @@ \seq{\inbnd(x, y),\outbnd x,\outbnd y}\\ \mbox{Encrypt}(x,y\colon\top)& \seq{\inbnd x,\inbnd y,\outbnd\enc{x}{y}}& -\seq{\inbnd\enc{x}{y},\inbnd \fn{inv}(y),\outbnd x} +\seq{\inbnd\enc{x}{y},\inbnd \fn{inv}(y),\outbnd x}\\ +\mbox{Hash}(x\colon\top)& +\seq{\inbnd x,\outbnd\hash{x}} \end{array}$$ \caption{Basic Crypto Algebra Penetrator Role Traces}\label{fig:pen} \end{figure} @@ -590,12 +599,12 @@ strands, and adjusting the communication ordering $\to$ appropriately. The set of bundles denoted by preskeleton~$k$, $\sembrack{k}$, is: -$$\sembrack{k_0} = \{\Upsilon\mid -\mbox{$k_0\homomorphism{\phi,\sigma}k_1$ and $k_1$ realizes modulo +$$\sembrack{k} = \{\Upsilon\mid +\mbox{$k\homomorphism{\phi,\sigma}k'$ and $k'$ realizes modulo listeners $\Upsilon$}\}$$ A {\cpsa} algorithm is \emph{complete} if -when given a preskeleton~$k_0$, either the algorithm diverges, or else it +when given a preskeleton~$k$, either the algorithm diverges, or else it terminates and produces a finite set of realized skeletons~$K$, such -that $\sembrack{k_0}=\bigcup_{k_1\in K}\sembrack{k_1}$. +that $\sembrack{k}=\bigcup_{k'\in K}\sembrack{k'}$. \label{def:preskeleton denotation} \section{Blanchet's Simple Example Protocol}\label{sec:blanchet's @@ -640,7 +649,7 @@ &\{\init(a_0,b_0,s_0,d_0),\resp(a_1,b_1,s_1,d_1)\}, &\mbox{Protocol}\\ &\seq{\seq{\outbnd\enc{\enc{s}{a^{-1}}}{b},\inbnd\enc{d}{s}}}, -&\mbox{Strands}\\ +&\mbox{Traces}\\ &\emptyset, &\mbox{Node orderings}\\ &\{a^{-1},b^{-1}\}, @@ -667,7 +676,7 @@ \seq{\outbnd\enc{\enc{s}{a^{-1}}}{b},\inbnd\enc{d}{s}},\\ \seq{\inbnd\enc{\enc{s}{a^{-1}}}{b},\outbnd\enc{d}{s}}\rangle, \end{array} -&\mbox{Strands}\\ +&\mbox{Traces}\\ &\{(1,1)\prec(2,1),(2,2)\prec(1,2)\}, &\mbox{Node orderings}\\ &\{a^{-1},b^{-1}\}, @@ -706,7 +715,7 @@ &\{\init(a_0,b_0,s_0,d_0),\resp(a_1,b_1,s_1,d_1)\}, &\mbox{Protocol}\\ &\seq{\seq{\inbnd\enc{\enc{s}{a^{-1}}}{b},\outbnd\enc{d}{s}}}, -&\mbox{Strands}\\ +&\mbox{Traces}\\ &\emptyset, &\mbox{Node orderings}\\ &\{a^{-1},b^{-1}\}, @@ -730,7 +739,7 @@ \seq{\outbnd\enc{\enc{s}{a^{-1}}}{b'}}\rangle, \end{array} &\begin{array}[t]{@{}l} -\mbox{Strands}\\ +\mbox{Traces}\\ \mbox{\emph{Note key is $b'$ not $b$!}} \end{array}\\ &\{(2,1)\prec(1,1)\}, @@ -755,7 +764,7 @@ &\seq{ \seq{\inbnd\enc{\enc{s}{a^{-1}}}{b},\outbnd\enc{d}{s}}, \seq{\inbnd d,\outbnd d}}, -&\mbox{Strands}\\ +&\mbox{Traces}\\ &\{(1,2)\prec(2,1), &\mbox{Node orderings}\\ &\{a^{-1},b^{-1}\}, @@ -797,7 +806,7 @@ &\{\init(a_0,b_0,m_0),\resp(a_1,b_1,m_1),\lsn(x)\}, &\mbox{Protocol}\\ &\seq{\seq{\outbnd\enc{\enc{m}{b},a}{b}},\seq{\inbnd m}}, -&\mbox{Strands}\\ +&\mbox{Traces}\\ &\emptyset, &\mbox{Node orderings}\\ &\{a^{-1},b^{-1}\}, @@ -888,6 +897,27 @@ \caption{A Bundle Realized by the Example Skeleton}\label{fig:bundle} \end{figure} +\section{External Syntax and Instances}\label{sec:instances} + +The external syntax used by {\cpsa} is a little different than what +has been described here. In the external syntax, the trace and the +role associated with a strand is specified by an +\index{instance}\emph{instance}. An instance is of the form +$\inst(r,h,\sigma)$, where~$r$ is a role, $h$ specifies the length of +a trace instantiated from the role, and~$\sigma$ specifies how to +instantiate the variables in the role to obtain the trace. Thus when +$r=\role_Y(C,N,U)$, the trace associated with $\inst(r,h,\sigma)$ is +$\sigma\circ\prefix{C}{h}$. An instance is well-formed if $1\leq +h\leq|C|$, and $\sdom(\sigma)$ is the set of variables that occur +in~$\prefix{C}{h}$. + +In the external syntax, the role map and sequence of traces are +replaced by a sequence of instances. So for preskeleton +$\skel_X(\rl,P,\Theta_X,\prec,N,U)$ the external syntax is +$\skel_X(P,I,\prec,N,U)$, where for each $s\in\sdom(\Theta_x)$, +$I(s)=\inst(r,h,\sigma)$, $r=\rl(s)$, and the trace of +$\inst(r,h,\sigma)$ is $\Theta_X(s)$. + \chapter{Algorithms as Reduction Systems}\label{chp:algorithms} Algorithms in this paper are specified as abstract reduction @@ -1101,11 +1131,14 @@ $k_0\reduction{\ops{S}_\sigma}k\reduction{\ops{C}_{s,s'}}k_1$, $k_0\homomorphism{\phi,\sigma}k_1$, and $k_1\homomorphism{\phi',\sigma'}k_0$, where -$\comp{\phi}{\phi'}=\idphi$ and $\comp{\sigma}{\sigma'}=\idsigma$. -In particular $\phi=\phi_{s,s'}$ and $\phi'=\phi'_s$ -with~$\phi_{s,s'}$ and~$\phi'_s$ as in Definition~\ref{def:compression - operator}. The bidirectional homomorphism requirement leads to the -following definition. +$\comp{\phi}{\phi'}=\idphi$ and +$\comp{\sigma}{\sigma'}=\idsigma$.\footnote{In category theory, + $(\phi',\sigma')$ is a section of $(\phi,\sigma)$, and + $(\phi,\sigma)$ is a retraction of $(\phi',\sigma')$.} In +particular $\phi=\phi_{s,s'}$ and $\phi'=\phi'_s$ with~$\phi_{s,s'}$ +and~$\phi'_s$ as in Definition~\ref{def:compression operator}. The +bidirectional homomorphism requirement leads to the following +definition. \begin{defn}[Pruning]\label{def:pruning} Suppose skeleton~$k_0$ has a redundant strand~$s$. Then there exists @@ -1145,6 +1178,18 @@ point-of-view skeleton, but the notation in the chapter on generalization shows how it might be done. +\begin{defn}[Thinning] +Two strands $s$ and $s'$ in a skeleton $k$ are \emph{effectively + equivalent} if $k$ with $s$ removed and $k$ with $s'$ removed are +isomorphic. We can define a different form of pruning based on this +idea. Skeleton $k_0$ reduces to skeleton $k_1$ by pruning, written +$k_0\reduction{\ops{P}_s}k_1$, if and only if there exists a strand +$s'$ that is effectively equivalent to $s$ in $k_0$ and $k_1$ is +isomorphic to both $k_0$ with $s$ removed and $k_0$ with $s'$ removed. +\end{defn} + +Thinning is not used yet. + \section{Reduction Systems} Notice that a setwise hulling reduction may produce the empty set, but @@ -1194,7 +1239,8 @@ \fn{enc}(t_0,t_1)=\seq{\inbnd t_0,\inbnd t_1, \outbnd\enc{t_0}{t_1}}\\ \fn{dec}(t_0,t_1)=\seq{\inbnd\enc{t_0}{t_1}, -\inbnd t_2,\outbnd t_0},\mbox{ where $t_2=\fn{inv}(t_1)$} +\inbnd t_2,\outbnd t_0},\mbox{ where $t_2=\fn{inv}(t_1)$}\\ +\fn{hash}(t)=\seq{\inbnd t,\outbnd\hash t} \end{array}$$ \caption{Penetrator Traces}\label{fig:pen traces} \end{figure} @@ -1234,13 +1280,16 @@ [\mbox{by $\fn{dec}(t_0,t_1)$}] \end{equation} -There are two constructive steps. +There are three constructive steps. $$\infer{\der{t_0}{T_p}{T_a}\qquad\der{t_1}{T_p}{T_a}}% {\der{(t_0,t_1)}{T_p}{T_a}}\quad [\mbox{by $\fn{cat}(t_0,t_1)$}]$$ $$\infer{\der{t_0}{T_p}{T_a}\qquad\der{t_1}{T_p}{T_a}}% {\der{\enc{t_0}{t_1}}{T_p}{T_a}}\quad [\mbox{by $\fn{enc}(t_0,t_1)$}]$$ +$$\infer{\der{t}{T_p}{T_a}}% +{\der{\hash{t}}{T_p}{T_a}}\quad +[\mbox{by $\fn{hash}(t)$}]$$ There are three rules for indivisible messages. $$\der{C_i}{T_p}{T_a}\quad @@ -1444,7 +1493,7 @@ Figure~\ref{fig:cows} displays the iterative procedure that breaks the cyclic dependencies. Each step of the iteration improves an approximation of a solution to the problem. The correctness of this -function is shown in~\cite{algimpl}, although for a version of the +function is shown in~\cite{algimpl11}, although for a version of the algorithm with the alternate definition for the function~$\fn{fold}$ in Figure~\ref{fig:fold}. @@ -1502,8 +1551,8 @@ $t=\msg_k(n)$ if \begin{enumerate} \item $p$ is a carried position in~$t$, -\item either $t\termat p\in U_k$ or $t\termat p=\enc{t_0}{t_1}$ - and~$t_1$ is not derivable before~$n$ in~$k$, +\item either $t\termat p\in U_k$, $t\termat p=\hash t_1$, or $t\termat + p=\enc{t_0}{t_1}$ and~$t_1$ is not derivable before~$n$ in~$k$, \item $\fn{esc}(k,n,t\termat p)$ is defined, and \item $\fn{anc}(t,p)\cap \fn{esc}(k,n,t\termat p)=\emptyset$. \end{enumerate} @@ -1512,8 +1561,10 @@ The message at a critical position is called an \emph{authentication test}. It is a \index{nonce test}\emph{nonce test} if the message is an atom, otherwise it is a \index{encryption test}\emph{encryption - test}. Observe that every critical message at a node in a skeleton -is not derivable at the node. + test}. (A hash\index{hash} is treated as a kind of encryption in +which the term that is hashed is the encryption key.) Observe that +every critical message at a node in a skeleton is not derivable at the +node. \begin{conj} A reception node is unrealized iff it has a critical position. @@ -1538,7 +1589,7 @@ \item for some~$t_p\in\outpred(k_1,n_1)$, $t_1$ is not carried only within~$T_1$ in~$t_p$, or \item - $\fn{targ}(t_1,T_1)\setminus\sigma(\fn{targ}(t_0,T_0))\neq\emptyset$ + $\fn{targ}(t_1,\fn{esc}(k_1,n_1,t_1))\setminus\sigma(\fn{targ}(t_0,T_0))\neq\emptyset$ and there are variables in $k$'s protocol that are not atoms, or \item the decryption key of a member of~$T_1$ is derivable before~$n_1$ in~$k_1$, or @@ -1919,11 +1970,12 @@ message is the same as the expected message, and abort the run if not. Here is an example of when the second behavior is desired. In -{\cpsa}, encryption can be used to represent hashing. The hash of~$t$, -$\#t$, expands to $\enc{\mbox{``hash''},t}{h}$, where~$h$ is an -asymmetric key known to all, but no one knows~$h^{-1}$. The tag -``hash'' is added to the encryption so as to ensure a hash is never -confused with other uses of encryption. +{\cpsa}, before hashing was part of the algebra, an encryption was +used to represent hashing. The hash of~$t$, $\#t$, expanded to +$\enc{\mbox{``hash''},t}{h}$, where~$h$ was an asymmetric key known to +all, but no one knew~$h^{-1}$. The tag ``hash'' was added to the +encryption so as to ensure a hash was never confused with other uses of +encryption. A role does not specify a valid program if the only possible way of interpreting the event~$\inbnd\#t$ is by using~$h^{-1}$ to decrypt @@ -2040,12 +2092,12 @@ is a formula in the language of order-sorted first-order logic called a \index{shape analysis sentence}\emph{shape analysis sentence,} often shortened to a shape sentence. The sentence has a special form, -$\all{X}\Psi\rightarrow\bigvee_i\some{Y_i}\Delta_i\wedge\Phi_i$, +$\all{X}(\Psi\supset\bigvee_i\some{Y_i}(\Delta_i\wedge\Phi_i$)), where~$\Psi$ and~$\Phi_i$ are conjunctions of atomic formulas and~$X$ and~$Y_i$ are variable sets. This fragment of first-order logic is called coherent logic. Formula~$\Psi$ describes the point-of-view -skeleton~$k$. For each homomorphism to a shape, -$k\homomorphism{\delta_i}k_i$, formula~$\Delta_i$ describes the +skeleton~$k_0$. For each homomorphism to a shape, +$k_0\homomorphism{\delta_i}k_i$, formula~$\Delta_i$ describes the structure preserving maps~$\delta_i$, and the shape~$k_i$ is described by~$\Phi_i$. @@ -2077,19 +2129,17 @@ zero and, of course, equality is binary. We define~$\form(k)=(Y,\Phi)$, where~$\Phi$ is $k$'s skeleton formula, -and~$Y$ is the formula's variable set. Let -$k=\skel_X(\rl,P,\Theta,\prec,N,U)$. The variable set~$Y$ is~$X$ -augmented with a variable~$z_s\colon\dom{nat}$ for each strand -$s\in\sdom(\Theta)$. The formula~$\Phi$ is a conjunction of atomic +and~$Y$ is the formula's variable set. Using the external syntax +presented in Section~\ref{sec:instances}, let +$k=\skel_X(P,I,\prec,N,U)$. The variable set~$Y$ is~$X$ augmented +with a variable~$z_s\colon\dom{nat}$ for each strand +$s\in\sdom(I)$. The formula~$\Phi$ is a conjunction of atomic formulas composed as follows. \begin{itemize} -\item For each $s\in\sdom(\Theta)$, let $r=\rl(s)=\role_Y(C,N,U)$, - $\comp{\sigma}{C|_h}=\Theta(s)$, and $h=|\Theta(s)|$. For each - variable $x\in\sdom(\sigma)$ and term $t=\sigma(x)$, assert - $P[r,h,x](z_s,t)$. Note $\sigma\colon\alga_Y\to\alga_X$ is the - homomorphism described near the end of Chapter~\ref{chp:strand - spaces and bundles}. +\item For each $s\in\sdom(I)$, let $I(s)=\inst(r,h,\sigma)$. For + each variable $x\in\sdom(\sigma)$ and term $t=\sigma(x)$, assert + $P[r,h,x](z_s,t)$. \item For each $(s,i)\prec(s',i')$, assert $\cn{prec}(z_s,i,z_{s'},i')$. \item For each $t\in N$, assert $\cn{non}(t)$. @@ -2104,20 +2154,20 @@ the~$\prec$ relation. The missing relations must be asserted as axioms for proper handling of a shape sentence. -Given a set of homomorphisms $k\homomorphism{\delta_i}k_i$, its shape +Given a set of homomorphisms $k_0\homomorphism{\delta_i}k_i$, its shape sentence is \begin{equation} -\sent(k\homomorphism{\delta_i}k_i)=\all{X}\Psi\rightarrow -\bigvee_i\some{Y_i}\Delta_i\wedge\Phi_i,\label{eq:shape sentence} +\sent(k_0\homomorphism{\delta_i}k_i)=\all{X}(\Psi\supset +\bigvee_i\some{Y_i}(\Delta_i\wedge\Phi_i)),\label{eq:shape sentence} \end{equation} -where $\form(k)=(X,\Psi)$. The same procedure produces~$Y_i$ +where $\form(k_0)=(X,\Psi)$. The same procedure produces~$Y_i$ and~$\Phi_i$ for shape~$k_i$ with one proviso---the variables in $Y_i$ that also occur in~$X$ must be renamed to avoid trouble while encoding the structure preserving maps~$\delta_i$. \begin{figure} $$\begin{array}{l} -\all{a_0,b_0\colon A, s_0\colon S, d_0\colon D, z_0\colon N}\\ +\all{a_0,b_0\colon A, s_0\colon S, d_0\colon D, z_0\colon N}(\\ \quad\init_{2,a}(z_0,a_0)\wedge \init_{2,b}(z_0,b_0)\wedge \init_{2,s}(z_0,s_0)\wedge @@ -2125,9 +2175,9 @@ \quad\cn{non}(a_0^{-1})\wedge \cn{non}(b_0^{-1})\wedge \cn{uniq}(s_0)\wedge\cn{orig}(s_0,z_0,1)\\ -\quad\rightarrow\\ +\quad\supset\\ \quad\some{a_1,b_1\colon A, s_1\colon S, d_1\colon D, z_1,z_2\colon - N}\\ + N}(\\ \qquad z_0=z_1\wedge a_0=a_1\wedge b_0=b_1\wedge s_0=s_1\wedge d_0=d_1\wedge{}\\ \qquad\init_{2,a}(z_1,a_1)\wedge \init_{2,b}(z_1,b_1)\wedge @@ -2141,7 +2191,7 @@ \cn{prec}(z_2,2,z_1,2)\wedge{}\\ \qquad\cn{non}(a_1^{-1})\wedge \cn{non}(b_1^{-1})\wedge -\cn{uniq}(s_1)\wedge\cn{orig}(s_1,z_1,1) +\cn{uniq}(s_1)\wedge\cn{orig}(s_1,z_1,1))) \end{array}$$ \caption{A Shape Analysis Sentence for Blanchet's Protocol}\label{fig:blanchet's shape analysis sentence} @@ -2153,7 +2203,7 @@ of~$\sigma_i$ and the term it maps to. Map~$\phi_i$ is coded as equalities between strand variables in~$\Psi$ and strand variables in~$\Phi_i$. Let~$Z$ be the sequence of strand variables freshly -generated for~$k$, and~$Z_i$ be the ones generated for~$k_i$. The +generated for~$k_0$, and~$Z_i$ be the ones generated for~$k_i$. The strand mapping part of~$\Delta_i$ is $\bigwedge_{j\in\sdom(\Theta)}Z(j)=Z_i(\phi_i(j))$. @@ -2166,21 +2216,21 @@ \section{Semantics of Shape Formulas} -Once again, let $k=\skel_X(\rl,P,\Theta,\prec,N,U)$. The universe of -discourse is $\alg{D}=\nat\cup\alga_X$. When formula~$\Psi$ is -satisfied in skeleton~$k$ with variable assignment $\alpha\colon Y\to -\alg{D}$, we write $k,\alpha\models\Psi$. When sentence~$\Sigma$ is -satisfied in skeleton~$k$, we write $k\models\Sigma$. +Let $k=\skel_X(\rl,P,\Theta,\prec,N,U)$. The universe of discourse is +$\alg{D}=\nat\cup\alga_X$. When formula~$\Psi$ is satisfied in +skeleton~$k$ with variable assignment $\alpha\colon Y\to \alg{D}$, we +write $k,\alpha\models\Psi$. When sentence~$\Sigma$ is satisfied in +skeleton~$k$, we write $k\models\Sigma$. For each protocol specific predicate $P[r,h,x]$, $k,\alpha\models P[r,h,x](y,z)$ iff $\alpha(y)\in\nat$, $\alpha(z)\in\alga$, and with -$\alpha(y)=s$, +$\alpha(y)=s$ and $r=\role(C,N,U)$, \begin{enumerate} \item $s\in\sdom(\Theta)$, \item $h\in\sdom(\Theta(s))$, and -\item $\alpha(z)=\sigma(x)$, where $\rl(s)=\role(C,N,U)$, -$\comp{\sigma}{C|_\ell}=\Theta(s)$, and $\ell=|\Theta(s)|$. +\item $\prefix{\Theta(s)}{h}=\sigma\circ\{x\mapsto\alpha(z)\}\circ\prefix{C}{h}$ + for some~$\sigma$. \end{enumerate} In an interpretation, $\rl(s)$ need not be~$r$. The events that make @@ -2204,10 +2254,10 @@ \end{itemize} \begin{thm}\label{thm:skeleton models} -Let $\form(k)=(X,\Psi)$ and $\Phi=\some{X}\Psi$. Formula~$\Phi$ is -satisfied in~$k'$ iff there is a homomorphism from~$k$ to -$k'$, i.e.\ $k'\models\Phi$ iff -$\some{\delta}k\homomorphism{\delta}k'$. +Let $\form(k_0)=(X,\Psi)$ and $\Phi=\some{X}\Psi$. Formula~$\Phi$ is +satisfied in~$k$ iff there is a homomorphism from~$k_0$ to +$k$, i.e.\ $k\models\Phi$ iff +$\some{\delta}k_0\homomorphism{\delta}k$. \end{thm} This theorem corrects the first of the two main results @@ -2215,16 +2265,16 @@ \begin{proof} For the forward direction, assume~$\alpha$ is a variable assignment -for the variables in~$X$ such that $k',\alpha\models\Psi$, and let~$Z$ +for the variables in~$X$ such that $k,\alpha\models\Psi$, and let~$Z$ be the sequence of strand variables constructed while -generating~$\Psi$ from~$k$. Then the pair of maps -$\delta=(\comp{\alpha}{Z},\alpha)$ demonstrate a homomorphism from~$k$ -to~$k'$, i.e.\ each item in the definition of a preskeleton +generating~$\Psi$ from~$k_0$. Then the pair of maps +$\delta=(\comp{\alpha}{Z},\alpha)$ demonstrate a homomorphism from~$k_0$ +to~$k$, i.e.\ each item in the definition of a preskeleton homomorphism on Page~\pageref{def:preskeleton homomorphism} is satisfied. For the reverse direction, assume maps $\delta=(\phi,\sigma)$ are such -that $k\homomorphism{\delta}k'$. Then the desired variable assigment is +that $k_0\homomorphism{\delta}k$. Then the desired variable assigment is $$\alpha(x)=\left\{ \begin{array}{ll} \phi(Z^{-1}(x))&x\in\sran(Z)\\ @@ -2236,10 +2286,10 @@ defined on Page~\pageref{def:preskeleton denotation}. \begin{thm}\label{thm:sentence implies} -Let $k\homomorphism{\delta_i}k_i$ be a complete set of homomorphisms -for shapes $k_i\in K$, and assume $\sembrack{k}=\bigcup_{k'\in - K}\sembrack{k'}$. Then the shape analysis -sentence~$\Sigma=\sent(k\homomorphism{\delta_i}k_i)$ is satisfied in +Let $k_0\homomorphism{\delta_i}k_i$ be a complete set of homomorphisms +for shapes $k_i\in K$, and assume $\sembrack{k_0}=\bigcup_{k\in + K}\sembrack{k}$. Then the shape analysis +sentence~$\Sigma=\sent(k_0\homomorphism{\delta_i}k_i)$ is satisfied in all realized skeletons~$k$, i.e.\ $k\models\Sigma$. \end{thm} @@ -2248,7 +2298,7 @@ skeleton in the image of~$k$ that is not in the image of one of the shapes. Therefore, by Theorem~\ref{thm:skeleton models}, the negation of the hypothesis of the implication is satisfied in all realized -skeletons that are not in the image of~$k$, and the disjunction is +skeletons that are not in the image of~$k_0$, and the disjunction is satisfied in the remaining realized skeletons. \end{proof} diff --git a/doc/cpsatheory.pdf b/doc/cpsatheory.pdf Binary files a/doc/cpsatheory.pdf and b/doc/cpsatheory.pdf differ diff --git a/doc/cpsauser.html b/doc/cpsauser.html --- a/doc/cpsauser.html +++ b/doc/cpsauser.html @@ -5,7 +5,7 @@ - CPSA 2.0 User Guide + CPSA 2.2 User Guide