cpsa-3.5.1: cpsa.cabal
Name: cpsa
Version: 3.5.1
Maintainer: mliskov@mitre.org
Cabal-Version: >= 1.6
License: BSD3
License-File: license.txt
Synopsis: Symbolic cryptographic protocol analyzer
Description:
The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to
enumerate all essentially different executions possibe for a
cryptographic protocol. We call them the shapes of the protocol.
Naturally occurring protocols have only finitely many, indeed very
few shapes. Authentication and secrecy properties are easy to
determine from them, as are attacks and anomalies.
.
For each input problem, the CPSA program is given some initial
behavior, and it discovers what shapes are compatible with
it. Normally, the initial behavior is from the point of view of one
participant. The analysis reveals what the other participants must
have done, given the participant's view. The search is based on a
high-level algorithm that was claimed to be complete, i.e. every
shape can in fact be found in a finite number of steps. Further
theoretical work showed classes of executions that are not found by
the algorithm, however it also showed that every omitted execution
requires an unnatural interpretation of a protocol's roles. Hence
the algorithm is complete relative to natural role semantics.
.
The package contains a set of programs used to perform and display
the analysis. A standards complient browser, such as Firefox,
Safari, or Chrome, is required to display the results. Program
documentation is in the doc directory in the source distribution,
and installed in the package's data directory. You can locate the
package's data directory by typing "cpsa --help" to a command
prompt. New users should start learning to use the tool from the
manual, found at "cpsamanual.pdf" in the data directory. Examples
referenced in the manual can be found in the data directory as well.
It is suggested that users make an examples directory and copy
"*.scm *.xhtml" to their local examples directory, both so that
they may be modified and for ease of access.
.
Serious Windows users should install MSYS so as to allow the use of
make and script execution.
.
The theory and algorithm used by CPSA was developed with the help of
Joshua D. Guttman, John D. Ramsdell, Jon C. Herzog, Shaddin
F. Doghmi, F. Javier Thayer, Paul D. Rowe, and Moses D. Liskov.
John D. Ramsdell and Moses D. Liskov implemented the algorithm in
Haskell. CPSA was designed and implemented at The MITRE Corporation.
Category: Cryptography
Build-Type: Simple
Data-Files:
Make.hs cpsa.mk cpsamanual.pdf examples/blanchet.scm
examples/blanchet.xhtml examples/bltk_or.scm examples/bltk_or.xhtml
examples/envelope.scm examples/envelope.xhtml examples/ffgg.scm
examples/ffgg.xhtml examples/fnof_test.scm examples/fnof_test.xhtml
examples/fnof_yahalom.scm examples/fnof_yahalom.xhtml
examples/goals.scm examples/goals.xhtml examples/kerb.scm
examples/kerb.xhtml examples/lt_test.scm examples/lt_test.xhtml
examples/neq_test.scm examples/neq_test.xhtml examples/ns.scm
examples/ns.xhtml examples/or.scm examples/or.xhtml
examples/pkinit.scm examples/pkinit.xhtml examples/plaindh.scm
examples/plaindh.xhtml examples/priority_test.scm
examples/priority_test.xhtml examples/station.scm
examples/station.xhtml examples/subsort_test.scm examples/woolam.scm
examples/yahalom.scm examples/yahalom.xhtml
examples/IKE_variants.tar.gz examples/IKE_variants_nobase.tar.gz
examples/iadh_um.scm examples/iadh_um.xhtml
examples/subsort_test.xhtml examples/woolam.xhtml
examples/dh_mim.scm examples/dh_mim.xhtml
examples/fluffy_draft03_fixing_gske.scm
examples/fluffy_draft03_gske.scm
examples/fluffy_draft03_improving_pske.scm
examples/fluffy_draft03_pske.scm examples/eq_test.scm
examples/eq_test.xhtml
Data-Dir: doc
Extra-Source-Files:
Makefile ChangeLog README.txt NEWS ghci cpsatst setup.bat
src/cpsa.el src/cpsaops.scm src/cpsa.pl src/pp.pl
src/sexpr.pl src/ghcmemlimit src/cpsajson.py src/split.py
tst/checktst tst/updatetst tst/graphtst
tst/Makefile tst/Make.hs tst/README
tst/axiom2.scm tst/axiom2.tst tst/blanchet.scm tst/blanchet.tst
tst/bltk_example.lisp tst/bltk_example.tst tst/bltk_test.scm
tst/bltk_test.tst tst/dh-ca.scm tst/dh-ca.tst tst/dh_mim2.scm
tst/dh_mim2.tst tst/dh_mim.scm tst/dh_mim.tst tst/dhnsl_basic.scm
tst/dhnsl_basic.tst tst/dhnsl.lisp tst/dhnsl.tst tst/dhnsl_use.scm
tst/dhnsl_use.tst tst/dh_sig.scm tst/dh_sig.tst tst/dh_test.scm
tst/dh_test.tst tst/enrich.scm tst/enrich.tst tst/envelope.scm
tst/envelope.tst tst/ffgg.scm tst/ffgg.tst tst/fnof_or.scm
tst/fnof_or.tst tst/fnof_test.scm tst/fnof_test.tst
tst/fnof_woolam.scm tst/fnof_woolam.tst tst/fnof_yahalom.scm
tst/fnof_yahalom.tst tst/goals.scm tst/goals.tst tst/iadh_um.scm
tst/iadh_um.tst tst/injection.scm tst/injection.tst
tst/kerberos++.scm tst/kerberos++.tst tst/lt_test.scm
tst/lt_test.tst tst/neq_test.scm
tst/neq_test.tst tst/ns.scm tst/ns.tst tst/or.scm tst/or.tst
tst/owang.scm tst/owang.tst tst/owat.scm tst/owat.tst tst/pkinit.scm
tst/pkinit.tst tst/plaindh.scm tst/plaindh.tst tst/priority_test.scm
tst/priority_test.tst tst/staticdh.scm tst/staticdh.tst
tst/station2.scm tst/station2.tst
tst/subsort_test.scm tst/subsort_test.tst
tst/test_small.scm tst/test_small.tst tst/unilateral.scm
tst/unilateral.tst tst/uniq-gen-test.scm tst/uniq-gen-test.tst
tst/wang.tst tst/woolam.scm tst/woolam.tst tst/wrap_decrypt.lsp
tst/wrap_decrypt.tst tst/yahalom.scm tst/yahalom.tst
tst/aik.scm tst/aik.tst tst/reflect.scm tst/reflect.tst
tst/station.scm tst/station.tst tst/kerb.scm tst/kerb.tst
Source-Repository head
Type: git
Location: git://github.com/mitre/cpsa.git
Executable cpsamatch
Main-Is: CPSA/Match/Main.hs
Build-Depends: base >= 3 && < 5, containers
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.Match.Match
CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra
Executable cpsa
Main-Is: CPSA/Lib/Main.hs
Build-Depends: base >= 3 && < 5, containers, parallel
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports -threaded -rtsopts
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa CPSA.Lib.Utilities
CPSA.Lib.Pretty CPSA.Lib.SExpr CPSA.Lib.Printer CPSA.Lib.Entry
CPSA.Lib.Algebra CPSA.Lib.AlgebraLibrary CPSA.Lib.State
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.Reduction
CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra CPSA.Lib.Declaration
Executable cpsagraph
Main-Is: CPSA/Graph/Main.hs
Build-Depends: base >= 3 && < 5, containers
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
CPSA.Lib.Printer CPSA.Lib.Notation CPSA.Lib.Entry CPSA.Lib.Algebra
CPSA.Graph.XMLOutput CPSA.Graph.Config
CPSA.Graph.SVG CPSA.Graph.Loader CPSA.Graph.Preskeleton
CPSA.Graph.Layout CPSA.Graph.Tree CPSA.Graph.CompactView
CPSA.Graph.ExpandedView CPSA.Graph.LaTeXView CPSA.Basic.Algebra
Executable cpsashapes
Main-Is: CPSA/Shapes/Main.hs
Build-Depends: base >= 3 && < 5, containers
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
CPSA.Shapes.Shapes CPSA.Basic.Algebra
Executable cpsaannotations
Main-Is: CPSA/Annotations/Main.hs
Build-Depends: base >= 3 && < 5, containers
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
CPSA.Annotations.Formulas CPSA.Annotations.Annotations
CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra
Executable cpsapp
Main-Is: CPSA/Pretty/Main.hs
Build-Depends: base >= 3 && < 5, containers
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
CPSA.Basic.Algebra
Executable cpsajson
Main-Is: CPSA/JSON/Main.hs
Build-Depends: base >= 3 && < 5, containers
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
CPSA.Basic.Algebra
Executable cpsadiff
Main-Is: CPSA/Diff/Main.hs
Build-Depends: base >= 3 && < 5, containers
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
CPSA.Basic.Algebra
Executable cpsasas
Main-Is: CPSA/SAS/Main.hs
Build-Depends: base >= 3 && < 5, containers
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.SAS.SAS
CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra
Executable cpsadebase
Main-Is: CPSA/Debase/Main.hs
Build-Depends: base >= 3 && < 5, containers
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra
CPSA.Basic.Algebra