Name:                   cpsa
Version:                4.4.3
Maintainer:             ramsdell@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 in fact be found in a finite number
  of steps, relative to a procedural semantics of protocol roles.
  .
  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 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 is easily installed on operating systems that decend
  from Unix.  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.  CPSA was
  designed and implemented at The MITRE Corporation.
Category:               Cryptography
Build-Type:             Simple
Data-Files:
  index.html cpsalogo.svg readme.html cpsauser.html cpsa4.mk Make4.hs
  init/Makefile cpsaprimer.pdf cpsagoals.pdf cpsaintroslides.pdf cpsaspec.pdf
  cpsafoundation.pdf cpsadesign.pdf cpsa4roletran.md roletran.pdf
  ffgg.scm ns.scm blanchet.scm or.scm woolam.scm yahalom.scm goals.scm
  rules.scm cpsa4manual.pdf

Data-Dir:               doc
Extra-Source-Files:
  Makefile ChangeLog README NEWS mkghci cpsatst fixperms setup.bat doc/README
  doc/src/cpsa.bib doc/src/cmstrands.mp doc/src/macros.tex
  doc/src/cpsa4manual/ns_skel1.pdf doc/src/cpsa4manual/intro.tex
  doc/src/cpsa4manual/cmstrands.mp doc/src/cpsa4manual/state-rules.scm
  doc/src/cpsa4manual/ns_skel0.pdf doc/src/cpsa4manual/algebra.tex
  doc/src/cpsa4manual/tools.tex doc/src/cpsa4manual/declarations.tex
  doc/src/cpsa4manual/ns_skel2.pdf
  doc/src/cpsa4manual/ns_search_tree.eps
  doc/src/cpsa4manual/CPSA_cribsheet.pptx
  doc/src/cpsa4manual/algorithm.tex
  doc/src/cpsa4manual/yahalom_q_resp_pov1.png
  doc/src/cpsa4manual/blanchet_skel13.eps
  doc/src/cpsa4manual/kerb_skel3_operation_circled.pdf
  doc/src/cpsa4manual/secureprotocols.bib
  doc/src/cpsa4manual/envelope_skel10.pdf
  doc/src/cpsa4manual/ns_skel4.pdf doc/src/cpsa4manual/macros.tex
  doc/src/cpsa4manual/plaindh_skel4_5.pdf doc/src/cpsa4manual/ltxs.mk
  doc/src/cpsa4manual/blanchet_tree6.pdf doc/src/cpsa4manual/Makefile
  doc/src/cpsa4manual/yahalom_ch_resp_pov.png
  doc/src/cpsa4manual/kerb_skel4.eps doc/src/cpsa4manual/blanchet.mp
  doc/src/cpsa4manual/cpsadiagrams.mp doc/src/cpsa4manual/goals.tex
  doc/src/cpsa4manual/kerb_skel7.eps
  doc/src/cpsa4manual/ns_skel1_cursor.pdf
  doc/src/cpsa4manual/kerb_skel7.pdf doc/src/cpsa4manual/bcasyntax.tex
  doc/src/cpsa4manual/termtree.mp doc/src/cpsa4manual/strands.mp
  doc/src/cpsa4manual/basic.tex doc/src/cpsa4manual/kerb_skel4.pdf
  doc/src/cpsa4manual/blanchet_tree6.eps
  doc/src/cpsa4manual/ns_skel2_cursor.pdf
  doc/src/cpsa4manual/input.tex
  doc/src/cpsa4manual/examples/plaindh.scm
  doc/src/cpsa4manual/examples/plaindh.tst
  doc/src/cpsa4manual/examples/dhcr_um_expt_assume.scm
  doc/src/cpsa4manual/examples/dhcr_um_expt_assume.tst
  doc/src/cpsa4manual/examples/commitment.scm
  doc/src/cpsa4manual/examples/Makefile
  doc/src/cpsa4manual/examples/minipay-rely-guar.scm
  doc/src/cpsa4manual/examples/open-closed.tst
  doc/src/cpsa4manual/examples/ns.tst
  doc/src/cpsa4manual/examples/kerberos-variant-guar.tst
  doc/src/cpsa4manual/examples/ns.scm
  doc/src/cpsa4manual/examples/open-closed.scm
  doc/src/cpsa4manual/examples/minipay-rely-guar.tst
  doc/src/cpsa4manual/examples/or.scm
  doc/src/cpsa4manual/examples/minipay.tst
  doc/src/cpsa4manual/examples/bltk_test.scm
  doc/src/cpsa4manual/examples/blanchet.scm
  doc/src/cpsa4manual/examples/chan-yahalom-role-decl.tst
  doc/src/cpsa4manual/examples/pkinit.scm
  doc/src/cpsa4manual/examples/blanchet.tst
  doc/src/cpsa4manual/examples/pkinit.tst
  doc/src/cpsa4manual/examples/chan-yahalom-role-decl.scm
  doc/src/cpsa4manual/examples/or.tst
  doc/src/cpsa4manual/examples/minipay.scm
  doc/src/cpsa4manual/examples/bltk_test.tst
  doc/src/cpsa4manual/examples/cpsa4diff_out.tst
  doc/src/cpsa4manual/examples/cpsa4.mk
  doc/src/cpsa4manual/examples/minipay-guar.tst
  doc/src/cpsa4manual/examples/rules.scm
  doc/src/cpsa4manual/examples/minipay-guar.scm
  doc/src/cpsa4manual/examples/kerb.tst
  doc/src/cpsa4manual/examples/kerb.scm
  doc/src/cpsa4manual/examples/open-closed-late-destructure.tst
  doc/src/cpsa4manual/examples/new_dhcr_um_expt_assume.tst
  doc/src/cpsa4manual/examples/chan-yahalom.scm
  doc/src/cpsa4manual/examples/open-closed-late-destructure.scm
  doc/src/cpsa4manual/examples/chan-yahalom.tst
  doc/src/cpsa4manual/cpsaprimer.tex doc/src/cpsa4manual/carriers.mp
  doc/src/cpsa4manual/ns_skel1_cursor.eps
  doc/src/cpsa4manual/CPSA_cribsheet.pdf
  doc/src/cpsa4manual/mitrelogo.mp
  doc/src/cpsa4manual/channels_state.tex
  doc/src/cpsa4manual/blanchet_skel13.pdf
  doc/src/cpsa4manual/ns_search_tree.pdf
  doc/src/cpsa4manual/ns_skel2.eps doc/src/cpsa4manual/ltxmp.mk
  doc/src/cpsa4manual/ns_skel0.eps doc/src/cpsa4manual/ns_skel1.eps
  doc/src/cpsa4manual/trace_constraints.tex
  doc/src/cpsa4manual/cpsa4manual.tex doc/src/cpsa4manual/setup.tex
  doc/src/cpsa4manual/state.tex
  doc/src/cpsa4manual/plaindh_skel4_5.eps
  doc/src/cpsa4manual/ns_skel4.eps
  doc/src/cpsa4manual/envelope_skel10.eps
  doc/src/cpsa4manual/troubleshooting.tex
  doc/src/cpsa4manual/kerb_skel3_operation_circled.eps
  doc/src/Makefile doc/src/blanchet.mp doc/src/cpsadiagrams.mp
  doc/src/cpsaspec.tex doc/src/bcasyntax.tex doc/src/termtree.mp
  doc/src/strands.mp doc/src/cpsaintroslides.tex doc/src/mkdoc
  doc/src/mitreslides.sty doc/src/cpsafoundation.tex
  doc/src/cpsaprimer.tex doc/src/carriers.mp doc/src/mitrelogo.mp
  doc/src/cpsagoals.tex doc/src/rulestheory.tex doc/src/cpsadesign.tex
  doc/SDAG.lhs doc/cpsalogo.mp src/index.html src/cpsajson.py
  src/split.py src/cpsa2svg src/cpsa.el src/cpsaperm.scm src/lastlabel.py
  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/scala/Main.scala
  src/scala/Pretty.scala src/scala/Printer.scala src/scala/SExpr.scala
  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/DH_hack.scm tst/DH_hack.tst tst/Make4.hs tst/Makefile tst/README
  tst/ab.scm tst/ab.tst tst/abc.scm tst/abc.tst tst/aik.scm
  tst/aik.tst tst/atomic-open-closed.scm tst/atomic-open-closed.tst
  tst/attest.scm tst/attest.tst tst/auth-enc.scm tst/auth-enc.tst
  tst/auth-hash.scm tst/auth-hash.tst tst/blanchet.scm
  tst/blanchet.tst tst/blanchet_doorsep.prot tst/blanchet_doorsep.tst
  tst/bug_example.scm tst/bug_example.tst tst/cert_lang.scm
  tst/cert_lang.tst tst/chan-envelope.scm tst/chan-envelope.tst
  tst/chan-perrig-song.scm tst/chan-perrig-song.tst
  tst/chan-unilateral.scm tst/chan-unilateral.tst
  tst/chan-yahalom-role-decl.scm tst/chan-yahalom-role-decl.tst
  tst/chan-yahalom.scm tst/chan-yahalom.tst tst/checktst
  tst/commitment.scm tst/commitment.tst tst/comp_test.scm
  tst/comp_test.tst tst/completeness-test.scm
  tst/completeness-test.tst tst/cpsagraphall tst/cpsagraphtst
  tst/cpsashapesall tst/crushing.scm tst/crushing.tst
  tst/dass-mod.lisp tst/dass.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_mesg.scm
  tst/deorig_mesg.tst tst/deorig_simple.scm tst/deorig_simple.tst
  tst/dh-ca_hack.scm tst/dh-ca_hack.tst tst/dh_encrypt_hack.scm
  tst/dh_encrypt_hack.tst tst/dh_group_sig.scm tst/dh_group_sig.tst
  tst/dh_group_sig_auth_failure.scm tst/dh_group_sig_auth_failure.tst
  tst/dh_mim.lisp tst/dh_mim_hack.scm tst/dh_mim_hack.tst
  tst/dhcr_um.lisp tst/dhcr_um.scm tst/dhcr_um.tst tst/dhcr_um3.scm
  tst/dhcr_um3.tst tst/dhcr_um_exercise_resolved_bug.scm
  tst/dhcr_um_exercise_resolved_bug.tst tst/dhcr_um_expt.scm
  tst/dhcr_um_expt.tst tst/dhcr_umx.scm tst/dhcr_umx.tst
  tst/dhke2.lisp tst/dhnsl_hack.scm tst/dhnsl_hack.tst
  tst/dhstatic-state.scm tst/dhstatic-state.tst tst/disclosure.scm
  tst/disclosure.tst tst/doorsep.scm tst/doorsep.tst
  tst/doorsep2invk.scm tst/doorsep2invk.tst tst/ds-short.lisp
  tst/dy.lsp tst/dy.tst tst/encsig.scm tst/encsig.tst tst/envelope.scm
  tst/envelope.tst 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/epmo_acctnum-key-hash.scm
  tst/epmo_acctnum-key-hash.tst tst/epmo_acctnum.lisp
  tst/epmo_acctnum.tst tst/expand.scm tst/expand.tst tst/facts.scm
  tst/facts.tst tst/factvar.scm tst/factvar.tst tst/ffgg.scm
  tst/ffgg.tst tst/fluffy_draft03_gske.scm tst/fluffy_draft03_gske.tst
  tst/fragile_pruning.scm 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-corrected.scm
  tst/isoreject-corrected.tst tst/isoreject.scm tst/isoreject.tst
  tst/jdg-neuman-stubblebine-reauth.tst tst/kelly1.scm tst/kelly1.tst
  tst/kelly64.lisp tst/kerb5.lisp tst/kerberos.scm tst/kerberos.tst
  tst/locn_envelope.scm tst/locn_envelope.tst tst/mass.lsp
  tst/mass.tst tst/mass2.lsp tst/mass2.tst tst/missing_contraction.scm
  tst/missing_contraction.tst tst/mksas tst/neq_test.scm
  tst/neq_test.tst tst/neuman-stubblebine-alt.lisp
  tst/neuman-stubblebine-reauth-tagged.tst
  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/non_transforming.scm
  tst/non_transforming.tst tst/nonaug-prune.scm tst/nonaug-prune.tst
  tst/ns-l.scm tst/ns-l.tst tst/ns-rebinding.scm tst/ns-rebinding.tst
  tst/ns.scm tst/ns.tst tst/nsl3.scm tst/nsl3.tst tst/nsl4.lisp
  tst/nsl4cm1.lisp tst/nsl4init.lisp tst/nsl4resp1.lisp
  tst/nsl4resp2.lisp tst/nsl4resp3.lisp tst/nsl5.lisp tst/nsl5i.lisp
  tst/nsl5resp3.lisp tst/nslsk.scm tst/nslsk.tst
  tst/open-closed-multiloc.scm tst/open-closed-multiloc.tst
  tst/open-closed-tag.scm tst/open-closed-tag.tst tst/open-closed.scm
  tst/open-closed.tst tst/or.scm tst/or.tst tst/ordered.scm
  tst/ordered.tst tst/par tst/pca.scm tst/pca.tst
  tst/pen-non-orig-test.scm tst/pen-non-orig-test.tst
  tst/pfs-via-pubkey.scm tst/pfs-via-pubkey.tst tst/pkinit.scm
  tst/pkinit.tst tst/preprocess.scm tst/preprocess.tst tst/print.scm
  tst/print.tst tst/prottrans.scm tst/prottrans.tst tst/pruning1.scm
  tst/pruning1.tst tst/puzzle_example.scm tst/puzzle_example.tst
  tst/reflect.scm tst/reflect.tst tst/renamings.scm tst/renamings.tst
  tst/role_uniq.scm tst/role_uniq.tst tst/rule-node.scm
  tst/rule-node.tst tst/rule-order.scm tst/rule-order.tst
  tst/sigenc.scm tst/sigenc.tst tst/sorted_epmo_acctnum.scm
  tst/sorted_epmo_acctnum.tst tst/sts.scm tst/sts.tst
  tst/sts_unflip.scm tst/sts_unflip.tst tst/sts_weak.scm
  tst/sts_weak.tst tst/subatomic-open-closed-test-genrule.scm
  tst/subatomic-open-closed-test-genrule.tst
  tst/subatomic-open-closed.scm tst/subatomic-open-closed.tst
  tst/sync_locn_envelope.scm tst/sync_locn_envelope.tst
  tst/targetterms1.scm tst/targetterms1.tst tst/targetterms2.scm
  tst/targetterms2.tst tst/targetterms6.scm tst/targetterms6.tst
  tst/targetterms8.scm tst/targetterms8.tst
  tst/thisthat.scm tst/thisthat.tst tst/tickle-unique.scm
  tst/tickle-unique.tst tst/timestamping.scm tst/timestamping.tst
  tst/tnsl5.lisp tst/trust-anchor.scm tst/trust-anchor.tst
  tst/uncarried_keys.scm tst/uncarried_keys.tst tst/unilateral.scm
  tst/unilateral.tst tst/uniq-gen-test.scm tst/uniq-gen-test.tst
  tst/uo.scm tst/uo.tst tst/updatetst tst/wang-hash.scm
  tst/wang-hash.tst tst/wang-key-hash-tst.tst tst/wang-key-hash.scm
  tst/wang-key-hash.tst tst/wang.lisp
  tst/weakened-subatomic-open-closed.tst tst/weird.scm tst/weird.tst
  tst/wide-mouth-frog-scyther.lsp tst/wide-mouth-frog-scyther.tst
  tst/wide-mouth-frog.lsp tst/wide-mouth-frog.tst tst/wonthull.scm
  tst/wonthull.tst tst/wonthull2.scm tst/wonthull2.tst
  tst/wonthull3.scm tst/wonthull3.tst tst/woolam.scm tst/woolam.tst
  tst/wrap_decrypt.tst tst/yahalom-6.3.6.scm tst/yahalom-6.3.6.tst
  tst/yahalom.scm tst/yahalom.tst tst/blanchet-strandmax.scm
  tst/blanchet-strandmax.tst tst/ugo.scm tst/ugo.tst
  coq/Sem_tactics.v coq/Comp.v coq/Alt_sem.v coq/Match.v coq/Alg.v
  coq/Exec.v coq/Intro.v coq/Nonce.v coq/Preamble.v
  coq/Unilateral_proof.v coq/Makefile coq/Run.v coq/procdoc.tex
  coq/Run_sem.v coq/_CoqProject coq/Monad.v coq/procdoc.mk coq/README
  coq/Sem.v coq/mkdist coq/Unilateral_role.v coq/mkdoc
  coq/Examples/Bad_unilateral.v coq/Examples/Bad_unilateral_proof.v
  coq/Examples/Bad_unilateral_role.v coq/Examples/Blanchet.v
  coq/Examples/Blanchet_akey.v coq/Examples/Blanchet_akey_proof.v
  coq/Examples/Blanchet_akey_role.v coq/Examples/Blanchet_proof.v
  coq/Examples/Blanchet_role.v coq/Examples/Invk.v
  coq/Examples/Invk_proof.v coq/Examples/Invk_role.v
  coq/Examples/Makefile coq/Examples/Nsl.v coq/Examples/Nsl_proof.v
  coq/Examples/Nsl_role.v coq/Examples/Otway_rees.v
  coq/Examples/Otway_rees_proof.v coq/Examples/Otway_rees_role.v
  coq/Examples/README coq/Examples/Yahalom.v
  coq/Examples/Yahalom_proof.v coq/Examples/Yahalom_role.v
  coq/Examples/_CoqProject coq/Examples/bad_unilateral.scm
  coq/Examples/blanchet.scm coq/Examples/blanchet_akey.scm
  coq/Examples/invk.scm coq/Examples/nsl.scm
  coq/Examples/otway_rees.scm coq/Examples/update
  coq/Examples/yahalom.scm coq/Proc.v
  coq/Derives.v coq/unilateral.scm coq/Unilateral.v coq/Role.v
  coq/Subst.v coq/CSem.v coq/CRun.v coq/CRun_csem.v

