Name: cpsa Version: 2.2.2 Maintainer: ramsdell@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 possible 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. . We are working towards a version of CPSA with the property that whenever it successfully terminates, every possible execution is described by its output. A proof of this correctness property is also in development. . 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" in a command prompt. New users should study the documentation and the sample inputs in the data directory. The source distribution includes a test suite with an expanded set of input files and program design documentation. 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 implemented the algorithm in Haskell. Category: Cryptography 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 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/cpsatheory.tex 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/cpsa.bib doc/SDAG.lhs doc/cpsatheory.pdf doc/cpsaspec.pdf doc/cpsadesign.pdf src/index.html src/cpsacgi src/cpsacgi.py src/cpsa2svg src/cpsa.el src/httpd_allow_execmem.te src/cpsaops.scm src/preskel src/cpsa.pl src/pp.pl src/sexpr.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 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/dass_simple.tst tst/denning-sacco.scm tst/denning-sacco.tst tst/deorig_contract.scm tst/deorig_contract.tst tst/dhke.scm tst/dhke.tst tst/deorig_simple.scm tst/deorig_simple.tst tst/ds-short.lisp tst/dy.lsp tst/dy.tst tst/encsig.scm tst/encsig.tst tst/epmo_acctnum.scm tst/epmo_acctnum.tst tst/epmo.scm tst/epmo.tst tst/ffgg.scm tst/ffgg.tst tst/fragile_pruning.scm tst/fragile_pruning.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/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/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/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/tor.scm 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 -- Disable with -f-par option during configuration. Flag Par Description: Enable use of the parallel construct par Default: True -- 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. Executable cpsa Main-Is: CPSA/Lib/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.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.DiffieHellman.IntLinEq CPSA.SimpleDiffieHellman.Algebra if flag(par) Cpp-Options: -DHAVE_PAR GHC-Options: -threaded Build-Depends: parallel 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.Lib.Protocol CPSA.Lib.Strand CPSA.Lib.Loader CPSA.Lib.Displayer CPSA.Lib.Cohort CPSA.Lib.CPSA 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 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.Notation CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.Lib.Protocol CPSA.Lib.Strand CPSA.Lib.Loader CPSA.Lib.Displayer CPSA.Lib.Cohort CPSA.Lib.CPSA CPSA.Shapes.Shapes 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.Notation CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.Lib.Protocol CPSA.Lib.Strand CPSA.Lib.Loader CPSA.Lib.Displayer CPSA.Lib.Cohort CPSA.Lib.CPSA CPSA.Annotations.Formulas CPSA.Annotations.Annotations CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra CPSA.DiffieHellman.IntLinEq CPSA.SimpleDiffieHellman.Algebra Executable cpsaparameters Main-Is: CPSA/Parameters/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.Lib.Protocol CPSA.Lib.Strand CPSA.Lib.Loader CPSA.Lib.Displayer CPSA.Lib.Cohort CPSA.Lib.CPSA CPSA.Parameters.Flow CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra CPSA.DiffieHellman.IntLinEq CPSA.SimpleDiffieHellman.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.Notation CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.Lib.Protocol CPSA.Lib.Strand CPSA.Lib.Loader CPSA.Lib.Displayer CPSA.Lib.Cohort CPSA.Lib.CPSA 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.Lib.CPSA