@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{http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf‎}}}

@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{http://hackage.haskell.org/package/cpsa} 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{http://hackage.haskell.org/package/cpsa} 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{http://hackage.haskell.org/package/cpsa} 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{http://hackage.haskell.org/package/cpsa} 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{http://hackage.haskell.org/package/cpsa} source
    distribution, \texttt{doc} directory},
  OPTannote = 	 {}
}

@InCollection{cpsa09,
  author = 	 {John D. Ramsdell and Joshua D. Guttman},
  title = 	 {{CPSA}: A cryptographic protocol shapes analyzer},
  booktitle = 	 {Hackage},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  publisher =    {The MITRE Corporation},
  year = 	 2009,
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTchapter = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  note = 	 {\url{http://hackage.haskell.org/package/cpsa}},
  OPTannote = 	 {}
}

@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.0418v1}},
  institution =  {The {MITRE} Corporation},
  month = 	 dec,
  year = 	 2009,
  type = 	 {{MITRE} Technical Report},
  number = 	 {{MTR090213}}
}