Source-Repository head
  Type:     git
  Location: git://github.com/mitre/cpsaexp.git

Executable cpsa4
  Main-Is:              CPSA/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.ReturnFail CPSA.Lib.Pretty
    CPSA.Lib.SExpr CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Options
    CPSA.Algebra CPSA.Protocol CPSA.Strand CPSA.Characteristic
    CPSA.Channel CPSA.LoadFormulas CPSA.GenRules CPSA.Loader
    CPSA.Displayer CPSA.Cohort
    CPSA.Lib.Expand CPSA.Reduction CPSA.Signature

Executable cpsa4sas
  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.Options CPSA.Algebra
    CPSA.Signature CPSA.SAS.SAS

Executable cpsa4prot
  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.Expand

Executable cpsa4goalsat
  Main-Is:              CPSA/GoalSat/Main.hs
  Default-Language:     Haskell2010
  Build-Depends:        base
  GHC-Options:
    -Wall -fno-warn-name-shadowing -fwarn-unused-imports
  Hs-Source-Dirs:       src
  Other-Modules:
    Paths_cpsa CPSA.Lib.Pretty CPSA.Lib.SExpr
    CPSA.Lib.Printer CPSA.Lib.Entry

Executable cpsa4diff
  Main-Is:              CPSA/Diff/Main.hs
  Default-Language:     Haskell2010
  Build-Depends:        base
  GHC-Options:
    -Wall -fno-warn-name-shadowing -fwarn-unused-imports
  Hs-Source-Dirs:       src
  Other-Modules:
    Paths_cpsa CPSA.Lib.Pretty CPSA.Lib.SExpr
    CPSA.Lib.Printer CPSA.Lib.Entry

