diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,22 @@ +2014-01-07 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as version 2.3.2 + +2013-12-27 John D. Ramsdell + + * src/prover9.pl: Reverted to work with strings as tags fixing a + bug introduced in version 2.3.1. + +2013-12-14 John D. Ramsdell + + * cpsa.cabal (Extra-Source-Files): Sorted the files. + +2013-10-15 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as version 2.3.1 + + * src/unsorted.pl: Added a missing occurs check and substitution. + 2013-10-11 John D. Ramsdell * src/CPSA/Lib/Cohort.hs (prioritizeVertices): Reversed the sort diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,5 +1,11 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.3.2 + +** Bug fixed in prover9 + A bug was introduced in 2.3.1 that caused it to fail when the input + contains a tag. + * Changes in version 2.3.1 ** Bug in priority ordering fixed. diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 2.3.1 +Version: 2.3.2 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3 @@ -64,18 +64,25 @@ src/cpsaextras/Main.scala src/cpsaextras/Pretty.scala src/cpsaextras/Printer.scala src/cpsaextras/SExpr.scala tst/README tst/Makefile tst/Make.hs tst/checktst tst/cpsagraphall - tst/cpsashapesall tst/blanchet.scm tst/blanchet.tst - tst/completeness-test.scm tst/completeness-test.tst tst/crushing.tst - tst/crushing.tst tst/dass.lisp tst/dass-mod.lisp tst/dass_simple.scm + tst/cpsashapesall + tst/blanchet.scm tst/blanchet.tst tst/completeness-test.scm + tst/completeness-test.tst tst/crushing.tst tst/crushing.tst + tst/dass.lisp tst/dass-mod.lisp tst/dass_simple.scm tst/dass_simple.tst tst/denning-sacco.scm tst/denning-sacco.tst - tst/deorig_contract.scm tst/deorig_contract.tst - tst/deorig_simple.scm tst/deorig_simple.tst - tst/ds-short.lisp tst/deorig_mesg.scm tst/deorig_mesg.tst tst/dy.lsp - tst/dy.tst tst/encsig.scm tst/encsig.tst tst/epmo_acctnum.lisp - tst/epmo.scm tst/epmo.tst tst/ffgg.scm - tst/ffgg.tst tst/fragile_pruning.scm tst/fragile_pruning.tst + tst/deorig_contract.scm tst/deorig_contract.tst tst/deorig_mesg.scm + tst/deorig_mesg.tst tst/deorig_simple.scm tst/deorig_simple.tst + tst/DH_hack.scm tst/DH_hack.tst tst/ds-short.lisp tst/dy.lsp + tst/dy.tst tst/encsig.scm tst/encsig.tst + tst/epmo_acctnum-key-hash.scm tst/epmo_acctnum-key-hash.tst + 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 @@ -84,31 +91,25 @@ tst/nonaug-prune.tst tst/non_transforming.scm tst/non_transforming.tst tst/nsl3.scm tst/nsl3.tst tst/nsl4cm1.lsp tst/nsl4cm1.tst tst/nsl4.lisp tst/nsl4resp2.lisp tst/nsl5i.lisp - tst/nsl5.lisp tst/nslsk.scm tst/nslsk.tst tst/ns.scm tst/ns.tst - tst/or.scm tst/or.tst tst/pca.scm tst/pca.tst tst/pruning1.scm - tst/pruning1.tst tst/sigenc.scm tst/sigenc.tst - tst/sorted_epmo_acctnum.scm tst/sorted_epmo_acctnum.tst - tst/targetterms2.scm tst/targetterms2.tst tst/targetterms6.scm - tst/targetterms6.tst tst/targetterms8.scm tst/targetterms8.tst - tst/tnsl5.lisp tst/uncarried_keys.scm tst/uncarried_keys.tst - tst/uo.scm tst/uo.tst tst/updatetst tst/weird.scm tst/weird.tst - tst/wide-mouth-frog.lsp tst/wide-mouth-frog.tst - tst/wide-mouth-frog-scyther.lsp tst/wide-mouth-frog-scyther.tst + tst/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 + tst/sigenc.tst tst/sorted_epmo_acctnum.scm + tst/sorted_epmo_acctnum.tst tst/targetterms2.scm + tst/targetterms2.tst tst/targetterms6.scm tst/targetterms6.tst + tst/targetterms8.scm tst/targetterms8.tst tst/timestamping.scm + tst/timestamping.tst tst/tnsl5.lisp tst/uncarried_keys.scm + tst/uncarried_keys.tst tst/uo.scm tst/uo.tst tst/updatetst + tst/wang-hash.scm tst/wang-hash.tst tst/wang-key-hash.scm + tst/wang-key-hash.tst tst/wang.lisp tst/weird.scm tst/weird.tst + tst/wide-mouth-frog.lsp tst/wide-mouth-frog-scyther.lsp + tst/wide-mouth-frog-scyther.tst tst/wide-mouth-frog.tst tst/wonthull2.scm tst/wonthull2.tst tst/wonthull3.scm tst/wonthull3.tst tst/wonthull.scm tst/wonthull.tst tst/woolam.scm tst/woolam.tst tst/yahalom-6.3.6.scm tst/yahalom-6.3.6.tst - tst/yahalom.scm tst/yahalom.tst tst/epmo_acctnum-key-hash.scm - tst/epmo_acctnum-key-hash.tst tst/epmo-key-hash.scm - tst/epmo-key-hash.tst tst/wang.lisp tst/pkinit.scm tst/pkinit.tst - tst/print.scm tst/print.tst tst/epmo-hash.scm tst/epmo-hash.tst - tst/hashtest-key-hash.scm tst/hashtest-key-hash.tst tst/hashtest.scm - tst/hashtest.tst tst/wang-key-hash.scm tst/wang-key-hash.tst - tst/wang-hash.scm tst/wang-hash.tst tst/mass.lsp tst/mass.tst - tst/mass2.lsp tst/mass2.tst tst/DH_hack.scm tst/DH_hack.tst - tst/timestamping.scm tst/timestamping.tst tst/ns-l.scm tst/ns-l.tst - tst/pen-non-orig-test.scm tst/pen-non-orig-test.tst - tst/preprocess.scm tst/preprocess.tst tst/incompleteness_example.scm - tst/incompleteness_example.tst + tst/yahalom.scm tst/yahalom.tst -- Algebra implementations must import CPSA.Lib.CPSA. -- Tools may additionally import CPSA.Lib.Entry. 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/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/cpsaspec.pdf b/doc/cpsaspec.pdf Binary files a/doc/cpsaspec.pdf and b/doc/cpsaspec.pdf differ 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.3.1} +\newcommand{\version}{2.3.2} \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/DiffieHellman/Algebra.hs b/src/CPSA/DiffieHellman/Algebra.hs --- a/src/CPSA/DiffieHellman/Algebra.hs +++ b/src/CPSA/DiffieHellman/Algebra.hs @@ -869,7 +869,9 @@ idSubst subst (F Exp [t0, G t1]) = case idSubst subst t0 of -- (exp (exp g x) y) = (exp g (mul x y)) F Exp [t0', G t1'] -> - idSubst subst (F Exp [t0', G $ mul t1' t1]) + case mul t1' $ groupSubst subst t1 of + t2 | M.null t2 -> t0' + | otherwise -> F Exp [t0', G t2] t -> expSubst subst t t1 idSubst subst (F s u) = F s (map (idSubst subst) u) @@ -1087,7 +1089,9 @@ F Exp [t0, G t1] -> case substChase subst t0 of F Exp [t0', G t1'] -> - substChase subst (F Exp [t0', G $ mul t1' t1]) + case mul t1' $ groupChase subst t1 of + t2 | M.null t2 -> t0' + | otherwise -> F Exp [t0', G t2] t -> expChase subst t t1 F s u -> F s (map (substChase subst) u) diff --git a/src/prover9.pl b/src/prover9.pl --- a/src/prover9.pl +++ b/src/prover9.pl @@ -203,11 +203,16 @@ load_term(Term, Internal), term_pp(Internal, Pretty). -%% Load a term using CPSA's parsing rules for terms. +%% Load a term using CPSA's parsing rules for terms. Also, convert +%% variables into uppercase atoms, and constants into lowercase atoms. load_term(Term, Internal) :- atom(Term), - load_atom(Term, Internal). + upcase_symbol(Term, Internal). +load_term(Term, Internal) :- + string(Term), + string_to_atom(Term, Atom), + downcase_symbol(Atom, Internal). load_term(Term, Term) :- integer(Term), Term >= 0. @@ -228,33 +233,28 @@ atom(Term), load_terms(Terms, Internals). -%% Convert variables into uppercase atoms, and constants into -%% lowercase atoms. +upcase_symbol(Atom, Symbol) :- + atom_chars(Atom, Chars), + upcase_parts(Chars, Parts), + atom_chars(Symbol, Parts). -load_atom('""', []) :- % The name for a listener is the null constant. - !. -load_atom(Atom, Symbol) :- - atom_chars(Atom, Chars), - parts(Chars, Parts), +upcase_parts([First|Rest], [Lead|Tail]) :- + upcase_atom(First, Lead), + symbol_parts(Rest, Tail). + +downcase_symbol(Atom, Symbol) :- + atom_chars(Atom, Chars), + downcase_parts(Chars, Parts), atom_chars(Symbol, Parts). -parts(['"'|Chars], Parts) :- - !, - downcase_parts(Chars, Parts). -parts(Chars, Parts) :- - upcase_parts(Chars, Parts). +%% The null constant is used for the name of the listener role. +downcase_parts([], ['[', ']']). downcase_parts([First|Rest], [Lead|Tail]) :- downcase_atom(First, Lead), symbol_parts(Rest, Tail). -upcase_parts([First|Rest], [Lead|Tail]) :- - upcase_atom(First, Lead), - symbol_parts(Rest, Tail). - symbol_parts([], []). -symbol_parts(['"'], []) :- - !. symbol_parts(['-'|Rest], ['_'|Tail]) :- !, symbol_parts(Rest, Tail). diff --git a/src/unsorted.pl b/src/unsorted.pl --- a/src/unsorted.pl +++ b/src/unsorted.pl @@ -8,7 +8,8 @@ %% modify it under the terms of the BSD License as published by the %% University of California. -:- module(unsorted, [to_unsorted/3, from_unsorted/3, unify/3, unify/4]). +:- module(unsorted, [to_unsorted/3, from_unsorted/3, + unify/3, unify/4, subst/3]). :- use_module(cpsa). @@ -165,9 +166,21 @@ lookup(Key, Map, Result), !, Result = Value. % Fails when key is mapped to another value -% Extend Map when Key is not mapped -extend_map(Key, Value, Map, [(Key, Value)|Map]). +% Extend Map when Key is not mapped as long as var does occur in term +extend_map(Key, Value, Map, [(Key, Value)|Map]) :- + \+occurs(Key, Value). +occurs(Var, Var). +occurs(Var, Term) :- + Term =.. [_|Terms], + occurs_list(Var, Terms). + +occurs_list(Var, [Term|_]) :- + occurs(Var, Term), + !. +occurs_list(Var, [_|Terms]) :- + occurs_list(Var, Terms). + %% Unification of unsorted terms given the equation invk(invk(k)) = k. %% unify(+Term0, +Term1, -Subst). @@ -250,3 +263,31 @@ unify_list([Term0|Terms0], [Term1|Terms1], InSubst, OutSubst) :- unify(Term0, Term1, InSubst, Subst), unify_list(Terms0, Terms1, Subst, OutSubst). + +%% Substition + +%% subst(+InTerm, +Subst, -OutTerm). + +subst(InTerm, Subst, OutTerm) :- + chase(InTerm, Subst, Term), + subst_aux(Term, Subst, OutTerm). + +subst_aux(Term, _, Term) :- + atom(Term), + !. +subst_aux(Term, _, Term) :- + string(Term), + !. +% Apply equation +subst_aux(invk(InTerm), Subst, OutTerm) :- + subst(InTerm, Subst, invk(OutTerm)), + !. +subst_aux(InTerm, Subst, OutTerm) :- + InTerm =.. [Fun|InTerms], + subst_list(InTerms, Subst, OutTerms), + OutTerm =.. [Fun|OutTerms]. + +subst_list([], _, []). +subst_list([InTerm|InTerms], Subst, [OutTerm|OutTerms]) :- + subst(InTerm, Subst, OutTerm), + subst_list(InTerms, Subst, OutTerms).