cpsa-4.4.1: doc/src/cpsa.bib
@Book{Pierce91,
author = {Benjamin C. Pierce},
title = {Basic Category Theory for Computer Sicentists},
publisher = {The {MIT} Press},
year = 1991}
@Unpublished{DoghmiGuttmanThayer06a,
author = {Shaddin F. Doghmi and Joshua D.~Guttman and F. Javier
Thayer},
title = {Searching for Shapes in Cryptographic Protocols (Extended Version)},
note = {\url{http://eprint.iacr.org/2006/435}},
month = nov,
year = 2006}
@InProceedings{DoghmiGuttmanThayer07,
author = {Shaddin F. Doghmi and
Joshua D. Guttman and
F. Javier Thayer},
title = {Searching for Shapes in Cryptographic Protocols},
booktitle = {Tools and Algorithms for Construction and
Analysis of Systems {(TACAS)}},
year = 2007,
series = {LNCS},
number = 4424,
pages = {523--538},
month = mar,
publisher = {Springer},
note = {Extended version at \url{http://eprint.iacr.org/2006/435}}}
@InProceedings{Fay79,
author = {M. Fay},
title = {First-order Unification in an Equational Theory},
booktitle = {Proc. 4th Workshop on Automated Deduction},
year = 1979}
@Book{BaaderNipkow98,
author = {Franz Baader and Tobias Nipkow},
title = {Term Rewriting and All That},
publisher = {Cambridge University Press},
year = 1998}
@Book{Paulson91,
author = {Laurence C. Paulson},
title = {ML for the Working Programmer},
publisher = {Cambridge University Press},
year = 1991}
@Book{RobinsonVoronkov01,
author = {Alan Robinson and Andrei Voronkov},
title = {Handbook of Automated Reasoning},
vol = 1,
publisher = {The {MIT} Press},
year = 2001}
@InCollection{BaaderSnyder01,
author = {Franz Baader and Wayne Snyder},
title = {Unification Theory},
booktitle = {Handbook of Automated Reasoning},
publisher = {The {MIT} Press},
year = 2001,
editor = {Alan Robinson and Andrei Voronkov},
volume = 1,
chapter = 8,
note = {\url{https://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf}}}
@book{Knuth81,
author = {Donald E. Knuth},
title = {The Art of Computer Programming, Volume {II:} Seminumerical Algorithms,
2nd Edition},
publisher = {Addison-Wesley},
year = {1981},
isbn = {0-201-03822-6},
timestamp = {Thu, 03 Jan 2002 11:51:07 +0100},
biburl = {http://dblp.org/rec/bib/books/aw/Knuth81},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@Misc{agum09,
author = {John D. Ramsdell},
title = {{AGUM}: Unification and Matching in an Abelian Group},
booktitle = {Hackage},
publisher = {The MITRE Corporation},
year = 2009,
note = {\url{http://hackage.haskell.org/package/agum}}
}
@InProceedings{KepserRichts99,
author = {Stephan Kepser and J\"{o}rn Richts},
title = {Optimisation Techniques for Combining Constraint Solvers},
booktitle = {Frontiers of Combining Systems 2},
pages = {193--210},
year = 1999,
editor = {Maarten de Rijke and Dov Gabbay},
address = {Asmsterdam},
publisher = {Research Studies Press/Wiley},
note = {\url{http://tcl.sfs.uni-tuebingen.de/~kepser/papers/optimisation.ps.gz}}}
@InProceedings{MeadowsNarendran02,
author = {Catherine Meadows and Paliath Narendran},
title = {A Unification Algorithm for the Group Diffie-Hellman Protocol},
booktitle = {WITS 2002},
month = jan,
year = 2002,
note = {\url{http://www.dsi.unive.it/IFIPWG1_7/WITS2002/prog/annotated_program.html}}}
@PhdThesis{Liu12,
author = {Zhiqiang Liu},
title = {Dealing Efficiently with Exclusive OR, Abelian
Groups and Homomorphism in Cryptographic Protocol
Analysis},
school = {Clarkson University},
year = 2012,
month = sep,
note = {\url{http://people.clarkson.edu/~clynch/papers/}}}
@article{GoguenMeseguer92,
author = "Joseph A. Goguen and Jose Meseguer",
title = "Order-Sorted Algebra {I}: Equational Deduction for Multiple
Inheritance, Overloading, Exceptions and Partial Operations",
journal = "Theoretical Computer Science",
volume = "105",
number = "2",
pages = "217--273",
year = "1992",
url = "citeseer.ist.psu.edu/goguen92ordersorted.html" }
@inproceedings{Millen99,
author = "Jonathan K. Millen",
title = "A Necessarily Parallel Attack",
booktitle = "Workshop on Formal Methods and Security Protocols,
Part of the Federated Logic Conference",
address = "Trento, Italy",
editor = "Nevin Heintze and Edmund Clarke",
year = "1999",
url = "citeseer.ist.psu.edu/millen99necessarily.html" }
@inproceedings{PavlovicMeadows06,
author = "Dusko Pavlovic and Catherine Meadows",
title = "Deriving Secrecy in Key Establishment Protocols",
booktitle = "European Symposium on Research in Computer Security",
month = sep,
year = 2006,
url = "http://www.kestrel.edu/home/people/pavlovic/security.html" }
@article{GansnerNorth00,
author = "Emden R. Gansner and Stephen C. North",
title = "An open graph visualization system and its applications to software engineering",
journal = "Soft\-ware --- Prac\-tice and Experience",
volume = "30",
number = "11",
pages = "1203--1233",
year = "2000",
url = "citeseer.ist.psu.edu/gansner99open.html" }
@Unpublished{Dijkstra82,
author = {Edsger W. Dijkstra},
title = {Why numbering should start at zero},
note = {\url{http://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/EWD831.html}},
month = aug,
year = 1982}
@article{GuttmanThayer02,
author = {Joshua D. Guttman and
F. Javier Thayer},
title = {Authentication tests and the structure of bundles},
journal = {Theor. Comput. Sci.},
volume = {283},
number = {2},
year = {2002},
pages = {333--380},
ee = {http://dx.doi.org/10.1016/S0304-3975(01)00139-6},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{ThayerEtal99,
author = {F. Javier Thayer and
Jonathan C. Herzog and
Joshua D. Guttman},
title = {Strand Spaces: Proving Security Protocols Correct},
journal = {Journal of Computer Security},
volume = {7},
number = {1},
year = {1999},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DolevYao83,
author = "Daniel Dolev and Andrew Yao",
title = "On the security of public-key protocols",
journal = "{IEEE} Transactions on Information Theory",
volume = 29,
pages = "198--208",
year = 1983
}
@TechReport{cpsatheory11,
title = {Completeness of {CPSA}},
author = {Moses D.~Liskov and Paul D.~Rowe and F.~Javier Thayer},
institution = {The MITRE Corporation},
year = 2011,
number = {MTR110479},
}
@Manual{cpsaspec09,
title = {The {CPSA} Specification:
A Reduction System for Searching for Shapes in Cryptographic Protocols},
OPTkey = {},
author = {John D.~Ramsdell and Joshua D.~Guttman and Moses D.~Liskov and Paul D.~Rowe},
organization = {The MITRE Corporation},
OPTaddress = {},
OPTedition = {},
OPTmonth = {},
year = 2009,
note = {In \url{https://github.com/mitre/cpsaexp} source
distribution, \texttt{doc} directory},
OPTannote = {}
}
@Manual{cpsadesign09,
title = {{CPSA} Design},
OPTkey = {},
author = {John D.~Ramsdell and Joshua D.~Guttman},
organization = {The MITRE Corporation},
OPTaddress = {},
OPTedition = {},
OPTmonth = {},
year = 2009,
note = {In \url{https://github.com/mitre/cpsaexp} source
distribution, \texttt{doc} directory},
OPTannote = {}
}
@Manual{cpsaprimer09,
title = {{CPSA} Primer},
OPTkey = {},
author = {John D.~Ramsdell and Joshua D.~Guttman},
organization = {The MITRE Corporation},
OPTaddress = {},
OPTedition = {},
OPTmonth = {},
year = 2009,
note = {In \url{https://github.com/mitre/cpsaexp} source
distribution, \texttt{doc} directory},
OPTannote = {}
}
@Manual{cpsagoals09,
title = {{CPSA} Security Goals and Rules},
OPTkey = {},
author = {John D.~Ramsdell},
organization = {The MITRE Corporation},
OPTaddress = {},
OPTedition = {},
OPTmonth = {},
year = 2015,
note = {In \url{https://github.com/mitre/cpsaexp} source
distribution, \texttt{doc} directory},
OPTannote = {}
}
@Manual{cpsaoverview09,
title = {{CPSA} Overview},
OPTkey = {},
author = {John D.~Ramsdell and Joshua D.~Guttman},
organization = {The MITRE Corporation},
OPTaddress = {},
OPTedition = {},
OPTmonth = {},
year = 2009,
note = {In \url{https://github.com/mitre/cpsaexp} source
distribution, \texttt{doc} directory},
OPTannote = {}
}
@Manual{cpsauser09,
title = {{CPSA} User Guide},
OPTkey = {},
author = {John D.~Ramsdell},
organization = {The MITRE Corporation},
OPTaddress = {},
OPTedition = {},
OPTmonth = {},
year = 2009,
note = {In \url{https://github.com/mitre/cpsaexp} source
distribution, \texttt{doc} directory},
OPTannote = {}
}
@Manual{cpsa09,
author = {John D. Ramsdell and Joshua D. Guttman},
title = {{CPSA4}: A cryptographic protocol shapes analyzer},
organization = {The MITRE Corporation},
year = 2018,
note = {\url{https://github.com/mitre/cpsaexp}},
}
@unpublished{algimpl11,
author = {Moses Liskov and John D. Ramsdell},
title = {Implementing Strand Space Algebras},
note = {\url{http://www.ccs.neu.edu/home/ramsdell/papers/algimpl.pdf}},
year = 2011
}
@incollection{ComonLundhMillen10,
author= {H. Comon-Lundh and S. Delaune and J. Millen},
title = {Constraint solving techniques and enriching
the model with equational theories},
booktitle = {Formal Models and Techniques for Analyzing
Security Protocols},
editor = {Veronique Cortier and Steve Kremer},
series = {Cryptology and Information Security Series},
volume = 5,
year = 2011,
isbn = {978-1-60750-713-0},
publisher = {{ISO} Press}
}
@InCollection{Guttman11,
author = {Joshua D. Guttman},
title = {Shapes: Surveying Crypto Protocol Runs},
booktitle = {Formal Models and Techniques for Analyzing
Security Protocols},
key = {CortierKremer2011},
publisher = {{IOS} Press},
year = 2011,
volume = 5,
isbn = {978-1-60750-713-0},
editor = {Veronique Cortier and Steve Kremer},
series = {Cryptology and Information Security Series}}
@article{CokerEtAl11,
author = {George Coker and Joshua Guttman and Peter Loscocco and
Amy Herzog and Jonathan Millen and Brian O'Hanlon
and John Ramsdell and Ariel Segall and Justin Sheehy
and Brian Sniffen},
affiliation = {National Security Agency and The MITRE Corporation},
title = {Principles of remote attestation},
journal = {International Journal of Information Security},
publisher = {Springer Berlin / Heidelberg},
issn = {1615-5262},
keyword = {Computer Science},
pages = {63-81},
volume = {10},
issue = {2},
url = {http://dx.doi.org/10.1007/s10207-011-0124-7},
note = {10.1007/s10207-011-0124-7},
year = {2011}
}
@InProceedings{Guttman09,
author = {Joshua D. Guttman},
title = {Security Theorems via Model Theory},
OPTcrossref = {},
OPTkey = {},
booktitle = {Express: Expressiveness in Concurrency,
Workshop affiliated with Concur},
OPTpages = {},
year = 2009,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
month = sep,
OPTorganization = {},
OPTpublisher = {},
note = {Post-proceedings to appear in EPTCS,
\url{http://www.eptcs.org/}},
OPTannote = {}
}
@article{DenningSacco81,
author = {Dorothy E. Denning and Giovanni M. Sacco},
title = {Timestamps in key distribution protocols},
journal = {Communications of the ACM},
volume = 24,
number = 8,
pages = {533--536},
month = aug,
year = 1981
}
@inproceedings{GuttmanEtAl04,
author = {Joshua D. Guttman and F. Javier Thayer and Jay A. Carlson and Jonathan C. Herzog and John D. Ramsdell and Brian T. Sniffen},
title = {Trust management in strand spaces: A rely-guarantee method},
booktitle = {In Proc. of the European Symposium on Programming (ESOP ’04), LNCS},
year = 2004,
pages = {325--339},
publisher = {Springer-Verlag}
}
@Misc{Ramsdell12,
author = {John D. Ramsdell},
title = {Deducing Security Goals from Shape Analysis Sentences},
howpublished = {The MITRE Corporation},
month = apr,
year = 2012,
note = {\url{http://arxiv.org/abs/1204.0480}}}
@TechReport{Ramsdell13,
title = {Proving Security Goals With Shape Analysis Sentences},
author = {John D.~Ramsdell},
institution = {The MITRE Corporation},
year = 2013,
month = sep,
number = {MTR130488},
note = {\url{http://arxiv.org/abs/1403.3563}},
}
@Misc{RamsdellEtAl14,
author = {John D. Ramsdell and Daniel J. Dougherty and
Joshua D. Guttman and Paul D. Rowe},
title = {A Hybrid Analysis for Security Protocols with State},
howpublished = {The MITRE Corporation and Worcester Polytechnic Institute},
month = apr,
year = 2014,
note = {\url{http://arxiv.org/abs/1404.3899}}}
@TechReport{RamsdellEtAl09,
author = {John D. Ramsdell and Joshua D. Guttman and
Jonathan K. Millen and Brian O'Hanlon},
title = {An Analysis of the {CAVES} Attestation Protocol using {CPSA}},
note = {\url{http://arxiv.org/abs/1207.0418}},
institution = {The {MITRE} Corporation},
month = dec,
year = 2009,
type = {{MITRE} Technical Report},
number = {{MTR090213}}
}
@InProceedings{GuttmanLiskovRowe14,
author = {Joshua D. Guttman and Moses D. Liskov and Paul D. Rowe},
title = {Security Goals and Evolving Standards},
booktitle = {Security Standardization Research},
year = 2014,
editor = {Liqun Chen and Chris Mitchell},
volume = 8839,
series = {LNCS},
pages = {93--110},
month = dec,
publisher = {Springer},
}
@Article{Guttman14,
author = {Joshua D. Guttman},
title = {Establishing and Preserving Protocol Security Goals},
journal = {Journal of Computer Security},
year = 2014,
volume = 22,
number = 2,
pages = {201--267}}
@Unpublished{prover9,
author = {Bill W. McCune},
title = {Prover9},
note = {\url{http://www.cs.unm.edu/~mccune/mace4/}},
OPTkey = {},
OPTmonth = {},
OPTyear = {},
OPTannote = {}
}
@InProceedings{LiskovThayer14,
author = {Moses D. Liskov and F. Javier Thayer},
title = {Modeling Diffie-Hellman Derivability for Automated Analysis},
OPTcrossref = {},
OPTkey = {},
booktitle = {Computer Security Foundations},
year = 2014,
OPTeditor = {},
OPTvolume = {},
number = 27,
OPTseries = {},
OPTpages = {},
month = jul,
OPTaddress = {},
organization = {{IEEE}},
OPTpublisher = {},
note = {\url{http://www.mitre.org/sites/default/files/publications/PR_13-2517.pdf}},
OPTannote = {}
}