Executable cpsa4graph
  Main-Is:              CPSA/Graph/Main.hs
  Default-Language:     Haskell2010
  Build-Depends:        base >= 4.13, 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.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 cpsa4shapes
  Main-Is:              CPSA/Shapes/Main.hs
  Default-Language:     Haskell2010
  Build-Depends:        base >= 4.13, containers
  GHC-Options:
    -Wall -fno-warn-name-shadowing -fwarn-unused-imports
  Hs-Source-Dirs:       src
  Other-Modules:
    Paths_cpsa CPSA.Lib.SExpr CPSA.Lib.Pretty CPSA.Lib.Printer
    CPSA.Lib.Entry CPSA.Shapes.Shapes

Executable cpsa4pp
  Main-Is:              CPSA/Pretty/Main.hs
  Default-Language:     Haskell2010
  Build-Depends:        base
  GHC-Options:
    -Wall -fno-warn-name-shadowing -fwarn-unused-imports
  Hs-Source-Dirs:       src
  Other-Modules:
    Paths_cpsa CPSA.Lib.Pretty CPSA.Lib.SExpr
    CPSA.Lib.Printer CPSA.Lib.Entry

Executable cpsa4json
  Main-Is:              CPSA/JSON/Main.hs
  Default-Language:     Haskell2010
  Build-Depends:        base
  GHC-Options:
    -Wall -fno-warn-name-shadowing -fwarn-unused-imports
  Hs-Source-Dirs:       src
  Other-Modules:
    Paths_cpsa CPSA.Lib.Pretty CPSA.Lib.SExpr
    CPSA.Lib.Printer CPSA.Lib.Entry

