cpsa 2.5.3 → 2.5.4
raw patch · 74 files changed
+87/−69 lines, 74 files
Files
- ChangeLog +13/−0
- cpsa.cabal +3/−2
- doc/cpsadesign.pdf binary
- doc/cpsagoals.pdf binary
- doc/cpsaintroslides.pdf binary
- doc/cpsaoverview.pdf binary
- doc/cpsaprimer.pdf binary
- doc/cpsaspec.pdf binary
- doc/cpsauser.html +1/−1
- doc/index.html +6/−2
- doc/macros.tex +1/−1
- tst/DH_hack.tst +1/−1
- tst/blanchet.tst +1/−1
- tst/completeness-test.tst +1/−1
- tst/crushing.tst +1/−1
- tst/dass_simple.tst +1/−1
- tst/denning-sacco.tst +1/−1
- tst/deorig_contract.tst +1/−1
- tst/deorig_mesg.tst +1/−1
- tst/deorig_simple.tst +1/−1
- tst/dy.tst +1/−1
- tst/encsig.tst +1/−1
- tst/epmo-hash.tst +1/−1
- tst/epmo-key-hash.tst +1/−1
- tst/epmo.tst +1/−1
- tst/epmo_acctnum-key-hash.tst +1/−1
- tst/ffgg.tst +1/−1
- tst/fragile_pruning.tst +1/−1
- tst/goals.tst +1/−1
- tst/hashtest-key-hash.tst +1/−1
- tst/hashtest.tst +1/−1
- tst/incompleteness_example.tst +1/−1
- tst/isoreject.tst +1/−1
- tst/kelly1.tst +1/−1
- tst/kerberos.tst +1/−1
- tst/mass.tst +1/−1
- tst/mass2.tst +1/−1
- tst/missing_contraction.tst +1/−1
- tst/neuman-stubblebine-reauth.tst +1/−1
- tst/neuman-stubblebine.tst +1/−1
- tst/no_contraction.tst +1/−1
- tst/non_transforming.tst +1/−1
- tst/nonaug-prune.tst +1/−1
- tst/ns-l.tst +1/−1
- tst/ns.tst +1/−1
- tst/nsl3.tst +1/−1
- tst/nslsk.tst +1/−1
- tst/or.tst +1/−1
- tst/pca.tst +1/−1
- tst/pen-non-orig-test.tst +1/−1
- tst/pkinit.tst +1/−1
- tst/preprocess.tst +1/−1
- tst/print.tst +1/−1
- tst/pruning1.tst +1/−1
- tst/sigenc.tst +1/−1
- tst/sorted_epmo_acctnum.tst +1/−1
- tst/targetterms2.tst +1/−1
- tst/targetterms6.tst +1/−1
- tst/targetterms8.tst +1/−1
- tst/timestamping.tst +1/−1
- tst/uncarried_keys.tst +1/−1
- tst/unilateral.tst +1/−1
- tst/uo.tst +1/−1
- tst/wang-hash.tst +1/−1
- tst/wang-key-hash.tst +1/−1
- tst/weird.tst +1/−1
- tst/wide-mouth-frog-scyther.tst +1/−1
- tst/wide-mouth-frog.tst +1/−1
- tst/wonthull.tst +1/−1
- tst/wonthull2.tst +1/−1
- tst/wonthull3.tst +1/−1
- tst/woolam.tst +1/−1
- tst/yahalom-6.3.6.tst +1/−1
- tst/yahalom.tst +1/−1
ChangeLog view
@@ -1,9 +1,22 @@+2016-01-12 John D. Ramsdell <ramsdell@mitre.org>++ * cpsa.cabal (Description): Added sentence saying CPSA was+ designed and implemented at The MITRE Corporation.++ * cpsa.cabal (Version): Tagged as version 2.5.4++2015-10-02 John D. Ramsdell <ramsdell@mitre.org>++ * doc/{index,cpsauser}.html: Added width limit of 48em.+ 2015-08-21 John D. Ramsdell <ramsdell@mitre.org> * src/CPSA/*/*.h: Removed leading tabs. * src/CPSA/Annotations/Formulas.hs (EitherS): Made EitherS an instance of Applicative.++ * cpsa.cabal (Version): Tagged as version 2.5.3 2015-08-07 John D. Ramsdell <ramsdell@mitre.org>
cpsa.cabal view
@@ -1,5 +1,5 @@ Name: cpsa-Version: 2.5.3+Version: 2.5.4 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3@@ -41,7 +41,8 @@ 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.+ John D. Ramsdell implemented the algorithm in Haskell. CPSA was+ designed and implemented at The MITRE Corporation. Category: Cryptography Build-Type: Simple Data-Files:
doc/cpsadesign.pdf view
binary file changed (275413 → 275413 bytes)
doc/cpsagoals.pdf view
binary file changed (194913 → 194917 bytes)
doc/cpsaintroslides.pdf view
binary file changed (93179 → 93179 bytes)
doc/cpsaoverview.pdf view
binary file changed (129008 → 129004 bytes)
doc/cpsaprimer.pdf view
binary file changed (277023 → 277025 bytes)
doc/cpsaspec.pdf view
binary file changed (388032 → 388034 bytes)
doc/cpsauser.html view
@@ -7,7 +7,7 @@ <meta name="generator" content="Amaya 9.54, see http://www.w3.org/Amaya/" /> <style type="text/css"> h1 { text-align: center }- body { background: white; color: black }+ body { background: white; color: black; max-width: 48em } </style> </head>
doc/index.html view
@@ -1,9 +1,13 @@ <?xml version="1.0" encoding="UTF-8"?> <html xmlns="http://www.w3.org/1999/xhtml"> <head>- <meta http-equiv="content-type" content="application/xhtml+xml; charset=UTF-8" />+ <meta http-equiv="content-type"+ content="application/xhtml+xml; charset=UTF-8" /> <title>CPSA</title>- <meta name="generator" content="Amaya 9.54, see http://www.w3.org/Amaya/" />+ <style type="text/css">+ h1 { text-align: center }+ body { background: white; color: black; max-width: 48em }+ </style> </head> <body>
doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.5.3}+\newcommand{\version}{2.5.4} \newcommand{\cpsacopying}{\begingroup \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The MITRE Corporation. Permission to copy without fee all or part of
tst/DH_hack.tst view
@@ -1,6 +1,6 @@ (herald "DH Hack" (bound 15)) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from DH_hack.scm") (comment "Strand count bounded at 15")
tst/blanchet.tst view
@@ -1,7 +1,7 @@ (herald "Blanchet's Simple Example Protocol" (comment "There is a flaw in this protocol by design")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from blanchet.scm") (defprotocol blanchet basic
tst/completeness-test.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from completeness-test.scm") (defprotocol completeness-test basic
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from crushing.scm") (defprotocol crushing basic
tst/dass_simple.tst view
@@ -1,6 +1,6 @@ (herald "Distributed Authentication Security Service Protocol Variants") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from dass_simple.scm") (defprotocol dass-simple basic
tst/denning-sacco.tst view
@@ -1,6 +1,6 @@ (herald "Denning-Sacco Protocol") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from denning-sacco.scm") (defprotocol denning-sacco basic
tst/deorig_contract.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from deorig_contract.scm") (defprotocol deorig-contract basic
tst/deorig_mesg.tst view
@@ -1,6 +1,6 @@ (herald deorig-mesg) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from deorig_mesg.scm") (defprotocol deorig-mesg basic
tst/deorig_simple.tst view
@@ -1,6 +1,6 @@ (herald deorig-simple) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from deorig_simple.scm") (defprotocol deorig-simple basic
tst/dy.tst view
@@ -1,6 +1,6 @@ (herald "Example 1.3 from 1983 Dolev-Yao Paper") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from dy.lsp") (defprotocol dy basic
tst/encsig.tst view
@@ -1,7 +1,7 @@ (herald "Encrypted Signed Message Example" (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from encsig.scm") (defprotocol mult-keys-enc-sig basic
tst/epmo-hash.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing" (comment "Annotated with trust management formulas")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from epmo-hash.scm") (defprotocol epmo basic
tst/epmo-key-hash.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing" (comment "Annotated with trust management formulas")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from epmo-key-hash.scm") (defprotocol epmo basic
tst/epmo.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol" (comment "Annotated with trust management formulas")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from epmo.scm") (defprotocol epmo basic
tst/epmo_acctnum-key-hash.tst view
@@ -2,7 +2,7 @@ "Electronic Purchase with Money Order Protocol Variant with Key Hashing" (comment "This version includes account numbers in exchanges")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from epmo_acctnum-key-hash.scm") (defprotocol epmo_acctnum basic
tst/ffgg.tst view
@@ -1,7 +1,7 @@ (herald "The ffgg Protocol" (comment "From A Necessarily Parallel Attack by Jon K. Millen")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from ffgg.scm") (defprotocol ffgg basic
tst/fragile_pruning.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from fragile_pruning.scm") (defprotocol fragile_pruning basic
tst/goals.tst view
@@ -1,6 +1,6 @@ (herald goals) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from goals.scm") (defprotocol ns basic
tst/hashtest-key-hash.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from hashtest-key-hash.scm") (defprotocol hashtest basic
tst/hashtest.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from hashtest.scm") (defprotocol hashtest basic
tst/incompleteness_example.tst view
@@ -1,7 +1,7 @@ (herald incompleteness-example (comment "Shows a shape not found by CPSA")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from incompleteness_example.scm") (defprotocol incompleteness-example basic
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from isoreject.scm") (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from kelly1.scm") (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from kerberos.scm") (defprotocol kerberos basic
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from mass.lsp") (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from mass2.lsp") (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from missing_contraction.scm") (defprotocol missing-contraction basic
tst/neuman-stubblebine-reauth.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from neuman-stubblebine-reauth.lsp") (defprotocol neuman-stubblebine-reauth basic
tst/neuman-stubblebine.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from neuman-stubblebine.scm") (defprotocol neuman-stubblebine basic
tst/no_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from no_contraction.scm") (defprotocol no-contraction basic
tst/non_transforming.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from non_transforming.scm") (defprotocol non_transforming basic
tst/nonaug-prune.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from nonaug-prune.scm") (defprotocol nonaug-prune basic
tst/ns-l.tst view
@@ -1,7 +1,7 @@ (herald "Needham-Schroeder-Low Public-Key Protocol" (comment "With deflistener's")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from ns-l.scm") (defprotocol ns basic
tst/ns.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder Public-Key Protocol Variants") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from ns.scm") (defprotocol ns basic
tst/nsl3.tst view
@@ -1,6 +1,6 @@ (herald "Three Party Needham-Schroeder-Lowe Protocol") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from nsl3.scm") (defprotocol nsl3 basic
tst/nslsk.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from nslsk.scm") (defprotocol nslsk basic
tst/or.tst view
@@ -1,7 +1,7 @@ (herald "Otway-Rees Protocol" (comment "Standard version using variables of sort mesg")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from or.scm") (defprotocol or basic
tst/pca.tst view
@@ -1,7 +1,7 @@ (herald "Privacy Certificate Authority" (bound 15) (comment "Generation of an Attestation Identity Certificate")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from pca.scm") (comment "Strand count bounded at 15")
tst/pen-non-orig-test.tst view
@@ -1,6 +1,6 @@ (herald "pen-non-orig test") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from pen-non-orig-test.scm") (defprotocol pennonorigtest basic
tst/pkinit.tst view
@@ -1,6 +1,6 @@ (herald "Kerberos PK init") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from pkinit.scm") (defprotocol pkinit basic
tst/preprocess.tst view
@@ -1,6 +1,6 @@ (herald "Pre-processing test example: modified NS with two responders") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from preprocess.scm") (defprotocol ns basic
tst/print.tst view
@@ -1,7 +1,7 @@ (herald "Print Test" (comment "See if read forms look like printed ones")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from print.scm") (defprotocol print-test basic
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from pruning1.scm") (defprotocol prune basic
tst/sigenc.tst view
@@ -1,7 +1,7 @@ (herald "Signed Encrypted Message Example" (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from sigenc.scm") (defprotocol mult-keys-sig-enc basic
tst/sorted_epmo_acctnum.tst view
@@ -4,7 +4,7 @@ "This version uses sorts to avoid confusion" "between a nonce and other data")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from sorted_epmo_acctnum.scm") (comment "Strand count bounded at 12")
tst/targetterms2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from targetterms2.scm") (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from targetterms6.scm") (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from targetterms8.scm") (defprotocol targetterms8 basic
tst/timestamping.tst view
@@ -1,6 +1,6 @@ (herald timestamping-service) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from timestamping.scm") (defprotocol timestamping-service basic
tst/uncarried_keys.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from uncarried_keys.scm") (defprotocol uncarried-keys basic
tst/unilateral.tst view
@@ -1,6 +1,6 @@ (herald unilateral) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from unilateral.scm") (defprotocol unilateral basic
tst/uo.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from uo.scm") (defprotocol uniq-orig basic
tst/wang-hash.tst view
@@ -1,6 +1,6 @@ (herald "Wang's Fair Exchange Protocol" (bound 10)) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from wang-hash.scm") (comment "Strand count bounded at 10")
tst/wang-key-hash.tst view
@@ -1,6 +1,6 @@ (herald "Wang's Fair Exchange Protocol" (bound 10)) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from wang-key-hash.scm") (comment "Strand count bounded at 10")
tst/weird.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from weird.scm") (defprotocol weird basic
tst/wide-mouth-frog-scyther.tst view
@@ -1,7 +1,7 @@ (herald "Wide-Mouth Frog Protocol from Scyther" (comment "This protocol has an infinite number of shapes")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from wide-mouth-frog-scyther.lsp") (defprotocol wide-mouth-frog basic
tst/wide-mouth-frog.tst view
@@ -1,7 +1,7 @@ (herald "Wide-Mouth Frog Protocol" (comment "This protocol has an infinite number of shapes")) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from wide-mouth-frog.lsp") (defprotocol wide-mouth-frog basic
tst/wonthull.tst view
@@ -1,6 +1,6 @@ (herald wonthull (bound 9)) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from wonthull.scm") (comment "Strand count bounded at 9")
tst/wonthull2.tst view
@@ -1,6 +1,6 @@ (herald wonthull2 (bound 9)) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from wonthull2.scm") (comment "Strand count bounded at 9")
tst/wonthull3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from wonthull3.scm") (defprotocol wonthull3 basic
tst/woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from woolam.scm") (defprotocol woolam basic
tst/yahalom-6.3.6.tst view
@@ -5,7 +5,7 @@ (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf") (bound 15)) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from yahalom-6.3.6.scm") (comment "Strand count bounded at 15")
tst/yahalom.tst view
@@ -1,6 +1,6 @@ (herald "Yahalom Protocol Without Forwarding" (bound 15)) -(comment "CPSA 2.5.3")+(comment "CPSA 2.5.4") (comment "All input read from yahalom.scm") (comment "Strand count bounded at 15")