diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,99 @@ +2015-05-21 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as version 2.5.0 + +2015-04-27 John D. Ramsdell + + * src/CPSA/Lib/Loader.hs (ReturnFail): Added ReturnFail Monad so + that fail is correctly handled. Added Functor and Applicative + instance to support GHC 7.10 base library. + +2015-04-20 John D. Ramsdell + + * cpsa.cabal (Source-Repository): Added github source repository. + +2015-04-10 John D. Ramsdell + + * src/CPSA/Lib/Strand.hs (mkListener): The role used for listener + strands is now the one stored in the protocol. It has a single + variable x of sort mesg as its set of variables. This change + enables satisfaction checking on skeleton that include listeners. + +2015-04-02 John D. Ramsdell + + * src/CPSA/Lib/Strand.hs (hull): Removed the hulling by + deorigination mode and returned to the hulling by compression + algorithm. Hulling is only used on the initial preskeleton. + + * src/CPSA/SAS/SAS.hs (form): Changed the output form from defsas + to defgoal. + +2015-03-30 John D. Ramsdell + + * src/CPSA/Lib/Loader.hs (loadPrimary): Improved the error + messages for ill-formed atomic formulas. + + * src/CPSA/SAS/SAS.hs (loadPOV, loadOtherPreskel): Flushed the + check that an atom assumed to uniquely originate must originate in + a skeleton. In this case, cpsasas generates a uniq assertion + rather than a uniq-at assertion. + +2015-03-27 John D. Ramsdell + + * src/CPSA/Lib/Loader.hs (findGoal): Allow more than one sentence + in a defgoal. + + * src/CPSA/SAS/SAS.hs (Preskel): Added pnon predicate symbol. + + * src/CPSA/Lib/Strand.hs (toSkeleton): Added hulling to the + process of converting an input preskeleton into a skeleton. + +2015-03-26 John D. Ramsdell + + * src/CPSA/Lib/{Characteristic,Strand,Loader}.hs: Added new + toplevel form: defgoal. The characteristic skeleton of the + antecedent in the goal is extracted and used as the initial + skeleton. + +2015-03-24 John D. Ramsdell + + * src/CPSA/Lib/{Reduction,Strand,Loader}.hs: Made it so that when + a shape does not satisfy a goal, an environment showing why is + printed. For each goal, the output is yes when the goal is + satisfied or (no (VAR VAL)...). + +2015-03-20 John D. Ramsdell + + * src/CPSA/Lib/{Goal,Strand,Loader}.hs: Added goal loading and + satisfaction checking. When a shape satisfies all goals in a + point-of-view skeleton, the shape is annotated with + (satifies-all-goals). + +2015-03-19 John D. Ramsdell + + * src/CPSA/Basic/Algebra.hs (Term): Added node variables and + constants for security goals. + + * src/CPSA/SAS/SAS.hs (form): Changed the format of a shape + analysis sentences. Instead of a bare formula, the formula is + wrapped in a defsas form, as in (defsas PROT SAS). Removed the + protocol from role position predicates and parameter predicates. + Replaced function symbols uniq and sprec with uniq-at and str-prec + respectively. + +2015-03-17 John D. Ramsdell + + * src/CPSA/SAS/SAS.hs (displayEq): Use = for function symbol + instead of equal. + +2014-11-24 John D. Ramsdell + + * src/prover9.pl: Added missing mesg predicates in output. + +2014-11-17 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as version 2.4.0 + 2014-11-15 John D. Ramsdell * src/CPSA/SAS/SAS.hs (nodeForm): Fixed bug where some role @@ -26,7 +122,6 @@ 2014-09-05 John D. Ramsdell * cpsa.cabal (Version): Tagged as version 2.3.5 - 2014-09-02 John D. Ramsdell diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,5 +1,22 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.5.0 + +** Added support for security goals + In CPSA, a security goal is expressed as a sentence in first-order + logic. It asserts that if some properties hold for a skeleton, + then some other properties must hold for all shapes computed by + CPSA starting with the skeleton. Security goals can be used to + formally state authentication and secrecy goals of a protocol. + + Security goals have been integrated into the main CPSA program. + The new defgoal form can be used to pose an analysis problem by a + sentence instead of a skeleton. CPSA extracts a point-of-view + skeleton from the antecedent of the formula and then analyzes it. + When it prints a shape, it checks to see if the shape satisfies the + conclusion of the security goal. See cpsagoals.pdf for more + information. + * Changes in version 2.4.0 ** Added program cpsasas diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 2.4.0 +Version: 2.5.0 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3 @@ -46,24 +46,25 @@ Build-Type: Simple Data-Files: index.html readme.html cpsauser.html cpsa.mk Make.hs cpsaprimer.pdf - cpsaoverview.pdf cpsaintroslides.pdf cpsaspec.pdf cpsadesign.pdf - ffgg.scm ns.scm blanchet.scm or.scm woolam.scm yahalom.scm + cpsagoals.pdf cpsaoverview.pdf cpsaintroslides.pdf cpsaspec.pdf + cpsadesign.pdf ffgg.scm ns.scm blanchet.scm or.scm woolam.scm + yahalom.scm goals.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/cpsaintroslides.tex doc/mitreslides.sty - 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/blanchet.mp doc/mitrelogo.mp - doc/cpsa.bib doc/SDAG.lhs + doc/cpsagoals.tex doc/bcasyntax.tex doc/cpsaintroslides.tex + doc/mitreslides.sty 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/blanchet.mp + doc/mitrelogo.mp doc/cpsa.bib doc/SDAG.lhs src/index.html src/cpsacgi src/cpsacgi.py src/cpsajson.py src/split.py src/cpsa2svg src/cpsa.el src/httpd_allow_execmem.te src/cpsaperm.scm src/cpsaops.scm src/preskel src/cpsa.pl src/unsorted.pl src/pp.pl src/sexpr.pl src/perm.pl src/prover9.pl src/zoom.js src/js2hs - src/ghcmemlimit build.xml src/cpsaextras/Main.scala - src/cpsaextras/Pretty.scala src/cpsaextras/Printer.scala - src/cpsaextras/SExpr.scala + src/ghcmemlimit build.xml src/scala/Main.scala + src/scala/Pretty.scala src/scala/Printer.scala + src/scala/SExpr.scala tst/README tst/Makefile tst/Make.hs tst/checktst tst/cpsagraphall tst/cpsashapesall tst/blanchet.scm tst/blanchet.tst tst/completeness-test.scm @@ -78,22 +79,23 @@ tst/epmo_acctnum.lisp tst/epmo-hash.scm tst/epmo-hash.tst tst/epmo-key-hash.scm tst/epmo-key-hash.tst tst/epmo.scm tst/epmo.tst tst/ffgg.scm tst/ffgg.tst tst/fragile_pruning.scm - tst/fragile_pruning.tst tst/hashtest-key-hash.scm - tst/hashtest-key-hash.tst tst/hashtest.scm tst/hashtest.tst - tst/incompleteness_example.scm tst/incompleteness_example.tst - tst/isoreject.scm tst/isoreject.tst tst/kelly1.scm tst/kelly1.tst - tst/kelly64.lisp tst/kerb5.lisp tst/kerberos.scm tst/kerberos.tst - tst/mass2.lsp tst/mass2.tst tst/mass.lsp tst/mass.tst - tst/missing_contraction.scm tst/missing_contraction.tst - tst/neuman-stubblebine-alt.lisp tst/neuman-stubblebine-reauth.lisp - tst/neuman-stubblebine-reauth.lsp tst/neuman-stubblebine-reauth.tst - tst/neuman-stubblebine.scm tst/neuman-stubblebine.tst - tst/no_contraction.scm tst/no_contraction.tst tst/nonaug-prune.scm - tst/nonaug-prune.tst tst/non_transforming.scm - tst/non_transforming.tst tst/nsl3.scm tst/nsl3.tst tst/nsl4cm1.lsp - tst/nsl4cm1.tst tst/nsl4.lisp tst/nsl4resp2.lisp tst/nsl5i.lisp - tst/nsl5.lisp tst/ns-l.scm tst/nslsk.scm tst/nslsk.tst tst/ns-l.tst - tst/ns.scm tst/ns.tst tst/or.scm tst/or.tst tst/pca.scm tst/pca.tst + tst/fragile_pruning.tst tst/goals.scm tst/goals.tst + tst/hashtest-key-hash.scm tst/hashtest-key-hash.tst tst/hashtest.scm + tst/hashtest.tst tst/incompleteness_example.scm + tst/incompleteness_example.tst tst/isoreject.scm tst/isoreject.tst + tst/kelly1.scm tst/kelly1.tst tst/kelly64.lisp tst/kerb5.lisp + tst/kerberos.scm tst/kerberos.tst tst/mass2.lsp tst/mass2.tst + tst/mass.lsp tst/mass.tst tst/missing_contraction.scm + tst/missing_contraction.tst tst/neuman-stubblebine-alt.lisp + tst/neuman-stubblebine-reauth.lisp tst/neuman-stubblebine-reauth.lsp + tst/neuman-stubblebine-reauth.tst tst/neuman-stubblebine.scm + tst/neuman-stubblebine.tst tst/no_contraction.scm + tst/no_contraction.tst tst/nonaug-prune.scm tst/nonaug-prune.tst + tst/non_transforming.scm tst/non_transforming.tst tst/nsl3.scm + tst/nsl3.tst tst/nsl4cm1.lsp tst/nsl4cm1.tst tst/nsl4.lisp + tst/nsl4resp2.lisp tst/nsl5i.lisp tst/nsl5.lisp tst/ns-l.scm + tst/nslsk.scm tst/nslsk.tst tst/ns-l.tst tst/ns.scm tst/ns.tst + tst/or.scm tst/or.tst tst/pca.scm tst/pca.tst tst/pen-non-orig-test.scm tst/pen-non-orig-test.tst tst/pkinit.scm tst/pkinit.tst tst/preprocess.scm tst/preprocess.tst tst/print.scm tst/print.tst tst/pruning1.scm tst/pruning1.tst tst/sigenc.scm @@ -110,8 +112,13 @@ tst/wonthull2.scm tst/wonthull2.tst tst/wonthull3.scm tst/wonthull3.tst tst/wonthull.scm tst/wonthull.tst tst/woolam.scm tst/woolam.tst tst/yahalom-6.3.6.scm tst/yahalom-6.3.6.tst - tst/yahalom.scm tst/yahalom.tst + tst/yahalom.scm tst/yahalom.tst tst/unilateral.scm + tst/unilateral.tst +Source-Repository head + Type: git + Location: git://github.com/ramsdell/cpsa.git + -- Algebra implementations must import CPSA.Lib.CPSA. -- Tools may additionally import CPSA.Lib.Entry. -- No other modules in CPSA.Lib should be imported by applications. @@ -125,9 +132,10 @@ Other-Modules: Paths_cpsa CPSA.Lib.Vector CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr CPSA.Lib.Printer CPSA.Lib.Notation CPSA.Lib.Entry - CPSA.Lib.Algebra CPSA.Lib.Protocol CPSA.Lib.Strand CPSA.Lib.Loader - CPSA.Lib.Displayer CPSA.Lib.Cohort CPSA.Lib.Expand CPSA.Lib.CPSA - CPSA.Lib.Reduction CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra + CPSA.Lib.Algebra CPSA.Lib.Protocol CPSA.Lib.Goal CPSA.Lib.Strand + CPSA.Lib.Characteristic CPSA.Lib.Loader CPSA.Lib.Displayer + CPSA.Lib.Cohort CPSA.Lib.Expand CPSA.Lib.CPSA CPSA.Lib.Reduction + CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra Executable cpsagraph Main-Is: CPSA/Graph/Main.hs diff --git a/doc/Makefile b/doc/Makefile --- a/doc/Makefile +++ b/doc/Makefile @@ -10,6 +10,7 @@ SHELL = /bin/sh PRIMER = cpsaprimer +GOALS = cpsagoals OVERVIEW = cpsaoverview SLIDES = cpsaintroslides DESIGN = cpsadesign @@ -31,8 +32,8 @@ %.ind: %.idx makeindex $* -all: $(PRIMER).pdf $(OVERVIEW).pdf $(SLIDES).pdf \ - $(DESIGN).pdf $(SPEC).pdf +all: $(PRIMER).pdf $(GOALS).pdf $(OVERVIEW).pdf \ + $(SLIDES).pdf $(DESIGN).pdf $(SPEC).pdf $(PRIMER).pdf: $(MP_SRCS:.mp=-0.mps) $(TEX_SRCS) \ $(PRIMER).tex $(PRIMER).bbl @@ -40,6 +41,11 @@ if test -f $(PRIMER).idx; then $(MAKE) $(PRIMER).ind; fi pdflatex $(PRIMER).tex +$(GOALS).pdf: $(MP_SRCS:.mp=-0.mps) $(TEX_SRCS) \ + $(GOALS).tex $(GOALS).bbl + if test ! -f $(GOALS).aux; then pdflatex $(GOALS).tex; fi + pdflatex $(GOALS).tex + $(OVERVIEW).pdf: $(OVERVIEW).tex $(OVERVIEW).bbl if test ! -f $(OVERVIEW).aux; then pdflatex $(OVERVIEW).tex; fi pdflatex $(OVERVIEW).tex @@ -59,8 +65,8 @@ if test -f $(SPEC).idx; then $(MAKE) $(SPEC).ind; fi pdflatex $(SPEC).tex -CLEAN_FILES := $(PRIMER).pdf $(OVERVIEW).pdf $(SLIDES).pdf \ - $(DESIGN).pdf $(SPEC).pdf \ +CLEAN_FILES := $(PRIMER).pdf $(GOALS).pdf $(OVERVIEW).pdf \ + $(SLIDES).pdf $(DESIGN).pdf $(SPEC).pdf \ $(wildcard *.log *.aux *.toc *.mps *.mpx *.lot *.lof) \ $(wildcard *.bbl *.blg *.ind *.idx *.ilg *.out) diff --git a/doc/README b/doc/README --- a/doc/README +++ b/doc/README @@ -8,12 +8,13 @@ * cpsaoverview.pdf: Another attempt at a gentle introduction to CPSA +* cpsagoals.pdf: CPSA and Formal Security Goals, an introduction + to reasoning about security goals using first-order logic. + * cpsaspec.pdf: The CPSA Specification, a formal specification of the algorithm * cpsadesign.pdf: CPSA Design, a description of implementation choices - -* cpsadha.pdf: Diffie-Hellman Algebra (an experiment with known flaws). To build the documentation, you need Metapost and XY-pic. On Linux, Metapost is supplied via the package texlive-metapost, and XY-pic is diff --git a/doc/bcasyntax.tex b/doc/bcasyntax.tex --- a/doc/bcasyntax.tex +++ b/doc/bcasyntax.tex @@ -1,14 +1,18 @@ The complete syntax for the analyzer using the Basic Crypto Algebra is -shown in Table~\ref{tab:syntax}. The start grammar symbol is -\textsc{file}, and the terminal grammar symbols are: \textsc{(, ), - symbol, string, integer,} and the constants set in typewriter font. +shown in Tables~\ref{tab:syntax} and~\ref{tab:goal}. The start +grammar symbol is \textsc{file}, and the terminal grammar symbols +are: \textsc{(, ), symbol, string, integer,} and the constants set in +typewriter font. The language used for stating security goals is in +Table~\ref{tab:goal}. The goal language adds the sort +symbol \texttt{node}. The \textsc{alist}, \textsc{prot-alist}, \textsc{role-alist}, -and \textsc{skel-alist} productions are Lisp style association lists, -that is, lists of key-value pairs, where every key is a symbol. -Key-value pairs with unrecognized keys are ignored, and are available -for use by other tools. On output, unrecognized key-value pairs are -preserved when printing protocols, but elided when printing skeletons. +\textsc{skel-alist}, and \textsc{goal-alist} productions are +Lisp style association lists, that is, lists of key-value pairs, where +every key is a symbol. Key-value pairs with unrecognized keys are +ignored, and are available for use by other tools. On output, +unrecognized key-value pairs are preserved when printing protocols, +but elided when printing skeletons. \begin{table} \newcommand{\sym}[1]{\textup{\texttt{#1}}} @@ -19,7 +23,7 @@ (\sym{herald}~title~alist) \\title&$\leftarrow$&$\mbox{symbol}\mid\mbox{string}$ \\form&$\leftarrow$& -$\mbox{comment}\mid\mbox{protocol}\mid\mbox{skeleton}$ +$\mbox{comment}\mid\mbox{protocol}\mid\mbox{skeleton}\mid\mbox{goal}$ \\ comment&$\leftarrow$& (\sym{comment}~\ldots) \\ protocol&$\leftarrow$& @@ -71,6 +75,34 @@ \end{tabular} \end{center} \caption{{\cpsa} Syntax}\label{tab:syntax} +\end{table} + +\begin{table} +\newcommand{\sym}[1]{\textup{\texttt{#1}}} +\begin{center}\scshape +\begin{tabular}{rcl} +goal&$\leftarrow$& +(\sym{defgoal} id sentence+ goal-alist) +\\ sentence&$\leftarrow$&(\sym{forall} (decl$\ast$) implication) +\\ implication&$\leftarrow$& +(\sym{implies} \mbox{antecedent} \mbox{conclusion}) +\\ conclusion&$\leftarrow$&(\sym{false}) + $\mid$ existential $\mid$ (\sym{or} existential$\ast)$ +\\ existential&$\leftarrow$&(\sym{exists} +(decl$\ast$) antecedent) $\mid$ antecedent +\\ antecedent&$\leftarrow$& atomic $\mid$ (\sym{and} atomic$\ast$) +\\ atomic&$\leftarrow$&(\sym{p} roleid pos nvar) +\\ &$\mid$&(\sym{p} roleid param nvar term) +\\ &$\mid$&(\sym{str-prec} nvar nvar) $\mid$ (\sym{prec} nvar nvar) +\\ &$\mid$&(\sym{non} term) $\mid$ (\sym{pnon} term) $\mid$ (\sym{uniq} term) +\\ &$\mid$&(\sym{uniq-at} term nvar) $\mid$ (= term term) +\\ roleid&$\leftarrow$& string +\\ pos&$\leftarrow$& integer +\\ nvar&$\leftarrow$& id +\\ param&$\leftarrow$& string +\end{tabular} +\end{center} +\caption{{\cpsa} Syntax Continued}\label{tab:goal} \end{table} The contents of a file can be interpreted as a sequence of diff --git a/doc/cpsa.bib b/doc/cpsa.bib --- a/doc/cpsa.bib +++ b/doc/cpsa.bib @@ -223,6 +223,20 @@ OPTannote = {} } +@Manual{cpsagoals09, + title = {{CPSA} and Formal Security Goals}, + OPTkey = {}, + author = {John D.~Ramsdell}, + organization = {The MITRE Corporation}, + OPTaddress = {}, + OPTedition = {}, + OPTmonth = {}, + year = 2015, + note = {In \url{http://hackage.haskell.org/package/cpsa} source + distribution, \texttt{doc} directory}, + OPTannote = {} +} + @Manual{cpsaoverview09, title = {{CPSA} Overview}, OPTkey = {}, @@ -399,10 +413,42 @@ author = {John D. Ramsdell and Joshua D. Guttman and Jonathan K. Millen and Brian O'Hanlon}, title = {An Analysis of the {CAVES} Attestation Protocol using {CPSA}}, - note = {\url{http://arxiv.org/abs/1207.0418v1}}, + note = {\url{http://arxiv.org/abs/1207.0418}}, institution = {The {MITRE} Corporation}, month = dec, year = 2009, type = {{MITRE} Technical Report}, number = {{MTR090213}} +} + +@InProceedings{GuttmanLiskovRowe14, + author = {Joshua D. Guttman and Moses D. Liskov and Paul D. Rowe}, + title = {Security Goals and Evolving Standards}, + booktitle = {Security Standardization Research}, + year = 2014, + editor = {Liqun Chen and Chris Mitchell}, + volume = 8839, + series = {LNCS}, + pages = {93--110}, + month = dec, + publisher = {Springer}, +} + +@Article{Guttman14, + author = {Joshua D. Guttman}, + title = {Establishing and Preserving Protocol Security Goals}, + journal = {Journal of Computer Security}, + year = 2014, + volume = 22, + number = 2, + pages = {201--267}} + +@Unpublished{prover9, + author = {Bill W. McCune}, + title = {Prover9}, + note = {\url{http://www.cs.unm.edu/~mccune/mace4/}}, + OPTkey = {}, + OPTmonth = {}, + OPTyear = {}, + OPTannote = {} } 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 @@ -927,8 +927,12 @@ Provides a common entry point for programs based on the CPSA library. \item[CPSA.Lib.Protocol:] Protocol data structures. +\item[CPSA.Lib.Goal:] +Security goal data structures. \item[CPSA.Lib.Strand:] Instance and preskeleton data structures and support functions. +\item[CPSA.Lib.Characteristic:] +Produces the characteristic skeleton of the antecedent of a goal. \item[CPSA.Lib.Cohort:] Computes the cohort associated with a skeleton or its generalization. \item[CPSA.Lib.Reduction:] @@ -936,7 +940,7 @@ \item[CPSA.Lib.Expand:] Expands macros using definitions in the input. \item[CPSA.Lib.Loader:] -Loads protocols and preskeletons from S-expressions. +Loads protocols, preskeletons, and goals from S-expressions. \item[CPSA.Lib.Displayer:] Displays protocols and preskeletons as S-expressions. \end{description} diff --git a/doc/cpsadiagrams.mp b/doc/cpsadiagrams.mp --- a/doc/cpsadiagrams.mp +++ b/doc/cpsadiagrams.mp @@ -73,11 +73,11 @@ strand.b(3, .5w, delta, btex $\mathstrut\mathit{resp}$ etex, node); % Messages and arrows - label.top(btex $\enc{N_1, A}{K_B}$ etex, .5[a1.e, b1.w]); + label.top(btex $\enc{N_1, A}{K_B}$ etex, .5[a1.c, b1.c]); drawmsg(a1.e -- b1.w); - label.top(btex $\enc{N_1, N_2}{K_A}$ etex, .5[a2.e, b2.w]); + label.top(btex $\enc{N_1, N_2}{K_A}$ etex, .5[a2.c, b2.c]); drawmsg(b2.w -- a2.e); - label.top(btex $\enc{N_2}{K_B}$ etex, .5[a3.e, b3.w]); + label.top(btex $\enc{N_2}{K_B}$ etex, .5[a3.c, b3.c]); drawmsg(a3.e -- b3.w); endfig; @@ -125,15 +125,15 @@ drawsucc(b1.s -- b2.n); drawsucc(b2.s -- b3.n); - label.top(btex $\enc{N_1, A}{K_P}$ etex, .5[a1.e, p1.w]); + label.top(btex $\enc{N_1, A}{K_P}$ etex, .5[a1.c, p1.c]); drawmsg(a1.e -- p1.w); - label.top(btex $\enc{N_1, A}{K_B}$ etex, .5[p2.e, b1.w]); + label.top(btex $\enc{N_1, A}{K_B}$ etex, .5[p2.c, b1.c]); drawmsg(p2.e -- b1.w); - label.top(btex $\enc{N_1, N_2}{K_A}$ etex, .75[b2.w, a2.e]); + label.top(btex $\enc{N_1, N_2}{K_A}$ etex, .75[b2.c, a2.c]); drawmsg(b2.w -- a2.e); - label.top(btex $\enc{N_2}{K_P}$ etex, .5[a3.e, p3.w]); + label.top(btex $\enc{N_2}{K_P}$ etex, .5[a3.c, p3.c]); drawmsg(a3.e -- p3.w); - label.top(btex $\enc{N_2}{K_B}$ etex, .5[p4.e, b3.w]); + label.top(btex $\enc{N_2}{K_B}$ etex, .5[p4.c, b3.c]); drawmsg(p4.e -- b3.w); endfig; @@ -156,17 +156,17 @@ endfor; % Messages and arrows - label.top(btex $\enc{N_1, A}{K_C}$ etex, alpha[a1.e, o1.w]); + label.top(btex $\enc{N_1, A}{K_C}$ etex, alpha[a1.c, o1.c]); drawmsg(a1.e -- beta[a1.e,o1.w]); % Shortened arrow - label.top(btex $\enc{N_1, A}{K_B}$ etex, alpha[b1.w, o1.e]); + label.top(btex $\enc{N_1, A}{K_B}$ etex, alpha[b1.c, o1.c]); drawmsg(beta[b1.w,o1.e] -- b1.w); % Shortened arrow - label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[a2.e, o2.w]); + label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[a2.c, o2.c]); drawmsg(o2.w -- a2.e); - label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[b2.w, o2.e]); + label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[b2.c, o2.c]); drawmsg(b2.w -- o2.e); - label.top(btex $\enc{N_2}{K_C}$ etex, alpha[a3.e, o3.w]); + label.top(btex $\enc{N_2}{K_C}$ etex, alpha[a3.c, o3.c]); drawmsg(a3.e -- o3.w); - label.top(btex $\enc{N_2}{K_B}$ etex, alpha[b3.w, o3.e]); + label.top(btex $\enc{N_2}{K_B}$ etex, alpha[b3.c, o3.c]); drawmsg(o3.e -- b3.w); endfig; @@ -186,17 +186,17 @@ endfor; % Messages and arrows - label.top(btex $\enc{N_1, A}{K_B}$ etex, alpha[a1.e, o1.w]); + label.top(btex $\enc{N_1, A}{K_B}$ etex, alpha[a1.c, o1.c]); drawmsg(a1.e -- o1.w); - label.top(btex $\enc{N_1, A}{K_B}$ etex, alpha[b1.w, o1.e]); + label.top(btex $\enc{N_1, A}{K_B}$ etex, alpha[b1.c, o1.c]); drawmsg(o1.e -- b1.w); - label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[a2.e, o2.w]); + label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[a2.c, o2.c]); drawmsg(o2.w -- a2.e); - label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[b2.w, o2.e]); + label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[b2.c, o2.c]); drawmsg(b2.w -- o2.e); label.top(btex $\enc{N_2}{K_B}$ etex, - alpha[a3.e, (xpart o2.w, ypart a3.c)]); - drawmsg(a3.e -- (beta * xpart o2.w, ypart a3.c)); + alpha[a3.c, (xpart o2.c, ypart a3.c)]); + drawmsg(a3.c -- (beta * xpart o2.c, ypart a3.c)); endfig; % Incompleteness example @@ -233,10 +233,72 @@ strand.b(2, .5w, delta, btex $\mathstrut\mathit{resp}$ etex, node); % Messages and arrows - label.top(btex $\enc{N}{K}$ etex, .5[a1.e, b1.w]); + label.top(btex $\enc{N}{K}$ etex, .5[a1.c, b1.c]); drawmsg(a1.e -- b1.w); - label.top(btex $N$ etex, .5[a2.e, b2.w]); + label.top(btex $N$ etex, .5[a2.c, b2.c]); drawmsg(b2.w -- a2.e); +endfig; + +beginfig(9); + % Strand for principal A + strand.a(3, origin, delta, btex $\mathstrut\mathit{init}$ etex, node); + + % Strand for principal B + strand.b(2, w + a2.c, delta, btex $\mathstrut\mathit{resp}$ etex, node); + + % Centered ordering symbols + boxit.o1(btex $\prec$ etex); o1.c = .5[a1.c, b1.c]; + boxit.o2(btex $\succ$ etex); o2.c = .5[a2.c, b2.c]; + + for i = 1 upto 2: + draw pic o[i]; + endfor; + + % Messages and arrows + label.top(btex $\enc{N_1, A}{K_B}$ etex, alpha[a1.c, o1.c]); + drawmsg(a1.e -- o1.w); + label.top(btex $\enc{N_1, A}{K_B}$ etex, alpha[b1.c, o1.c]); + drawmsg(o1.e -- b1.w); + label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[a2.c, o2.c]); + drawmsg(o2.w -- a2.e); + label.top(btex $\enc{N_1, N_2'}{K_A}$ etex, alpha[b2.c, o2.c]); + drawmsg(b2.w -- o2.e); + label.top(btex $\enc{N_2}{K_B}$ etex, + alpha[a3.c, (xpart o2.c, ypart a3.c)]); + drawmsg(a3.e -- (beta * xpart o2.w, ypart a3.c)); +endfig; + +beginfig(10); + % Strand for principal A + strand.a(3, origin, delta, btex $\mathstrut\mathit{resp}$ etex, node); + + % Strand for principal B + strand.b(3, w, delta, btex $\mathstrut\mathit{init}$ etex, node); + + % Centered ordering symbols + boxit.o2(btex $\prec$ etex); o2.c = .5[a2.c, b2.c]; + boxit.o3(btex $\succ$ etex); o3.c = .5[a3.c, b3.c]; + + for i = 2 upto 3: + draw pic o[i]; + endfor; + + % Messages and arrows + label.top(btex $\enc{N_1, A}{K_B}$ etex, + alpha[a1.c, (xpart o2.c, ypart a1.c)]); + drawmsg(a1.e -- (beta * xpart o2.w, ypart a1.c)); + label.top(btex $\enc{N_1, A}{K_{B'}}$ etex, + alpha[b1.c, (xpart o2.c, ypart b1.c)]); + drawmsg((1-beta)[(xpart o2.e, ypart b1.c), b1.w] -- b1.w); + label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[a2.c, o2.c]); + drawmsg(a2.e -- o2.w); + label.top(btex $\enc{N_1, N_2}{K_A}$ etex, alpha[b2.c, o2.c]); + drawmsg(o2.e -- b2.w); + label.top(btex $\enc{N_2}{K_B}$ etex, alpha[a3.c, o3.c]); + drawmsg(o3.w -- a3.e); + label.top(btex $\enc{N_2}{K_{B'}}$ etex, alpha[b3.c, o3.c]); + drawmsg(b3.w -- o3.e); + endfig; verbatimtex diff --git a/doc/cpsagoals.pdf b/doc/cpsagoals.pdf new file mode 100644 Binary files /dev/null and b/doc/cpsagoals.pdf differ diff --git a/doc/cpsagoals.tex b/doc/cpsagoals.tex new file mode 100644 --- /dev/null +++ b/doc/cpsagoals.tex @@ -0,0 +1,718 @@ +\documentclass[12pt]{article} +\usepackage{amssymb} +\usepackage{amsmath} +\usepackage{url} +\usepackage{graphicx} +\usepackage{alltt} +\input{macros} + +\newcommand{\sym}[1]{\textup{\texttt{#1}}} + +\title{CPSA and Formal Security Goals} +\author{John D.~Ramsdell\\ + The MITRE Corporation\\ CPSA Version \version} + +\begin{document} +\maketitle +\cpsacopying + +\tableofcontents + +\newpage + +\listoffigures + +\listoftables + +\newpage + +\section{Introduction} + +\begin{sloppypar} +Analyzing a cryptographic protocol means finding out what security +properties---essentially, authentication and secrecy properties---are +true in all its possible executions. +\end{sloppypar} + +Given a protocol definition and some assumptions about executions, +{\cpsa} attempts to produce descriptions of all possible executions of +the protocol compatible with the assumptions. Naturally, there are +infinitely many possible executions of a useful protocol, since +different participants can run it with varying parameters, and the +participants can run it repeatedly. + +However, for many naturally occurring protocols, there are only +finitely many of these runs that are essentially different. Indeed, +there are frequently very few, often just one or two, even in cases +where the protocol is flawed. We call these essentially different +executions the \emph{shapes} of the protocol. Authentication and +secrecy properties are easy to ``read off'' from the shapes, as are +attacks and anomalies, according to the introduction in the {\cpsa} +Primer~\cite{cpsaprimer09}. + +But how easy is it to read off authentication and secrecy properties? +What precisely is it that an expert sees? This paper describes +{\cpsa}'s support for reasoning about security goals using first-order +logic. With security goals expressed in first-order logic, intuition +is replaced by determining if a formula is true in all executions of +the protocol. + +% \emph{Something about the benefits of first-order logic goes here.} + +This treatment of security goals relies heavily on a branch of +first-order logic called model theory. It deals with the relationship +between descriptions in first-order languages and the structures that +satisfy these descriptions. In our case, the structures are skeletons +that denote a collection of executions of a protocol. This paper +attempts to describe the language of security goals and its +structures without requiring the reader to have studied model theory. + +The model theoretical foundation of this approach to security goals +appears in~\cite{Guttman14}. A practical use of security goals in +protocol standardization is described in~\cite{GuttmanLiskovRowe14}. +The precise semantics of the goal language is +in~\cite[Appendix~C]{cpsaspec09}. The syntax of security goals +appears in~\cite[Table~2]{cpsaprimer09}. + +The distribution in which this paper is included contains the sample +input {\cpsa} file \texttt{goals.scm}. It contains the examples in +this paper. You are encouraged to run the examples and examine the +output while reading this paper. + +%% Use a margin width of 62 for S-expressions + +\begin{figure} +\begin{center} +\includegraphics{cpsadiagrams-0.mps}\hfil +\includegraphics{cpsadiagrams-1.mps}\\ +\end{center} +\begin{center} +\begin{minipage}{3in} +\begin{verbatim} +(defprotocol ns basic + (defrole init + (vars (a b name) (n1 n2 text)) + (trace + (send (enc n1 a (pubk b))) + (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b))))) + (defrole resp + (vars (b a name) (n2 n1 text)) + (trace + (recv (enc n1 a (pubk b))) + (send (enc n1 n2 (pubk a))) + (recv (enc n2 (pubk b)))))) +\end{verbatim} +\end{minipage} +\end{center} +\caption{Needham-Schroeder Initiator and Responder Roles} +\label{fig:ns roles} +\end{figure} + +\begin{figure} +\begin{verbatim} +(defgoal ns ; Goal + (forall ((b name) (n1 text) (z0 node)) + (implies + (and (p "init" 2 z0) + (p "init" "n1" z0 n1) (p "init" "b" z0 b) + (non (privk b)) (uniq n1)) + (exists ((z1 node)) + (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))) + +(defskeleton ns ; Point of view skeleton + (vars (a b name) (n1 n2 text)) + (defstrand init 3 (a a) (b b) (n1 n1) (n2 n2)) + (non-orig (privk b)) + (uniq-orig n1)) +\end{verbatim} +\begin{center} +\includegraphics{cpsadiagrams-9.mps} +\end{center} +\begin{verbatim} +(defskeleton ns ; Shape + (vars (n1 n2 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a)) + (precedes ((0 0) (1 0)) ((1 1) (0 1))) + (non-orig (privk b)) + (uniq-orig n1) + (satisfied yes)) +\end{verbatim} +\caption{Needham-Schroeder Initiator Point of View} +\label{fig:ns init} +\end{figure} + +The {\cpsa} Primer~\cite{cpsaprimer09} is a prerequisite for reading +this paper. In particular, the Needham-Schroeder Protocol in +Section~10 is reanalyzed using security goals here. The roles are +displayed in Figure~\ref{fig:ns roles}. + +The protocol is analyzed from the point of view of a complete run of +one instance of the initiator role. The input security goal, followed +by the point of view skeleton it generates and the shape produced by +{\cpsa}, are shown in Figure~\ref{fig:ns init}. The syntax and +semantics of the goal will be explained later. Roughly speaking, it +asserts that if a realized skeleton contains a full length initiator +strand, its private key is uncompromised, and it uniquely generates +\texttt{n1}, then the skeleton will contain a responder strand that +agrees with the initiator on the name \texttt{b}. The shape produced +by {\cpsa} contains the annotation \texttt{(satisfies yes)}. This +indicates that its structure satisfies the description given by the +security goal. It will be explained later why the properties of +{\cpsa} allows us to conclude that this goal is true in all executions +of the protocol, and therefore conclude that the Needham-Schroeder +protocol achieves this authentication goal. + +\section{Syntax}\label{sec:syntax} + +To be precise, a security goal is an order-sorted first-order logic +sentence in a restricted form. The sentence in Figure~\ref{fig:ns + init} has the form shared by all security goals. It is a universally +quantified implication. The antecedent is a conjunction of atomic +formulas. For this sentence, the conclusion is an existentially +quantified conjunction of atomic formulas, but in general, the +conclusion is a disjunction of existentially quantified conjunctions +of atomic formulas. \sym{(false)} is a synonym for \sym{(or)}. + +\begin{center}\scshape + \begin{tabular}{rcl} + goal&$\leftarrow$&(\sym{defgoal} prot sent$+$ comments) + \\ sent&$\leftarrow$&(\sym{forall} (decl$\ast$) (\sym{implies} antec concl)) + \\ concl&$\leftarrow$&(\sym{false}) + $\mid$ existl $\mid$ (\sym{or} existl$\ast)$ + \\ existl&$\leftarrow$&(\sym{exists} + (decl$\ast$) antec) $\mid$ antec + \\ antec&$\leftarrow$&atomic $\mid$ (\sym{and} atomic$\ast$) + \end{tabular} +\end{center} + +Variables are declared as they are for roles and skeletons with one +exception, there is a new sort symbol \sym{node}. Notice that in the +sentence, variables \sym{z0} and \sym{z1} have sort \sym{node}. Every +universally quantified variable must occur in the antecedent of the +implication. + +The predicates used to construct an atomic formula (\textsc{atomic}) +are listed in Table~\ref{tab:predicates}. The first line gives the +syntax of a role position predicate. It contains three tokens, +\texttt{p}, a string that names a role, and an integer that specifies +a position within the trace of the role. That is, for role~$r$ with a +trace of length~$n$, there are~$n$ role position predicates, +\mbox{\texttt{p} $r$ $i$}, for $0\leq i < n$. The second line gives +the syntax of a role parameter predicate. It contains three tokens, +\texttt{p}, a string that names a role, and a string that names a role +variable. For role~$r$, there is role parameter predicate for each +variable declared by~$r$. + +The empty string names the listener role of a protocol. The role +has the variable \texttt{x} of sort \texttt{mesg} as its only role +variable. There are two positions in the listener role. + +When a variable of sort \sym{node} occurs in a formula, its position +must be specified using a role position formula. When an algebra +variable occurs in formula, its association with the parameter of some +role must be specified using a role parameter formula. + +\begin{table} +\begin{center} + \begin{tabular}{lcl} + Symbol & Sort & Description\\ + \hline + \scshape\sym{p} role pos & \dom{node} & \mbox{Role position} \\ + \scshape\sym{p} role param & $\dom{node}\times\dom{mesg}$ + & \mbox{Role parameter} \\ + \sym{str-prec}& $\dom{node}\times\dom{node}$ + & \mbox{Precedes on strand} \\ + \sym{prec}& $\dom{node}\times\dom{node}$ + & \mbox{Precedes} \\ + \sym{non}& \dom{atom} + & \mbox{Non-origination} \\ + \sym{pnon}& \dom{atom} + & \mbox{Penetrator non-origination} \\ + \sym{uniq}& \dom{atom} + & \mbox{Unique origination} \\ + \sym{uniq-at}& $\dom{atom}\times\dom{node}$ + & \mbox{Unique origination at node} \\ + $=$ & $\dom{all}\times\dom{all}$ & Equality + \end{tabular} +\end{center} +\caption{Predicates}\label{tab:predicates} +\end{table} + +\section{Semantics}\label{sec:semantics} + +In a \texttt{defgoal} sentence, the antecedent specifies the point of +view skeleton. We focus on the antecedent. In the example, + +\begin{quote} +\begin{verbatim} +(defstrand init 3 (a a) (b b) (n1 n1) (n2 n2)) +\end{verbatim} +\end{quote} +is extracted from +\begin{quote} +\begin{verbatim} +(and (p "init" 2 z0) + (p "init" "n1" z0 n1) (p "init" "b" z0 b)). +\end{verbatim} +\end{quote} +Notice that {\cpsa} adds a binding for \texttt{a} and \texttt{n2} just +as it does had +\begin{quote} +\begin{verbatim} +(defstrand init 3 (b b) (n1 n1)) +\end{verbatim} +\end{quote} +been given as input. + +Our aim now is to specify how to decide if a security goal is true in +all possible executions of a protocol. A skeleton defines a set of +executions that contain the skeleton's structure. We say a skeleton +\emph{satisfies} a formula if the formula is true in all executions +that contain the skeleton's structure. To decide if a skeleton +satisfies a formula, we decide if it satisfies each of its atomic +formulas, and combine the results using the rules of first-order +logic. + +Atomic formula \texttt{(p "init" 2 z0)} is called a role position +formula. A skeleton~$k$ satisfies the formula if \texttt{z0} maps to +a node $n=(s,2)$ in~$k$ such that +\begin{enumerate} +\item the trace of strand~$s$ in~$k$ has a length greater than 2, and +\item the trace when truncated to length 3 is an instance of the init + role. +\end{enumerate} +Consider the shape in Figure~\ref{fig:ns init}. It satisfies +\texttt{(p "init" 2 z0)} when \texttt{z0} maps to $(0,2)$. + +Atomic formula \texttt{(p "init" "n1" z0 n1)} is called a role +parameter formula. A skeleton~$k$ satisfies the formula if +\texttt{z0} maps to a node $n=(s,i)$ in~$k$ and \texttt{n1} maps to a +message algebra term~$t$ in~$k$ such that +\begin{enumerate} +\item the trace of strand~$s$ in~$k$ has a length greater than~$i$, +\item the trace truncated to length $i+1$ is an instance of the + init role, and +\item the truncated trace is compatible with mapping the init role's + \texttt{"n1"} role variable to~$t$. +\end{enumerate} +The shape in Figure~\ref{fig:ns init} satisfies \texttt{(p "init" "n1" + z0 n1)} when \texttt{z0} maps to $(0,2)$ and \texttt{n1} maps to the +message algebra term \texttt{n1}. + +Collectively, a skeleton satisfies the formula +\begin{quote} +\begin{verbatim} +(and (p "init" 2 z0) + (p "init" "a" z0 a) (p "init" "b" z0 b) + (p "init" "n1" z0 n1) (p "init" "n2" z0 n2)) +\end{verbatim} +\end{quote} +if the skeleton contains the structure specified by +\begin{quote} +\begin{verbatim} +(defstrand init 3 (a a) (b b) (n1 n1) (n2 n2)). +\end{verbatim} +\end{quote} + +The antecedent in Figure~\ref{fig:ns init} contains two origination +assertions. The formula \texttt{(non (privk b))} is extracted as +\texttt{(privk b)}. A skeleton~$k$ satisfies the formula if +\texttt{b} maps to a message algebra term~$t$ in~$k$ such that~$k$ +assumes that~$t$ is non-originating. The unique origination formula for +\texttt{n1} is similarly extracted. + +Putting it all together, the mapping +\[\{\mathtt{n1}\mapsto\mathtt{n1}, +\mathtt{n2}\mapsto\mathtt{n2}, \mathtt{a}\mapsto\mathtt{a}, +\mathtt{b}\mapsto\mathtt{b},\mbox{\tt z0}\mapsto(0,2)\}\] shows that +the shape in Figure~\ref{fig:ns init} satisfies the antecedent of the +security goal. + +The \texttt{prec} predicate is used to assert a node precedes another +node. The conclusion in Figure~\ref{fig:ns init} with \texttt{(prec + z1 z0)} added is satisfied by the shape using the mapping $\mbox{\tt + z0}\mapsto(0,2)$ and $\mbox{\tt z1}\mapsto(1,1)$. + +The \texttt{str-prec} predicate is used to assert a node precedes another +node and that both are on the same strand. + +The \texttt{uniq-at} predicate is used to assert not only that an atom +uniquely originates, but also the node at which it originates. It is +typically used in conjunction with a \texttt{str-prec} formula. In +the Figure~\ref{fig:ns init} goal, the \texttt{(uniq n1)} formula +could have been replaced by +\begin{quote} +\begin{verbatim} +(p "init" 0 z2) (str-prec z2 z0) (uniq-at n1 z2), +\end{verbatim} +\end{quote} +where \texttt{z2} has sort \texttt{node}. The extracted point of view +skeleton is the same. Of course, an error is raised if the role +position formula is replaced by \texttt{(p "init" 1 z2)}. + +Recall that our aim in analyzing a protocol is to find out what +security goals are true in all of its possible executions. We are +interested in runs of {\cpsa} that show that when every shape +satisfies a goal, it is true in every execution. + +When {\cpsa} performs a shape analysis, every shape it generates +refines the input skeleton. Skeleton refinement is defined +in~\cite[Section~6]{cpsaprimer09}, but roughly speaking, skeleton~$A$ +refines skeleton~$B$ if~$A$ contains the structure of skeleton~$B$. + +The skeleton~$k_0$ extracted from the antecedent of a security goal +has the property that every skeleton than refines~$k_0$ satisfies the +antecedent. A skeleton with this property is called the +\emph{characteristic skeleton} of the antecedent. + +Given a goal~\(\Phi\), consider a shape analysis starting from the +characteristic skeleton~$k_0$ of its antecedent. Assume {\cpsa} finds +shapes $k_1,\ldots,k_n$ and that {\cpsa} determines that each~$k_i$ +satisfies~$\Phi$. Consider the executions that contain the structure +in~$k_0$. {\cpsa} tells us that each execution is in the executions +that contain the structure of some~$k_i$. Furthermore, because~$k_0$ +is a characteristic skeleton, each~$k_i$ satisfies the antecedent +of~$\Phi$. Therefore,~$\Phi$ is true in all executions of the +protocol and maximally informative. + +\section{Examples}\label{sec:examples} + +This section contains examples of both authentication and secrecy +goals. The first example shows the feedback the user receives when a +shape does not satisfy a security goal. The second example shows how +to use a listener to state a secrecy goal. + +\subsection{Needham-Schroeder Responder}\label{sec:ns resp} + +\begin{figure} +\begin{verbatim} +(defgoal ns ; Goal + (forall ((a b name) (n2 text) (z0 node)) + (implies + (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) + (p "resp" "a" z0 a) (p "resp" "b" z0 b) + (non (privk a)) (uniq n2)) + (exists ((z1 node)) + (and (p "init" 1 z1) (p "init" "b" z1 b))))) + +(defskeleton ns ; Point of view skeleton + (vars (a b name) (n1 n2 text)) + (defstrand init 3 (a a) (b b) (n1 n1) (n2 n2)) + (non-orig (privk a)) + (uniq-orig n2)) +\end{verbatim} +\begin{center} +\includegraphics{cpsadiagrams-10.mps} +\end{center} +\begin{verbatim} +(defskeleton ns ; Shape + (vars (n1 n2 text) (a b b-0 name)) + (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0)) + (precedes ((0 1) (1 1)) ((1 2) (0 2))) + (non-orig (privk a)) + (uniq-orig n2) + (satisfies (no (a a) (b b) (n2 n2) (z0 (0 2)))) +\end{verbatim} +\caption{Needham-Schroeder Responder Point of View} +\label{fig:ns resp} +\end{figure} + +Figure~\ref{fig:ns resp} contains an analysis of Needham-Schroeder +from the point of view of a complete run of the responder under the +assumption that the responder's private key is uncompromised and the +nonce it generates uniquely originates. + +The conclusion of the goal asserts that in an execution compatible +with the point of view, there must be an initiator strand that agrees +with the responder strand on the name \texttt{b}. The shape produced +by {\cpsa} is a counterexample to this assertion. Because of this, +{\cpsa} annotates the shape with +\begin{quote} +\begin{verbatim} +(satisfies (no (a a) (b b) (n2 n2) (z0 (0 2))). +\end{verbatim} +\end{quote} +The annotation includes a variable mapping for the shape that +satisfies the antecedent of the goal but does not satisfy its +conclusion. The mapping \texttt{(b b)} is the reason the shape does +not satisfy the goal. + +Galvin Lowe identified this authentication failure in +Needham-Schroeder and provided a fix. In the Needham-Schroeder-Lowe +Protocol, the name \texttt{b} is included within the encryption in second +message of both roles. With this modification, the shape found by +{\cpsa} satisfies the security goal in Figure~\ref{fig:ns resp}, so +Needham-Schroeder-Lowe achieves this authentication goal. + +\subsection{A Needham-Schroeder Secrecy Goal}\label{sec:secrecy goal} + +\begin{figure} +\begin{quote} +\begin{verbatim} +(defgoal ns + (forall ((a b name) (n1 text) (z0 z1 node)) + (implies + (and (p "init" 2 z0) (p "init" "n1" z0 n1) + (p "init" "a" z0 a) (p "init" "b" z0 b) + (p "" 0 z1) (p "" "x" z1 n1) ; Listener + (non (privk a)) (non (privk b)) (uniq n1)) + (false)))) +\end{verbatim} +\end{quote} +\caption{Needham-Schroeder Secrecy Goal}\label{fig:ns secrecy} +\end{figure} + +Figure~\ref{fig:ns secrecy} contains an analysis of Needham-Schroeder +from the point of view of a complete run of the initiator under the +assumption that the responder's and its peer's private key are +uncompromised and the nonce~\texttt{n1} it generates uniquely +originates. Futhermore, the point of view asserts that the nonce is +leaked using a listener. +\begin{quote} +\begin{verbatim} +(p "" 0 z1) (p "" "x" z1 n1) ; Listener +\end{verbatim} +\end{quote} + +{\cpsa} finds no shapes, so Needham-Schroeder achieves this secrecy +goal and does not leak~\texttt{n1}. + +\subsection{Unilateral Authentication}\label{sec:unilateral} + +This example focuses on unilateral authentication. To best visualize +this example, process the sample file \texttt{goal.scm} with {\cpsa} +and display its output in a browser. + +The protocol and its goal is shown in Figure~\ref{fig:unilateral}. +The goal asserts that if a realized skeleton contains a full length +initiator strand that uniquely generates \texttt{n1}, and +peer~\texttt{a}'s private key is uncompromised, then the skeleton will +contain a responder strand that agrees with the initiator on the +name~\texttt{a}. When given as input, {\cpsa} verifies that the goal +is true in all executions of the protocol. + +\begin{figure} +\begin{minipage}{2.7in} +\begin{verbatim} +(defprotocol unilateral basic + (defrole init + (vars (a name) (n text)) + (trace + (send (enc n (pubk a))) + (recv n))) + (defrole resp + (vars (a name) (n text)) + (trace + (recv (enc n (pubk a))) + (send n)))) +\end{verbatim} +\end{minipage}\hfil +\begin{minipage}{3.0in} +\begin{verbatim} +(defgoal unilateral + (forall ((a name) (n text) + (z0 node)) + (implies + (and (p "init" 1 z0) + (p "init" "n" z0 n) + (p "init" "a" z0 a) + (non (privk a)) (uniq n)) + (exists ((z1 node)) + (and (p "resp" 1 z1) + (p "resp" "a" z1 a)))))) +\end{verbatim} +\end{minipage} +\caption{Unilateral Protocol and Authentication Goal}\label{fig:unilateral} +\end{figure} + +\begin{figure} +\begin{quote} +\begin{verbatim} +(defgoal ns + (forall ((a name) (n text) (z0 node)) + (implies + (and (p "init" 1 z0) (p "init" "n1" z0 n) + (p "init" "b" z0 a) (non (privk a)) (uniq n)) + (exists ((z1 node)) + (and (p "resp" 1 z1) (p "resp" "b" z1 a)))))) +\end{verbatim} +\end{quote} +\caption{Translated Unilateral Goal for the + Initiator}\label{fig:unilateral ns init} +\end{figure} + +\begin{figure} +\begin{quote} +\begin{verbatim} +(defgoal ns + (forall ((a name) (n text) (z0 node)) + (implies + (and (p "resp" 2 z0) (p "resp" "n2" z0 n) + (p "resp" "a" z0 a) (non (privk a)) (uniq n)) + (exists ((z1 node)) + (and (p "init" 2 z1) (p "init" "a" z1 a))))) +\end{verbatim} +\end{quote} +\caption{Translated Unilateral Goal for the + Responder}\label{fig:unilateral ns resp} +\end{figure} + +In Section~\ref{sec:ns resp}, a goal written for the Needham-Schroeder +Protocol was reused to analyze the Needham-Schroeder-Lowe Protocol. +We now use the unilateral authentication goal to analyze +Needham-Schroeder. + +Consider the goal in Figure~\ref{fig:unilateral ns init}. This goal +is the result of translating the Unilateral role position and +parameter predicates as follows. +\begin{center} +\begin{tabular}{l@{$\quad\rightarrow\quad$}l} + \texttt{p "init" "n"}&\texttt{p "init" "n1"}\\ + \texttt{p "init" "a"}&\texttt{p "init" "b"}\\ + \texttt{p "resp" "a"}&\texttt{p "resp" "b"} +\end{tabular} +\end{center} +When given Figure~\ref{fig:unilateral ns init} as input, {\cpsa} +verifies that the goal is true in all executions of the protocol. + +There is another way to translate the Unilateral goal. +\begin{center} +\begin{tabular}{l@{$\quad\rightarrow\quad$}l} + \texttt{p "init" 1}&\texttt{p "resp" "2"}\\ + \texttt{p "init" "n"}&\texttt{p "resp" "n2"}\\ + \texttt{p "init" "a"}&\texttt{p "resp" "a"}\\ + \texttt{p "resp" "1"}&\texttt{p "init" "2"}\\ + \texttt{p "resp" "a"}&\texttt{p "init" "a"} +\end{tabular} +\end{center} +When given Figure~\ref{fig:unilateral ns resp} as input, {\cpsa} +verifies that the goal is true in all executions of the protocol. + +{\cpsa} has demonstrated two ways in which Needham-Schroeder achieves +the goals of the Unilateral Protocol. + +\section{The Whole Story}\label{sec:whole story} + +The examples in the previous section demonstrate the typical way +security goals are analyzed with {\cpsa}. However, there are more +features that may be useful. + +A \texttt{defgoal} form may contain more than one sentence. See +Figure~\ref{fig:ns init goals} for an example. When presented with +more than one sentence, {\cpsa} extracts the point of view skeleton +from the first sentence. + +It is wise to ensure that the antecedent in every sentence is +identical. When {\cpsa} performs satisfaction-checking on +sentence~$\Phi$, it only determines if each shape it finds is +satisfied. If the point of view skeleton in not the characteristic +skeleton of the antecedent of~$\Phi$, the fact that all skeletons +satisfy~$\Phi$ cannot be used to conclude that~$\Phi$ is true in all +executions of the protocol. + +\begin{figure} +\begin{quote} +\begin{verbatim} +(defgoal ns + (forall ((a b name) (n text) (z0 node)) + (implies + (and (p "init" 1 z0) (p "init" "n1" z0 n) + (p "init" "a" z0 a) (p "init" "b" z0 b) + (non (privk a)) (non (privk b)) (uniq n)) + (exists ((z1 node)) + (and (p "resp" 1 z1) (p "resp" "b" z1 b))))) + (forall ((a b name) (n text) (z0 node)) + (implies + (and (p "init" 1 z0) (p "init" "n1" z0 n) + (p "init" "a" z0 a) (p "init" "b" z0 b) + (non (privk a)) (non (privk b)) (uniq n)) + (exists ((z1 node)) + (and (p "resp" 1 z1) (p "resp" "a" z1 a)))))) +\end{verbatim} +\end{quote} +\caption{Two Initiator Authentication Goals}\label{fig:ns init goals} +\end{figure} + +{\cpsa} performs satisfaction-checking when an input skeleton in annotated +with one or more security goals. The annotation uses the +\texttt{goals} key. + +\begin{quote} + \begin{alltt} +(defskeleton + \ldots + (goals \textsc{sent\ensuremath{+}})) + \end{alltt} +\end{quote} + +The program \texttt{cpsasas}, discussed in the next section, can be +used to generate an formula with an antecedent such that the input +skeleton is the characteristic skeleton of the antecedent. + +\subsection{Shape Analysis Sentences}\label{sec:sas} + +A shape analysis sentence expresses all that can be learned from a run +of {\cpsa} as a security goal. If a security goal can be derived from +a shape analysis sentence, then the protocol achieves the security +goal, that is, the goal is true in all executions of the protocol. + +The program \texttt{cpsasas} extracts shape analysis sentences from +the output of {\cpsa}. Consider the first example in this paper +(Figure~\ref{fig:ns init}), which is in the sample file +\texttt{goals.scm}. To generate a maximally informative security goal +from the initiator point of view with \texttt{ghci} and +\texttt{Make.hs}, type +\begin{quote} +\begin{verbatim} +$ ghci Make.hs +*Make> sas "goals" +\end{verbatim} +\end{quote} +When using GNU make, type ``\texttt{make goals\_sas.text}''. The +resulting shape analysis sentence is displayed in Figure~\ref{fig:ns + sas}. + +\begin{figure} +\begin{verbatim} +(defgoal ns + (forall ((n1 n2 text) (b a name) (z z-0 node)) + (implies + (and (p "init" 0 z) (p "init" 2 z-0) + (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2) + (p "init" "a" z-0 a) (p "init" "b" z-0 b) + (str-prec z z-0) (non (privk b)) (uniq-at n1 z)) + (exists ((n2-0 text) (z-1 z-2 z-3 node)) + (and (p "init" 1 z-1) (p "resp" 0 z-2) + (p "resp" 1 z-3) (p "resp" "n2" z-3 n2-0) + (p "resp" "n1" z-3 n1) (p "resp" "b" z-3 b) + (p "resp" "a" z-3 a) (prec z z-2) (prec z-3 z-1) + (str-prec z z-1) (str-prec z-1 z-0) + (str-prec z-2 z-3)))))) +\end{verbatim} +\caption{Initiator Shape Analysis Sentence}\label{fig:ns sas} +\end{figure} + +A shape analysis sentences asserts that either a realized skeleton +does not satisfy its antecedent or it satisfies one or more of the +disjuncts in its conclusion. {\cpsa} has been designed so that this +assertion is true. Therefore, every shape analysis sentence is true +in all executions. + +A security goal is true in all executions if it can be derived from a +shape analysis sentence~\cite{Ramsdell12}. {\cpsa} comes with a +Prolog program that translates shape analysis sentences into Prover9 +syntax~\cite{prover9}. Prover9 can then be used to perform the +required theorem-proving. + +In practice, theorem-proving using shape analysis sentences is rarely +employed. It's clumsy and it requires too much expertise. The main +use of \texttt{cpsasas} is for generating a formula that is edited to +become a desired security goal. + +\bibliography{cpsa} +\bibliographystyle{plain} + +\end{document} diff --git a/doc/cpsaintroslides.pdf b/doc/cpsaintroslides.pdf Binary files a/doc/cpsaintroslides.pdf and b/doc/cpsaintroslides.pdf differ 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 @@ -1098,6 +1098,22 @@ (comment "Nothing left to do") \end{verbatim} +\section{First-Order Logic and Security Goals}\label{sec:security goals} + +Another way to specify a problem statement is with a security goal. A +security goal a sentence in first-order logic. It asserts that if +some properties hold for a skeleton, then some other properties must +hold for all shapes computed by CPSA starting with the skeleton. +Security goals can be used to formally state authentication and +secrecy goals of a protocol. + +The \texttt{defgoal} form is used to pose an analysis problem with a +sentence instead of a skeleton. CPSA extracts a point of view +skeleton from the antecedent of the formula and then analyzes it. +When it prints a shape, it checks to see if the shape satisfies the +conclusion of the security goal. See~\cite{cpsagoals09} for details. +The grammar of security goals is in Table~\ref{tab:goal}. + \section{Macros}\label{sec:macros} After reading the input, {\cpsa} expands macros before in analyzing 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 @@ -2114,10 +2114,10 @@ each role~$\role_Y(C,N,U)\in P$ and variable~$x:S$ that occurs in~$C$, there is a protocol specific binary parameter predicate $P[r,x]:\dom{node}\times{}S$. The protocol independent unary -predicates are $\mathsf{non}: B$ for each base sort~$B$. The -remaining protocol independent predicates are binary, and are -$\mathsf{uniq}: B\times\dom{node}$, -$\mathsf{sprec}:\dom{node}\times\dom{node}$, +predicates are $\mathsf{non}: B$ and $\mathsf{uniq}: B$ for each base +sort~$B$. The remaining protocol independent predicates are binary, +and are $\mathsf{\uniqat}: B\times\dom{node}$, +$\mathsf{\strprec}:\dom{node}\times\dom{node}$, $\mathsf{prec}:\dom{node}\times\dom{node}$, and equality. Soon we define~$\form(k)=(Y,\Phi)$, where~$\Phi$ is $k$'s skeleton @@ -2158,12 +2158,14 @@ $P[r,x](v(s,h-1),t)$, where $r^c=C$ when $r=\role(C,N,U)$. \item For each $(s,i),(s,i')\in N$ such that $i - CPSA 2.4 User Guide + CPSA 2.5 User Guide