• Home
• Search 
• Browse
• What's new
• Upload
• User accounts

Directory listing for cpsa-4.4.7 source tarball

cpsa-4.4.7/

• ChangeLog
• Makefile
• NEWS
• README
• Setup.hs
• build.xml
• cinstall
• cpsa.cabal
• cpsatst
• dbtst
• fixperms
• license.txt
• mkghci
• setup.bat
• coq/
  • Alg.v
  • Alt_sem.v
  • CRun.v
  • CRun_csem.v
  • CSem.v
  • Comp.v
  • Derives.v
  • Exec.v
  • Intro.v
  • Makefile
  • Match.v
  • Monad.v
  • Nonce.v
  • Preamble.v
  • Proc.v
  • README
  • Role.v
  • Run.v
  • Run_sem.v
  • Sem.v
  • Sem_tactics.v
  • Subst.v
  • Unilateral.v
  • Unilateral_proof.v
  • Unilateral_role.v
  • _CoqProject
  • mkdist
  • mkdoc
  • procdoc.mk
  • procdoc.tex
  • unilateral.scm
  • Examples/
    • Bad_unilateral.v
    • Bad_unilateral_proof.v
    • Bad_unilateral_role.v
    • Blanchet.v
    • Blanchet_akey.v
    • Blanchet_akey_proof.v
    • Blanchet_akey_role.v
    • Blanchet_proof.v
    • Blanchet_role.v
    • Invk.v
    • Invk_proof.v
    • Invk_role.v
    • Makefile
    • Nsl.v
    • Nsl_proof.v
    • Nsl_role.v
    • Otway_rees.v
    • Otway_rees_proof.v
    • Otway_rees_role.v
    • README
    • Yahalom.v
    • Yahalom_proof.v
    • Yahalom_role.v
    • _CoqProject
    • bad_unilateral.scm
    • blanchet.scm
    • blanchet_akey.scm
    • invk.scm
    • nsl.scm
    • otway_rees.scm
    • update
    • yahalom.scm
• doc/
  • Make4.hs
  • README
  • SDAG.lhs
  • blanchet.scm
  • cpsa4.mk
  • cpsa4manual.pdf
  • cpsa4prolog.pl
  • cpsa4roletran.md
  • cpsadesign.pdf
  • cpsafoundation.pdf
  • cpsagoals.pdf
  • cpsaintroslides.pdf
  • cpsalogo.mp
  • cpsalogo.svg
  • cpsaprimer.pdf
  • cpsaspec.pdf
  • cpsauser.html
  • ffgg.scm
  • goals.scm
  • index.html
  • ns.scm
  • or.scm
  • readme.html
  • roletran.pdf
  • rules.scm
  • woolam.scm
  • yahalom.scm
  • init/
    • Makefile
  • src/
    • Makefile
    • bcasyntax.tex
    • blanchet.mp
    • carriers.mp
    • cmstrands.mp
    • cpsa.bib
    • cpsadesign.tex
    • cpsadiagrams.mp
    • cpsafoundation.tex
    • cpsagoals.tex
    • cpsaintroslides.tex
    • cpsaprimer.tex
    • cpsaspec.tex
    • macros.tex
    • mitrelogo.mp
    • mitreslides.sty
    • mkdoc
    • rulestheory.tex
    • strands.mp
    • termtree.mp
    • cpsa4manual/
      • CPSA_cribsheet.pdf
      • CPSA_cribsheet.pptx
      • Makefile
      • algebra.tex
      • algorithm.tex
      • basic.tex
      • bcasyntax.tex
      • blanchet.mp
      • blanchet_skel13.eps
      • blanchet_skel13.pdf
      • blanchet_tree6.eps
      • blanchet_tree6.pdf
      • carriers.mp
      • channels_state.tex
      • cmstrands.mp
      • cpsa4manual.tex
      • cpsadiagrams.mp
      • cpsaprimer.tex
      • declarations.tex
      • envelope_skel10.eps
      • envelope_skel10.pdf
      • goals.tex
      • input.tex
      • intro.tex
      • kerb_skel3_operation_circled.eps
      • kerb_skel3_operation_circled.pdf
      • kerb_skel4.eps
      • kerb_skel4.pdf
      • kerb_skel7.eps
      • kerb_skel7.pdf
      • ltxmp.mk
      • ltxs.mk
      • macros.tex
      • mitrelogo.mp
      • ns_search_tree.eps
      • ns_search_tree.pdf
      • ns_skel0.eps
      • ns_skel0.pdf
      • ns_skel1.eps
      • ns_skel1.pdf
      • ns_skel1_cursor.eps
      • ns_skel1_cursor.pdf
      • ns_skel2.eps
      • ns_skel2.pdf
      • ns_skel2_cursor.pdf
      • ns_skel4.eps
      • ns_skel4.pdf
      • plaindh_skel4_5.eps
      • plaindh_skel4_5.pdf
      • secureprotocols.bib
      • setup.tex
      • state-rules.scm
      • state.tex
      • strands.mp
      • termtree.mp
      • tools.tex
      • trace_constraints.tex
      • troubleshooting.tex
      • yahalom_ch_resp_pov.png
      • yahalom_q_resp_pov1.png
      • examples/
        • Makefile
        • blanchet.scm
        • blanchet.tst
        • bltk_test.scm
        • bltk_test.tst
        • chan-yahalom-role-decl.scm
        • chan-yahalom-role-decl.tst
        • chan-yahalom.scm
        • chan-yahalom.tst
        • commitment.scm
        • cpsa4.mk
        • cpsa4diff_out.tst
        • dhcr_um_expt_assume.scm
        • dhcr_um_expt_assume.tst
        • kerb.scm
        • kerb.tst
        • kerberos-variant-guar.tst
        • minipay-guar.scm
        • minipay-guar.tst
        • minipay-rely-guar.scm
        • minipay-rely-guar.tst
        • minipay.scm
        • minipay.tst
        • new_dhcr_um_expt_assume.tst
        • ns.scm
        • ns.tst
        • open-closed-late-destructure.scm
        • open-closed-late-destructure.tst
        • open-closed.scm
        • open-closed.tst
        • or.scm
        • or.tst
        • pkinit.scm
        • pkinit.tst
        • plaindh.scm
        • plaindh.tst
        • rules.scm
