Directory listing for cpsa-4.4.5 source tarball
cpsa-4.4.5/
- 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
- 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/
- 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
- cpsa4prolog.pl
- 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/
- ocaml/
- scala/
- tst/
- DH_hack.scm
- DH_hack.tst
- Make4.hs
- 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
- 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
- dhcr_um.lisp
- dhcr_um.scm
- dhcr_um.tst
- dhcr_um3.scm
- dhcr_um3.tst
- dhcr_um3_goals.scm
- dhcr_um3_goals.tst
- dhcr_um_goals.scm
- dhcr_um_implicit_auth.scm
- dhcr_umx.scm
- dhcr_umx.tst
- dhcr_umx_goals.scm
- dhcr_umx_implicit_auth.scm
- 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
- 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.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
- 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_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
- 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