Executable cpsa4init
  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 cpsa42latex
  Main-Is:              CPSA/Latex/Main.hs
  Default-Language:     Haskell2010
  Build-Depends:        base
  GHC-Options:
    -Wall -fno-warn-name-shadowing -fwarn-unused-imports
  Hs-Source-Dirs:       src
  Other-Modules:
    Paths_cpsa CPSA.Lib.Pretty CPSA.Lib.SExpr
    CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Expand

Executable cpsa4roletran
  Main-Is:              CPSA/Roletran/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.ReturnFail CPSA.Lib.Pretty CPSA.Lib.SExpr
    CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Expand
    CPSA.Roletran.Algebra CPSA.Roletran.Protocol CPSA.Roletran.Loader
    CPSA.Roletran.Displayer CPSA.Roletran.Derivation CPSA.Roletran.Emitter

Executable cpsa4coq
  Main-Is:              CPSA/Coq/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.Pretty CPSA.Lib.SExpr CPSA.Lib.Printer
    CPSA.Lib.Entry CPSA.Lib.Expand CPSA.Proc.Proc

Executable cpsa4rolecoq
  Main-Is:              CPSA/RoleCoq/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.ReturnFail CPSA.Lib.Pretty CPSA.Lib.SExpr
    CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Expand
    CPSA.Roletran.Algebra CPSA.Roletran.Protocol CPSA.Roletran.Loader
    CPSA.Roletran.Displayer CPSA.Roletran.Emitter

Executable cpsa4debranch
  Main-Is:              CPSA/Debranch/Main.hs
  Default-Language:     Haskell2010
  Build-Depends:        base
  GHC-Options:
    -Wall -fno-warn-name-shadowing -fwarn-unused-imports
  Hs-Source-Dirs:       src
  Other-Modules:
    Paths_cpsa CPSA.Lib.Pretty CPSA.Lib.SExpr
    CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Expand

Executable cpsa4query
  Main-Is:              CPSA/Query/Main.hs
  Default-Language:     Haskell2010
  Build-Depends:        base, containers
  GHC-Options:
    -Wall -fno-warn-name-shadowing -fwarn-unused-imports
  Hs-Source-Dirs:       src
  Other-Modules:
    Paths_cpsa CPSA.Lib.Pretty CPSA.Lib.SExpr
    CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Expand
    CPSA.Lib.Utilities
    CPSA.Query.Loader CPSA.Query.Tree CPSA.Query.Query