• src/
  • cpsa.el
  • cpsa.pl
  • cpsa2svg
  • cpsajson.py
  • cpsaops.scm
  • cpsaperm.scm
  • ghcmemlimit
  • index.html
  • js2hs
  • lastlabel.py
  • perm.pl
  • pp.pl
  • preskel
  • prover9.pl
  • sexpr.pl
  • split.py
  • unsorted.pl
  • zoom.js
  • CPSA/
    • Algebra.hs
    • Channel.hs
    • Characteristic.hs
    • Cohort.hs
    • Displayer.hs
    • GenRules.hs
    • LoadFormulas.hs
    • Loader.hs
    • Main.hs
    • Operation.hs
    • Options.hs
    • Protocol.hs
    • Reduction.hs
    • Signature.hs
    • Strand.hs
    • Coq/
      • Main.hs
    • DL/
      • Compiler.hs
      • Loader.hs
      • Main.hs
      • Prolog.hs
      • Simplifier.hs
      • Structs.hs
    • Db/
      • Displayer.hs
      • Loader.hs
      • Main.hs
      • Structs.hs
      • Tree.hs
    • DbProlog/
      • Main.hs
    • Debranch/
      • Main.hs
    • Diff/
      • Main.hs
    • GoalSat/
      • Main.hs
    • Graph/
      • CompactView.hs
      • Config.hs
      • ExpandedView.hs
      • LaTeXView.hs
      • Layout.hs
      • Loader.hs
      • Main.hs
      • Preskeleton.hs
      • SVG.hs
      • Tree.hs
      • XMLOutput.hs
    • Init/
      • Main.hs
    • JSON/
      • Main.hs
    • Latex/
      • Main.hs
    • Lib/
      • Entry.hs
      • Expand.hs
      • Pretty.hs
      • Printer.hs
      • ReturnFail.hs
      • SExpr.hs
      • Utilities.hs
    • Pretty/
      • Main.hs
    • Proc/
      • Proc.hs
    • Prot/
      • Main.hs
    • Query/
      • Loader.hs
      • Main.hs
      • Query.hs
      • Tree.hs
    • RoleCoq/
      • Main.hs
    • Roletran/
      • Algebra.hs
      • Derivation.hs
      • Displayer.hs
      • Emitter.hs
      • Loader.hs
      • Main.hs
      • Protocol.hs
    • SAS/
      • Main.hs
      • SAS.hs
    • Shapes/
      • Main.hs
      • Shapes.hs
  • ocaml/
    • Makefile
    • README
    • cpsa.d.itarget
    • cpsa.itarget
    • cpsa.mllib
    • cpsa.mltop
    • cpsa.odocl
    • expand.ml
    • main.ml
    • main.mli
    • pp.ml
    • scanner.mll
    • sexpr.ml
    • sexpr.mli
    • sexpr_type.ml
    • token.ml
    • token.mli
  • scala/
    • Main.scala
    • Pretty.scala
    • Printer.scala
    • SExpr.scala
