cpsa-3.6.11: cpsa.cabal
Name: cpsa
Version: 3.6.11
Maintainer: mliskov@mitre.org
Cabal-Version: >= 1.10
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 possible for a
cryptographic protocol. We call them the shapes of the protocol.
Many 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, and an auxiliary
tool reads off strongest authentication and secrecy goals from the
shapes.
.
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 complete,
i.e. we proved every shape can be found in a finite number of steps,
relative to a procedural semantics of protocol roles. This version
of CPSA has the ability to analyze Diffie-Hellman protocols.
.
The package contains a set of programs used to perform the analysis
and display it in a browser. 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.
.
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 init/Makefile init/template.lisp
examples/IKE_variants.tar.gz examples/IKE_variants_nobase.tar.gz
examples/Makefile examples/blanchet.scm examples/blanchet.xhtml
examples/bltk_or.scm examples/bltk_or.xhtml examples/bltk_test.scm
examples/dh_mim.scm examples/dh_mim.xhtml examples/envelope.scm
examples/envelope.xhtml examples/eq_test.scm examples/eq_test.xhtml
examples/ffgg.scm examples/ffgg.xhtml
examples/fluffy_draft03_fixing_gske.scm
examples/fluffy_draft03_gske.scm
examples/fluffy_draft03_improving_pske.scm
examples/fluffy_draft03_pske.scm examples/fnof_test.scm
examples/fnof_test.xhtml examples/fnof_yahalom.scm
examples/fnof_yahalom.xhtml examples/goals.scm examples/goals.xhtml
examples/iadh_um.scm examples/iadh_um.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/rules.scm examples/rules.xhtml
examples/station.scm examples/station.xhtml
examples/subsort_test.scm examples/subsort_test.xhtml
examples/woolam.scm examples/woolam.xhtml examples/yahalom.scm
examples/yahalom.xhtml
Data-Dir: doc
Extra-Source-Files:
Makefile ChangeLog README.txt NEWS mkghci fixperms 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
src/ocaml/Makefile src/ocaml/README src/ocaml/cpsa.d.itarget
src/ocaml/cpsa.itarget src/ocaml/cpsa.mllib src/ocaml/cpsa.mltop
src/ocaml/cpsa.odocl src/ocaml/expand.ml src/ocaml/main.ml
src/ocaml/main.mli src/ocaml/pp.ml src/ocaml/token.ml
src/ocaml/token.mli src/ocaml/scanner.mll src/ocaml/sexpr.ml
src/ocaml/sexpr.mli src/ocaml/sexpr_type.ml
tst/checktst tst/updatetst tst/cpsagraphtst
tst/Makefile tst/Make.hs tst/README
tst/aik.scm tst/aik.tst tst/attest.scm tst/attest.tst tst/axiom2.scm
tst/axiom2.tst tst/blanchet.scm tst/blanchet.tst tst/bltk_or.scm
tst/bltk_or.tst tst/bltk_test.scm tst/bltk_test.tst tst/comment.scm
tst/comment.tst tst/comp_test.scm tst/comp_test.tst tst/dh-ca.scm
tst/dh-ca.tst tst/dh_group_sig.scm tst/dh_group_sig.tst
tst/dh_mim.scm tst/dh_mim.tst tst/dh_mim2.scm tst/dh_mim2.tst
tst/dh_mim_nobase.scm tst/dh_mim_nobase.tst tst/dh_sig.scm
tst/dh_sig.tst tst/dh_test.scm tst/dh_test.tst tst/dhcr_um.scm
tst/dhcr_um.tst tst/dhcr_um3.scm tst/dhcr_um3.tst tst/dhcr_umx.scm
tst/dhcr_umx.tst tst/dhnsl_basic.scm tst/dhnsl_basic.tst
tst/dhnsl_use.scm tst/dhnsl_use.tst tst/doorsep.scm tst/doorsep.tst
tst/doorsep2invk.scm tst/doorsep2invk.tst tst/eadh_um.scm
tst/eadh_um.tst tst/enrich.scm tst/enrich.tst tst/envelope.scm
tst/envelope.tst tst/envelope_short.scm tst/envelope_short.tst
tst/eq_test.scm tst/eq_test.tst tst/ffgg.scm tst/ffgg.tst
tst/fluffy_draft03_gske.scm tst/fluffy_draft03_gske.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/iadh_um_eq.scm tst/iadh_um_eq.tst
tst/iadh_um_joshua.scm tst/iadh_um_joshua.tst tst/iadh_umx.scm
tst/iadh_umx.tst tst/injection.scm tst/injection.tst tst/kerb.scm
tst/kerb.tst tst/kerberos++.scm tst/kerberos++.tst tst/lt_test.scm
tst/lt_test.tst tst/neq_test.scm tst/neq_test.tst tst/nh-ca-w-dh.scm
tst/nh-ca-w-dh.tst tst/nh-ca.scm tst/nh-ca.tst tst/nhcr_um.scm
tst/nhcr_um.tst tst/nhcr_um3.scm tst/nhcr_um3.tst tst/nhcr_umx.scm
tst/nhcr_umx.tst tst/ns.scm tst/ns.tst tst/or.scm tst/or.tst
tst/ordered.scm tst/ordered.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/precursor.scm tst/precursor.tst
tst/priority_test.scm tst/priority_test.tst tst/prottrans.scm
tst/prottrans.tst tst/reflect.scm tst/reflect.tst tst/reflect_dh.scm
tst/reflect_dh.tst tst/role_uniq.scm tst/role_uniq.tst
tst/rule-order.scm tst/rule-order.tst tst/staticdh.scm
tst/staticdh.tst tst/station.scm tst/station.tst tst/station2.scm
tst/station2.tst tst/station_newhope.scm tst/station_newhope.tst
tst/station_nobase.scm tst/station_nobase.tst tst/stationbase.scm
tst/stationbase.tst tst/subsort_test.scm tst/subsort_test.tst
tst/tag_test.scm tst/tag_test.tst tst/target.scm tst/target.tst
tst/test_g.scm tst/test_g.tst tst/test_small.scm tst/test_small.tst
tst/thinning.scm tst/thinning.tst tst/trust-anchor.scm
tst/trust-anchor.tst tst/ugen_test.scm tst/ugen_test.tst
tst/unilateral.scm tst/unilateral.tst tst/uniq-gen-test.scm
tst/uniq-gen-test.tst tst/uniq_orig_doesnt_fail.scm
tst/uniq_orig_doesnt_fail.tst tst/wd-goalssat.scm
tst/wd-goalssat.tst tst/wd-gs-simple.scm tst/wd-gs-simple.tst
tst/woolam.scm tst/woolam.tst tst/yahalom.scm tst/yahalom.tst
tst/yolo.scm tst/yolo.tst tst/wrap_decrypt.lsp tst/wrap_decrypt.tst
tst/blanchet_doorsep.prot tst/blanchet_doorsep.tst
Source-Repository head
Type: git
Location: git://github.com/mitre/cpsa.git
Executable cpsa
Main-Is: CPSA/Lib/Main.hs
Default-Language: Haskell2010
Build-Depends: base >= 4.13 && < 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.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
Default-Language: Haskell2010
Build-Depends: base >= 4.13 && < 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
Default-Language: Haskell2010
Build-Depends: base >= 4.13 && < 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
Default-Language: Haskell2010
Build-Depends: base >= 4.13 && < 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 cpsadiff
Main-Is: CPSA/Diff/Main.hs
Default-Language: Haskell2010
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
Default-Language: Haskell2010
Build-Depends: base >= 4.13 && < 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 cpsaprot
Main-Is: CPSA/Prot/Main.hs
Default-Language: Haskell2010
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 CPSA.Lib.Expand
Executable cpsapp
Main-Is: CPSA/Pretty/Main.hs
Default-Language: Haskell2010
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
Default-Language: Haskell2010
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 cpsadebase
Main-Is: CPSA/Debase/Main.hs
Default-Language: Haskell2010
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 cpsamatch
Main-Is: CPSA/Match/Main.hs
Default-Language: Haskell2010
Build-Depends: base >= 4.13 && < 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 cpsainit
Main-Is: CPSA/Init/Main.hs
Default-Language: Haskell2010
Build-Depends: base, directory
GHC-Options:
-Wall -fno-warn-name-shadowing -fwarn-unused-imports
Hs-Source-Dirs: src
Other-Modules:
Paths_cpsa
Executable cpsagoalsat
Main-Is: CPSA/GoalSat/Main.hs
Default-Language: Haskell2010
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 cpsa2latex
Main-Is: CPSA/Latex/Main.hs
Default-Language: Haskell2010
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.SExpr CPSA.Lib.Expand CPSA.Lib.Entry
CPSA.Basic.Algebra CPSA.Lib.Algebra CPSA.Lib.Pretty
CPSA.Lib.Printer CPSA.Lib.Utilities