• tst/
  • DH_hack.scm
  • DH_hack.tst
  • Makefile
  • README
  • ab.scm
  • ab.tst
  • abc.scm
  • abc.tst
  • aik.scm
  • aik.tst
  • atomic-open-closed.scm
  • atomic-open-closed.tst
  • attest.scm
  • attest.tst
  • auth-enc.scm
  • auth-enc.tst
  • auth-hash.scm
  • auth-hash.tst
  • blanchet-strandmax.scm
  • blanchet-strandmax.tst
  • blanchet.scm
  • blanchet.tst
  • blanchet_doorsep.prot
  • blanchet_doorsep.tst
  • bug_example.scm
  • bug_example.tst
  • cert_lang.scm
  • cert_lang.tst
  • chan-envelope.scm
  • chan-envelope.tst
  • chan-perrig-song.scm
  • chan-perrig-song.tst
  • chan-unilateral.scm
  • chan-unilateral.tst
  • chan-yahalom-role-decl.scm
  • chan-yahalom-role-decl.tst
  • chan-yahalom.scm
  • chan-yahalom.tst
  • commitment.scm
  • commitment.tst
  • comp_test.scm
  • comp_test.tst
  • completeness-test.scm
  • completeness-test.tst
  • crushing.scm
  • crushing.tst
  • dass-mod.lisp
  • dass.lisp
  • dass_simple.scm
  • dass_simple.tst
  • defact-atomic-open-closed.tst
  • defact-atomic-open-closed_shapes.tst
  • defact-dhstatic-state.tst
  • defact-dhstatic-state_shapes.tst
  • defact-locn_envelope.tst
  • defact-locn_envelope_shapes.tst
  • defact-open-closed-multiloc.tst
  • defact-open-closed-multiloc_shapes.tst
  • defact-open-closed-tag.tst
  • defact-open-closed-tag_shapes.tst
  • defact-open-closed.tst
  • defact-open-closed_shapes.tst
  • defact-subatomic-open-closed-test-genrule.tst
  • defact-subatomic-open-closed-test-genrule_shapes.tst
  • defact-subatomic-open-closed.tst
  • defact-subatomic-open-closed_shapes.tst
  • defact-sync_locn_envelope.tst
  • defact-sync_locn_envelope_shapes.tst
  • denning-sacco.scm
  • denning-sacco.tst
  • deorig_contract.scm
  • deorig_contract.tst
  • deorig_mesg.scm
  • deorig_mesg.tst
  • deorig_simple.scm
  • deorig_simple.tst
  • dh-ca_hack.scm
  • dh-ca_hack.tst
  • dh_encrypt_hack.scm
  • dh_encrypt_hack.tst
  • dh_group_sig.scm
  • dh_group_sig.tst
  • dh_group_sig_auth_failure.scm
  • dh_group_sig_auth_failure.tst
  • dh_mim.lisp
  • dh_mim_hack.scm
  • dh_mim_hack.tst
  • dhke2.lisp
  • dhnsl_hack.scm
  • dhnsl_hack.tst
  • dhstatic-state.scm
  • dhstatic-state.tst
  • disclosure.scm
  • disclosure.tst
  • doorsep.scm
  • doorsep.tst
  • doorsep2invk.scm
  • doorsep2invk.tst
  • ds-short.lisp
  • dy.lsp
  • dy.tst
  • encsig.scm
  • encsig.tst
  • envelope.scm
  • envelope.tst
  • epmo-hash.scm
  • epmo-hash.tst
  • epmo-key-hash.scm
  • epmo-key-hash.tst
  • epmo.scm
  • epmo.tst
  • epmo_acctnum-key-hash.scm
  • epmo_acctnum-key-hash.tst
  • epmo_acctnum.lsp
  • epmo_acctnum.tst
  • example.tst
  • expand.scm
  • expand.tst
  • facts.scm
  • facts.tst
  • factvar.scm
  • factvar.tst
  • ffgg.scm
  • ffgg.tst
  • fluffy_draft03_gske.scm
  • fluffy_draft03_gske.tst
  • fragile_pruning.scm
  • fragile_pruning.tst
  • goals.scm
  • goals.tst
  • goalsvar.scm
  • goalsvar.tst
  • hashtest-key-hash.scm
  • hashtest-key-hash.tst
  • hashtest.scm
  • hashtest.tst
  • incompleteness_example.scm
  • incompleteness_example.tst
  • isoreject-corrected.scm
  • isoreject-corrected.tst
  • isoreject.scm
  • isoreject.tst
  • jdg-wonthull.tst
  • kelly1.scm
  • kelly1.tst
  • kelly64.lisp
  • kerb5.lisp
  • kerberos-variant-guar.tst
  • kerberos.scm
  • kerberos.tst
  • locn_envelope.scm
  • locn_envelope.tst
  • mass.lsp
  • mass.tst
  • mass2.lsp
  • mass2.tst
  • missing_contraction.scm
  • missing_contraction.tst
  • neq_test.scm
  • neq_test.tst
  • neuman-stubblebine-alt.lisp
  • neuman-stubblebine-reauth-tagged.tst
  • neuman-stubblebine-reauth.lisp
  • neuman-stubblebine-reauth.lsp
  • neuman-stubblebine-reauth.tst
  • neuman-stubblebine.scm
  • neuman-stubblebine.tst
  • no_contraction.scm
  • no_contraction.tst
  • non_transforming.scm
  • non_transforming.tst
  • nonaug-prune.scm
  • nonaug-prune.tst
  • ns-l.scm
  • ns-l.tst
  • ns-rebinding.scm
  • ns-rebinding.tst
  • ns-unrebinding.scm
  • ns-unrebinding.tst
  • ns.scm
  • ns.tst
  • nsl3.scm
  • nsl3.tst
  • nsl4.lisp
  • nsl4cm1.lisp
  • nsl4init.lisp
  • nsl4resp1.lisp
  • nsl4resp2.lisp
  • nsl4resp3.lisp
  • nsl5.lisp
  • nsl5i.lisp
  • nsl5resp3.lisp
  • nslsk.scm
  • nslsk.tst
  • open-closed-multiloc.scm
  • open-closed-multiloc.tst
  • open-closed-tag.scm
  • open-closed-tag.tst
  • open-closed.scm
  • open-closed.tst
  • or.scm
  • or.tst
  • ordered.scm
  • ordered.tst
  • orderedvar.scm
  • orderedvar.tst
  • pca.scm
  • pca.tst
  • pen-non-orig-test.scm
  • pen-non-orig-test.tst
  • pfs-via-pubkey.scm
  • pfs-via-pubkey.tst
  • pkinit.scm
  • pkinit.tst
  • preprocess.scm
  • preprocess.tst
  • print.scm
  • print.tst
  • prottrans.scm
  • prottrans.tst
  • pruning1.scm
  • pruning1.tst
  • puzzle_example.scm
  • puzzle_example.tst
  • reflect.scm
  • reflect.tst
  • renamings.scm
  • renamings.tst
  • role_uniq.scm
  • role_uniq.tst
  • rule-node.scm
  • rule-node.tst
  • rule-order.scm
  • rule-order.tst
  • sa.tst
  • sigenc.scm
  • sigenc.tst
  • sorted_epmo_acctnum.scm
  • sorted_epmo_acctnum.tst
  • sts.scm
  • sts.tst
  • sts_non_role.scm
  • sts_non_role.tst
  • sts_weakened_reflect.scm
  • sts_weakened_reflect.tst
  • subatomic-open-closed-dist.tst
  • subatomic-open-closed-test-genrule.scm
  • subatomic-open-closed-test-genrule.tst
  • subatomic-open-closed.scm
  • subatomic-open-closed.tst
  • sync_locn_envelope.scm
  • sync_locn_envelope.tst
  • targetterms1.scm
  • targetterms1.tst
  • targetterms2.scm
  • targetterms2.tst
  • targetterms6.scm
  • targetterms6.tst
  • targetterms8.scm
  • targetterms8.tst
  • thisthat.scm
  • thisthat.tst
  • tickle-unique.scm
  • tickle-unique.tst
  • timestamping.scm
  • timestamping.tst
  • tmp-yahalom.tst
  • tnsl5.lisp
  • trust-anchor.scm
  • trust-anchor.tst
  • ugen-at.scm
  • ugen-at.tst
  • ugo.scm
  • ugo.tst
  • uncarried_keys.scm
  • uncarried_keys.tst
  • unilateral.scm
  • unilateral.tst
  • uniq-at.scm
  • uniq-at.tst
  • uniq-gen-test.scm
  • uniq-gen-test.tst
  • uo.scm
  • uo.tst
  • wang-hash.scm
  • wang-hash.tst
  • wang-key-hash.scm
  • wang-key-hash.tst
  • wang.lisp
  • weird.scm
  • weird.tst
  • wide-mouth-frog-scyther.lsp
  • wide-mouth-frog-scyther.tst
  • wide-mouth-frog.lsp
  • wide-mouth-frog.tst
  • wonthull.scm
  • wonthull.tst
  • wonthull2.scm
  • wonthull2.tst
  • wonthull3.scm
  • wonthull3.tst
  • woolam.scm
  • woolam.tst
  • yahalom-6.3.6.scm
  • yahalom-6.3.6.tst
  • yahalom-forward.scm
  • yahalom-forward.tst
  • yahalom.scm
  • yahalom.tst
  • yes-or-no.scm
  • yes-or-no.tst