packages feed

cpsa-4.4.1: doc/src/cpsa4manual/secureprotocols.bib

@Article{Abadi98,
  author =       {Mart{\'\i}n Abadi},
  title =        {On {SDSI}'s linked Local Name Spaces},
  journal =      {Journal of Computer Security},
  year =         1998,
  volume =       6,
  number =       {1--2},
  pages =        {3--21}
}

@article{AbadiBlanchet05,
  author = {Mart{\'\i}n Abadi and Bruno Blanchet},
  title = {Analyzing Security Protocols with Secrecy Types and Logic Programs},
  journal = {Journal of the ACM},
  year = 2005,
  volume = 52,
  number = 1,
  pages = {102--146},
  month = {January}
}

@InProceedings{AbadiEtAl04,
  author =       {Mart{\'\i}n Abadi and Bruno Blanchet and C{\'{e}}dric Fournet},
  title =        {{Just Fast Keying} in the Pi Calculus},
  booktitle =    {Programming Languages and Systems: {ESOP} 2004 Proceedings},
  pages =        {340--354},
  month =        {January},
  year =         2004,
  editor =       {David Schmidt},
  number =       2986,
  series =       {LNCS},
  publisher =    {Springer Verlag}
}

@Article{AbadiEtAl93,
  author =       {Mart{\'\i}n Abadi and Michael Burrows and Butler Lampson and Gordon D. Plotkin},
  title =        {A Calculus for Access Control in Distributed Systems},
  journal =      {{ACM} Transactions on Programming Languages and Systems},
  year =         1993,
  volume =       15,
  number =       4,
  pages =        {706--34},
  month =        {September}
}

@InProceedings{FioreAbadi01,
  author =       {Marcelo Fiore and Mart{\'\i}n Abadi},
  title =        {Computing Symbolic Models for Verifying Cryptographic Protocols},
  booktitle = {Computer Security Foundations Workshop},
  year =         2001,
  month =        {June}}

@InProceedings{AbadiFournet01,
  author =       {Mart{\'\i}n Abadi and C{\'{e}}dric Fournet},
  title =        {Mobile Values, New Names, and Secure Communication},
  booktitle =    {28th ACM Symposium on Principles of Programming Languages ({POPL} '01)},
  pages =        {104--115},
  year =         2001,
  month =        {January}
}

@article{AbadiJurjens01,
    author = "Mart{\'\i}n Abadi and Jan J{\"u}rjens",
    title = "Formal Eavesdropping and Its Computational Interpretation",
    journal = "Lecture Notes in Computer Science",
    volume = "2215",
    pages = "82ff.",
    year = "2001",
    url = "http://citeseer.nj.nec.com/abadi00formal.html" }

@misc{AbadiJurjens00,
  title=        {Formal Eavesdropping and its Computational Interpretation},
  author=       {Mart{\'{\i}}n Abadi and Jan J{\"u}rjens},
  year=         2000,
  note=         {submitted for publication},
}

@Article{AbadiRogaway02,
  author =       {Mart{\'\i}n Abadi and Phillip Rogaway},
  title =        {Reconciling two views of cryptography (The
                  computational soundness of formal encryption)},
  journal =      {Journal of Cryptology},
  year =         2002,
  volume =       15,
  number =       2,
  pages =        {103--127}}

@InProceedings{AbadiRogaway00,
  author =       {Mart\'{\i}n Abadi and Phillip Rogaway},
  title =        {Reconciling two views of cryptography (The computational soundness of formal encryption)},
  booktitle =    {IFIP
International Conference on Theoretical Computer Science (IFIP TCS2000)},
  year =         2000,
  series =       {Lecture Notes in Computer Science},
  publisher =    {Springer-Verlag}
}

@InProceedings{AbadiGordon97,
  author =       {Mart\'{\i}n Abadi and Andrew D. Gordon},
  title =        {A Calculus for Cryptographic Protocols: The Spi Calculus},
  booktitle =    {4th ACM Conference on Computer and Communications Security},
  pages =        {36--47},
  year =         1997,
  month =        {April},
  publisher =    {ACM Press},
  annote =       {From URL http://www.research.digital.com/SRC}
}

@Article{AbadiGordon99,
  author =       {Mart\'{\i}n Abadi and Andrew D. Gordon},
  title =        {A Calculus for Cryptographic Protocols: The Spi Calculus},
  journal =      {Information and Computation},
  year =         1999,
  volume =       148,
  number =       1,
  pages =        {1--70},
  month =        {January}
}

@InProceedings{AbadiGordon97a,
  author =       {Mart\'{\i}n Abadi and Andrew D. Gordon},
  title =        {Reasoning about cryptographic protocols in the spi calculus},
  booktitle =    {CONCUR 97},
  pages =        {59--73},
  year =         1997,
  series =       {Lecture Notes in Computer Science},
  month =        {July},
  publisher =    {Springer-Verlag}
}

@InProceedings{AbadiNeedham94,
  author =       {Mart\'{\i}n Abadi and Roger Needham},
  title =        {Prudent Engineering Practice for Cryptographic Protocols},
  booktitle =    {Proceedings, 1994 IEEE Symposium on Research in
                  Security and Privacy},
  year =         1994,
  organization = {{\sc ieee}},
  publisher =    {{\sc ieee} CS Press},
  pages =        {122--136}
}

@InProceedings{AbadiTuttle91,
  author =       {Mart\'{\i}n Abadi and Mark R. Tuttle},
  title =        {A Semantics for a Logic of Authentication},
  booktitle =    {Proceedings of the 10th {ACM} Symposium on Principles of Distributed Computing},
  pages =        {201--216},
  year =         1991,
  month =        {August}
}

@book{abiteboul1994foundations,
  title={{Foundations of Databases: The Logical Level}},
  author={Abiteboul, S. and Hull, R. and Vianu, V.},
  year=1994,
  publisher={Addison Wesley}
}

@article{ables2010escrowed,
  title={Escrowed data and the digital envelope},
  author={Ables, K. and Ryan, M.},
  journal={Trust and Trustworthy Computing},
  pages={246--256},
  year={2010},
  publisher={Springer}
}

@Article{AbrahametalIBM91,
  author =       "DG Abraham and GM Dolan and GP Double and JV Stevens",
  title =        "Transaction Security Systems",
  journal =      "IBM Systems Journal",
  year =         1991,
  volume =       30,
  number =       2,
  pages =        "206--229"
}

@Article{Adam92,
  author =       "J. Adam",
  title =        "Cryptography = Privacy?",
  journal =      "IEEE Spectrum",
  year =         1992,
  pages =        "29--35",
  month =        aug
}

@InProceedings{AdaoEtAl05,
  author =       {Pedro Ad{\~a}o and Gergei Bana and Jonathan Herzog and Andre Scedrov},
  title =        {Soundness of Formal Encryption in the Presence of Key-Cycles},
  booktitle =    {Proceedings of the 10th European Symposium On Research In Computer Security {(ESORICS 2005)}},
  year =         2005,
  month =        {September}
}

@Article{Ajluni95,
  author =       "C. Ajluni",
  title =        "Two New Imagine Techniques Promise To Improve IC Defect Identification",
  journal =      "Electronic Design",
  volume =       "43",
  number =       "14",
  month =        "July",
  year =         1995,
  pages =        "37--38"
}

@Article{Akl83,
  author =       "Selim G. Akl",
  title =        "Digital Signatures: A Tutorial Survey",
  journal =      "Computer",
  year =         1983,
  pages =        "15--24",
  month =        feb
}

@InProceedings{AmadioLugiez00,
  author =       {Roberto M. Amadio and Denis Lugiez},
  title =        {On the Reachability Problem in Cryptographic Protocols},
  booktitle = {Concur},
  pages =        {380--394},
  year =         2000,
  number =       1877,
  series =       {LNCS}}

@article{amadio2003symbolic,
  title={On the symbolic reduction of processes with cryptographic functions},
  author={Amadio, R.M. and Lugiez, D. and Vanack{\`e}re, V.},
  journal={Theoretical Computer Science},
  volume={290},
  number={1},
  pages={695--740},
  year={2003},
  publisher={Elsevier}
}

@InProceedings{AndersonKuhn96,
  author =       "Ross Anderson and M. Kuhn",
  title =        "Tamper Resistance - a Cautionary Note",
  booktitle =    "Proceedings of the Second Usenix Workshop on Electronic Commerce",
  pages =        "1--11",
  year =         1996
}

@InProceedings{AndersonKuhn97,
  author =       "Ross Anderson and Markus Kuhn",
  title =        "Low Cost Attacks on Tamper Resistant Devices",
  booktitle =    "{IWSP}: International Workshop on Security Protocols, {LNCS}",
  year =         "1997"
}

@Article{AndersonNeedham,
  author =       "R. Anderson and R. Needham",
  title =        "Programming Satan's Computer",
  journal =      "Computer Science Today: Lecture Notes in Computer Science",
  volume =       "1000",
  year =         1995,
  pages =        "426--441"
}
 @Article{ACGMMR2006composing,
 title = {Sufficient Conditions for Composing Security Protocols},
 author = {S. Andova and C.J.F. Cremers and K. Gj{\o}steen and S. Mauw
                  and S.F. Mj{\o}lsnes and S. Radomirovi\'{c}},
 booktitle = {Special issue on Computer Security: Foundations and Automated Reasoning},
 journal = {Information and Computation},
 volume={206},
 number={2},
 pages={425--459},
 year = 2008
}

@article{ankney1995unified,
  title={{The Unified Model}. Contribution to {ANSI X9F1}},
  author={Ankney, R. and Johnson, D. and Matyas, M.},
  journal={Standards Projects (Financial Crypto Tools), ANSI X},
  volume={42},
  year={1995}
}

@Article{AnsonMitchell90,
  author =       "Colin l'Anson and Chris Mitchell",
  title =        "Security Defects in the CCITT Recommendation {X}.509 ---
                  The Directory Authentication Framework",
  journal =      "Computer Communication Review",
  year =         1990,
  volume =       20,
  number =       2,
  pages =        "30-34",
  month =        apr
}

@inproceedings{Anteniese99,
 author = {Ateniese, Giuseppe},
 title = {Efficient verifiable encryption (and fair exchange) of digital signatures},
 booktitle = {CCS '99: Proceedings of the 6th ACM conference on Computer and communications security},
 year = {1999},
 isbn = {1-58113-148-8},
 pages = {138--146},
 location = {Kent Ridge Digital Labs, Singapore},
 doi = {http://doi.acm.org/10.1145/319709.319728},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@InProceedings{AppelFelten99,
  author =       {Andrew W. Appel and Edward W. Felten},
  title =        {Proof-Carrying Authentication},
  booktitle =    {6th {ACM} Conference on Computer and Communications Security},
  year =         1999,
  month =        {November}
}

@InProceedings{ArapinisEtAl2011,
  author =       {Myrto Arapinis and Mark Ryan and Eike Ritter},
  title =        {{StatVerif}: Verification of Stateful Processes},
  booktitle = {{IEEE} Symposium on Computer Security Foundations},
  year =         2011,
  month =        {June},
  publisher = {{IEEE CS} Press}}

@Book{AristotleNE,
  author =       {Aristotle},
  title =        {Nicomachean Ethics},
  publisher =    {Oxford University Press},
  year =         1953
}

@Misc{ASN1,
  author =       {ISO},
  title =        {Abstract Syntax Notation One ({ASN.1})},
  howpublished = {ISO/IEC 8824}
}

@article{AsokanEtAl00,
  title={Optimistic fair exchange of digital signatures},
  author={N. Asokan and Victor Shoup and Michael Waidner},
  journal={{IEEE} J. Sel.~Areas in Comms.},
  volume=18,
  number=4,
  pages={593--610},
  year=2000
}

@InProceedings{AsokanEtAl97,
  author =       {N. Asokan and Matthias Schunter and Michael Waidner},
  title =        {Optimistic Protocols for Fair Exchange},
  booktitle = {4th Conference on Computer and Communications Security ({CCS})},
  pages =        {6--17},
  year =         1997,
  publisher = {{ACM}}}

@Misc{rfc1826,
  OPTkey =       {},
  author =       {R. Atkinson},
  title =        {{IP} Authentication Header},
  howpublished = {Internet Request for Comments 1826},
  year =         {1995},
  month =        {August},
  note =         {Available at \texttt{http://ds.internic.net/rfc/rfc1826.txt}.},
  OPTannote =    {}
}

@article{ax1968elementary,
  title={{The elementary theory of finite fields}},
  author={Ax, J.},
  journal={The Annals of Mathematics},
  volume={88},
  number={2},
  pages={239--271},
  issn={0003-486X},
  year={1968},
  publisher={JSTOR}
}

@InProceedings{BackesEtAl02,
  author =       {Michael Backes and Christian Jacobi and Birgit Pfitzmann},
  title =        {Deriving Cryptographically Sound Implementations
                  Using Composition and Formally Verified Bisimulation},
  booktitle =    {Formal Methods Europe '02 (FME)},
  pages =        {310--329},
  year =         2002,
  series =       {LNCS},
  volume =       2391,
  publisher =    {Springer Verlag}
}

@InProceedings{BackesPfitzmann05,
  author =       {Michael Backes and Birgit Pfitzmann},
  title =        {Relating Cryptographic and Symbolic Key Secrecy},
  booktitle = {Proceedings, 26th {IEEE} Symposium on Security and Privacy},
  year =         2005,
  month =        {May},
  note =         {Extended version,
                  \url{http://eprint.iacr.org/2004/300}}}

@InProceedings{BackesEtAl08,
  author =       {Michael Backes and Matteo Maffei and Dominique Unruh},
  title =        {Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the {Direct Anonymous Attestation} Protocol},
  booktitle = {{IEEE} Symposium on Security and Privacy},
  year =         2008}

@inproceedings{MaffeiEtAl07,
 author = {Michael Backes and Agostino Cortesi and Riccardo Focardi and Matteo Maffei},
 title = {A calculus of challenges and responses},
 booktitle = {FMSE '07: ACM Workshop on Formal methods in Security Engineering},
 year = 2007,
 isbn = {978-1-59593-887-9},
 pages = {51--60},
 location = {Fairfax, Virginia, USA},
 doi = {http://doi.acm.org/10.1145/1314436.1314444},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@Misc{rfc1827,
  OPTkey =       {},
  author =       {R. Atkinson},
  title =        {{IP} Encapsulating Security Payload {(ESP)}},
  howpublished = {Internet Request for Comments 1827},
  year =         {1995},
  month =        {August},
  note =         {Available at \texttt{http://ds.internic.net/rfc/rfc1827.txt}.},
  OPTannote =    {}
}

@InProceedings{BartalEtAl99,
  author =       {Yair Bartal and Alain Mayer and Kobbi Nissim and Avishai Wool},
  title =        {Firmato: A Novel Firewall Management Toolkit},
  booktitle =    {Proceedings, {IEEE} Symposium on Security and Privacy},
  year =         1999,
  month =        {May},
  publisher =    {IEEE CS Press}
}

@inproceedings{BasinEtAl05,
  author    = {A. Armando and
               D. A. Basin and
               Y. Boichut and
               Y. Chevalier and
               L. Compagna and
               J. Cu{\'e}llar and
               P. Hankes Drielsma and
               P.-C. H{\'e}am and
               O. Kouchnarenko and
               J. Mantovani and
               S. M{\"o}dersheim and
               D. von Oheimb and
               M. Rusinowitch and
               J. Santiago and
               M. Turuani and
               L. Vigan{\`o} and
               L. Vigneron},
  title     = {The {AVISPA} Tool for the Automated Validation of Internet
               Security Protocols and Applications},
  booktitle = {CAV},
  year      = {2005},
  pages     = {281--285},
  ee        = {http://dx.doi.org/10.1007/11513988_27},
  crossref  = {DBLP:conf/cav/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/ijisec/BasinMV05,
  author    = {David A. Basin and
               Sebastian M{\"o}dersheim and
               Luca Vigan{\`o}},
  title     = {{OFMC}: A symbolic model checker for security protocols},
  journal   = {Int. J. Inf. Sec.},
  volume    = {4},
  number    = {3},
  year      = {2005},
  pages     = {181-208},
  ee        = {http://dx.doi.org/10.1007/s10207-004-0055-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{CaleiroEtAl2005,
  title={{Relating strand spaces and distributed temporal logic for security protocol analysis}},
  author={Caleiro, C. and Vigano, L. and Basin, D.},
  journal={Logic Journal of IGPL},
  volume={13},
  number={6},
  pages={637},
  year={2005},
  publisher={Oxford Univ Press}
}

@proceedings{DBLP:conf/cav/2005,
  editor    = {Kousha Etessami and
               Sriram K. Rajamani},
  title     = {Computer Aided Verification, 17th International Conference,
               CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3576},
  year      = {2005},
  isbn      = {3-540-27231-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{BeckerSewell04,
  author =       {Moritz Y. Becker and Peter Sewell},
  title =        {Cassandra: Flexible Trust Management, Applied to Electronic Health Records},
  booktitle =    {17th Computer Security Foundations Workshop},
  pages =        {139--154},
  year =         2004,
  address =      {Asilomar, CA},
  month =        {June},
  publisher =    {{IEEE CS} Press}
}

@TechReport{BellLaPadula75,
  author =       {David E. Bell and Leonard J. LaPadula},
  title =        {Computer Security Model:  Unified Exposition and {Multics} Interpretation},
  institution =  {ESD},
  year =         1975,
  number =       {75-306},
  month =        {June}
}

@TechReport{BellaEtAl01,
  author =       {Giampaolo Bella and Fabio Massacci and Lawrence C. Paulson},
  title =        {Verifying the {SET} Purchase Protocols},
  institution =  {Cambridge University Computer Laboratory},
  year =         {2001},
  OPTkey =       {},
  OPTtype =      {Report},
  OPTnumber =    {524},
  OPTaddress =   {},
  OPTmonth =     {November},
  note =         {Short version appeared in International Joint Conference on Automated Reasoning, June, 2001.  Available at http://www.cl.cam.ac.uk/\-users/\-lcp/\-papers/\-protocols.html},
  OPTannote =    {}
}

@InProceedings{Bellare98,
  author =       {Mihir Bellare},
  title =        {Practice-Oriented Provable Security},
  booktitle =    {First International Workshop on Information Security ({ISW} 97)},
  year =         1998,
  editor =       {E. Okamoto and G. Davida and M. Mambo},
  volume =       1396,
  series =       {LNCS},
  publisher =    {Springer Verlag}
}

@InProceedings{BellareKillianRogaway94,
  author =       {Mihir Bellare and J. Killian and Phillip Rogaway},
  title =        {The Security of Cipher Block Chaining},
  booktitle =    {Advances in Cryptology --- Crypto 94},
  year =         1994,
  editor =       {Yvo Desmedt},
  volume =       839,
  series =       {LNCS},
  publisher =    {Springer Verlag}
}

@InProceedings{BellareRogaway93,
  author =       {Mihir Bellare and Phillip Rogaway},
  title =        {Entity Authentication and Key Distribution},
  booktitle =    {Advances in Cryptology -- Crypto '93 Proceedings},
  year =         1993,
  number = 773,
  series = {LNCS},
  publisher =    {Springer-Verlag}
}

@InProceedings{BellareRogaway93a,
  author =       {Mihir Bellare and Phillip Rogaway},
  title =        {Random Oracles are Practical: a paradigm for designing efficient protocols},
  booktitle =    {Proceedings, {ACM} Conference on Communications and Computer Security},
  year =         1993,
  pages =        "62--73",
  publisher =    {{ACM}},
  note =         {Full version available at http://www-cse.ucsd.edu/users/mihir/papers/}
}

@Article{BellerChangYacobi93,
  author =       "Michael J. Beller and Li-Fung Chang and Yacov Yacobi",
  title =        "Privacy and Authentication on a Portable
                  Communications System",
  journal =      "Journal on Selected Areas in Communications",
  year =         1993,
  volume =       11,
  number =       6,
  pages =        "821--829",
  month =        aug
}

@Article{BellovinMerrit90,
  author =        "S. M. Bellovin and M. Merrit",
  title =        "Limitations of the {Kerberos} Authentication System",
  journal =      "Computer Communication Review",
  year =         1990,
  volume =       20,
  number =       5,
  pages =        "119--132",
  month =        oct,
}

@InProceedings{BellovinMerrit92,
  author =       "S. M. Bellovin and M. Merrit",
  title =        "Encrypted Key Exchange: Password based protocols
                  secure against dictionary attacks",
  pages =        "72--84",
  booktitle =    "Proceedings 1992 IEEE Symposium on Research in
                  Security and Privacy",
  year =         1992,
  publisher =    "IEEE CS",
  month =        may
}

@InProceedings{Bellovin96,
  author =       {Steven Bellovin},
  title =        {Problem Areas for the {IP} Security Protocols},
  booktitle =    {Proceedings of the Sixth USENIX {UNIX} Security Symposium},
  year =         1996,
  month =        {July},
  note =         {Also at ftp://ftp.research.att.com/dist/smb/badesp.ps}
}

@Article{BessonEtAl01,
  author =       {F. Besson and T. Jensen and D. L. M{\'e}tayer and T. Thorn},
  title =        {Model Checking Security Properties of Control Flow Graphs},
  journal =      {Journal of Computer Security},
  year =         2001,
  volume =       9,
  pages =        {217--250}
}

@inproceedings{DBLP:conf/lpar/BezemC05,
  author    = {Marc Bezem and
               Thierry Coquand},
  title     = {Automating Coherent Logic},
  booktitle = {{LPAR}, Logic for Programming, Artificial Intelligence,
                  and Reasoning},
  year      = 2005,
  pages     = {246-260},
  series    = {Lecture Notes in Computer Science},
  volume    = 3835,
  ee        = {http://dx.doi.org/10.1007/11591191_18},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/lpar/2005,
  editor    = {Geoff Sutcliffe and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning,
               12th International Conference, LPAR 2005, Montego Bay, Jamaica,
               December 2-6, 2005, Proceedings},
  booktitle = {LPAR},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3835},
  year      = {2005},
  isbn      = {3-540-30553-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{Bieber90,
  author =       "P. Bieber",
  title =        "A Logic of Communication in a Hostile Environment",
  pages =        "14--22",
  booktitle =    "Proceedings of the Computer Security Foundations
                  Workshop III",
  year =         1990,
  publisher =    "IEEE CS Press"
}

@Article{BihamShamir91a,
author =       "E. Biham and A. Shamir",
title =        "Differential Cryptanalysis of DES-like Cryptosystems",
OPTcrossref =  "",
OPTkey =       "",
OPTjournal =   "Advances in Cryptology -- Proceedings of CRYPTO
'90",
OPTyear =      "1991",
OPTvolume =    "",
OPTnumber =    "",
OPTpages =     "3--72",
OPTmonth =     "",
OPTnote =      "",
OPTannote =    ""
}

@Article{BihamShamir97,
  author =       "Eli Biham and Adi Shamir",
  title =        "Differential Fault Analysis of Secret Key Cryptosystems",
  journal =      "Lecture Notes in Computer Science",
  volume =       "1294",
  year =         "1997"
}

@InProceedings{BirdGopalHerzbergJansonKuttenMolvaYung91,
  author =       "R. Bird and I. Gopal and A. Herzberg and P. A.
                  Janson and S. Kutten and R. Mulva and M. Yung",
  title =        "Systematic Design of Two-Party Authentication Protocols",
  editor =       "J. Feigenbaum",
  series =       "Lecture Notes in Computer Science",
  number =       576,
  pages =        "44--61",
  booktitle =    "Proceedings of Crypto '91: Advances in Cryptology ",
  year =         1991,
  publisher =    "Springer Verlag"
}

@Article{BirdGopalHerzbergJansonKuttenMolvaYung93,
  author =       "R. Bird and I. Gopal and A. Herzberg and P. A.
                  Janson and S. Kutten and R. Mulva and M. Yung",
  title =        "Systematic Design of a Family of Attack-Resistant
                  Authentication protocols",
  journal =      "IEEE Journal on Selected Areas in Communications",
  year =         1993,
  volume =       11,
  number =       5,
  pages =        "679--693"
}

@Article{Birrell85,
  author =       "A. D. Birrell",
  title =        "Secure Communication using Remote Procedure Calls",
  journal =      "ACM Transactions on Operating Systems",
  year =         1985,
  volume =       3,
  number =       1,
  pages =        "1--14",
  month =        feb
}

@InProceedings{Blakely79,
  author =       "G. R. Blakely",
  title =        "Safeguarding Cryptographic Keys.",
  pages =        "313--317",
  booktitle =    "Proceedings AFIPS 1979 National Computer Conference",
  year =         1979,
  publisher =    AFIPS
}

@InProceedings{Blanchet01,
  author =       {Bruno Blanchet},
  title =        {An Efficient Protocol Verifier based on {Prolog} Rules},
  booktitle =    {14th Computer Security Foundations Workshop},
  pages =        {82--96},
  year =         2001,
  month =        {June},
  publisher =    {IEEE CS Press}
}

@InProceedings{Blanchet02,
  author =       {Bruno Blanchet},
  title =        {From Secrecy to Authenticity in Security Protocols},
  booktitle =    {9th Static Analysis Symposium},
  pages =        {342--359},
  number =       2477,
  series =       {LNCS},
  month =        {September},
  year =         2002,
  publisher =    {Springer Verlag}
}

@INPROCEEDINGS{Blanchet04,
  title={Automatic proof of strong secrecy for security protocols},
  author={Blanchet, B.},
  booktitle={Security and Privacy, 2004. Proceedings. 2004 IEEE Symposium on},
  year=2004,
  month={May},
  publisher =    {IEEE CS Press},
  pages={ 86-100} }

@PHDTHESIS{Blanchet08,
  AUTHOR = {Bruno Blanchet},
  TITLE = {V\'{e}rification automatique de protocoles cryptographiques:  mod{\`e}le formel et mod{\`e}le calculatoire. Automatic verification of security protocols: formal model and computational model},
  SCHOOL = {Universit{\'e} Paris-Dauphine},
  YEAR = 2008,
  TYPE = {M\'{e}moire d'habilitation \`{a} diriger des recherches},
  MONTH = NOV,
  NOTE = {En fran\c{c}ais avec publications en anglais en annexe. In French with publications in English in appendix.}
}

@InProceedings{BlanchetPodelski03,
  author =       {Bruno Blanchet and Andreas Podelski},
  title =        {Verification of Cryptographic Protocols:  Tagging Enforces Termination},
  booktitle =    {Foundations of Software Science and Computation Structures},
  pages =        {136--152},
  year =         2003,
  series =       {LNCS},
  month =        {April}
}

@InProceedings{Boebert85,
  author =       "W. E. Boebert and R. Y. Kain",
  title =        "A Practical Alternative to Hierarchical Integrity Policies",
  booktitle =    "Proceedings of the Eighth National Computer Security Conference",
  year =         1985
}

@InProceedings{BlazeEtAl97,
  author =       {Matt Blaze and Joan Feigenbaum and Jack Lacy},
  title =        {Distributed Trust Management},
  booktitle =    {Proceedings, 1996 {IEEE} Symposium on Security and Privacy},
  pages =        {164--173},
  year =         1997,
  month =        {May}
}

@Misc{BlazeEtAl99,
  author =       {Matt Blaze and Joan Feigenbaum and John Ioannidis and Angelos D. Keromytis},
  title =        {The {KeyNote} Trust Management System, version 2},
  howpublished = {{IETF RFC} 2704},
  month =        {September},
  year =         1999
}

@Article{BonehEtAl97,
  author =       "Dan Boneh and Richard A. DeMillo and Richard J. Lipton",
  title =        "On the Importance of Checking Cryptographic Protocols for Faults",
  journal =      "Lecture Notes in Computer Science",
  volume =       "1233",
  pages =        "37--51",
  year =         "1997"
}

@TechReport{BonehEtAl98,
  author =       "Bill Aiello and Dan Boneh and Matthew Franklin and Jeremy Horwitz",
  title =        "Protocols for Secure Generation of Shared {RSA} Keys",
  institution =  "Standford University",
  year =         1998,
  note =         "DARPA Contract F30602-97-C-0326, Data Item Number A007: Technical Information Report"
}

@InProceedings{Boneh98,
  author =       {Dan Boneh},
  title =        {The decision {Diffie-Hellman} problem},
  booktitle =    {Proceedings of the Third Algorithmic Number Theory Symposium},
  pages =        {48--63},
  year =         1998,
  number =       1423,
  series =       {Lecture Notes in Computer Science},
  publisher =    {Springer--Verlag}
}

@InProceedings{BonehFranklin97,
  author =       "D. Boneh and M. Franklin",
  title =        "Efficient Generation of Shared RSA Keys",
  series =       "Lecture Notes in Computer Science",
  number =       1233,
  pages =        "425--439",
  booktitle =    "Proceedings of Crypto '97",
  year =         1997,
  publisher =    "Springer Verlag"
}

@InProceedings{Boreale01,
  author =       {Michele Boreale},
  title =        {Symbolic Trace Analysis of Cryptographic Protocols},
  booktitle =    {{ICALP}},
  year =         2001
}

@InProceedings{Bovenlander,
  author =       "E. Bovenlander and RL van Renesse",
  title =        "Smartcards and Biometrics: An Overview",
  booktitle =    "Computer Fraud and Security Bulletin",
  year =         "1995",
  pages =        "8--12"
}

@Article{Boyd90,
  author =       "Colin Boyd",
  title =        "Hidden Assumptions in Cryptographic Protocols",
  journal =      "Proceedings of the IEE",
  year =         1990,
  volume =       "137 Pt E",
  number =       6,
  pages =        "433--436",
  month =        nov,
}

@InProceedings{Boyd92,
  author =       "C. Boyd",
  title =        "A Formal Framework for Authentication",
  pages =        "273--292",
  booktitle =    "Proceedings ESORICS 92",
  editor =       "Y. Deswarte and G. Eizenberg and J.-J. Quisquater",
  publisher =    "Springer LNCS 648",
  year =         "1992",
}

@InProceedings{BoydMao94a,
  title =        "Designing Secure Key Exchange Protocols",
  year =         1994,
  pages =        "93--106",
  editor =       "Dieter Gollmann",
  booktitle=     "Computer Security---{ESORICS} '94",
  author =       "Colin Boyd and Wenbo Mao",
  publisher =    "Springer-Verlag"
}

@InProceedings{BraceEtAl90,
  author =       {Karl S. Brace and Richard L. Rudell and Randal E. Bryant},
  title =        {Efficient Implementation of a {BDD} Package},
  booktitle =    {27th {ACM/IEEE} Design Automation Conference},
  pages =        {40--45},
  year =         1990
}

@InProceedings{BrickellCamenischChen04,
  author =       {Ernie Brickell and Jan Camenisch and Liqun Chen},
  title =        {Direct Anonymous Attestation},
  booktitle = {ACM Conference on Communications and Computer Security ({CCS})},
  year =         2004,
  note =         {Full version available at \url{http://eprint.iacr.org/2004/205}}}

@Article{BrickellOdlyzko88,
  author =       "E. F. Brickell and A. M. Odlyzko",
  title =        "Cryptanalysis: A Survey of Recent Results",
  journal =      "Proceedings of the IEEE",
  year =         1988,
  volume =       76,
  number =       5,
  month =        may
}

@InProceedings{BroadfootLowe03,
  author =       {Philippa Broadfoot and Gavin Lowe},
  title =        {On Distributed Security Transactions that use Secure Transport Protocols},
  booktitle =    {Proceedings, 16th Computer Security Foundations Workshop},
  pages =        {63--73},
  year =         2003,
  publisher =    {{IEEE} {CS} Press}
}

@Article{Bryant86,
  author =       {Randal E. Bryant},
  title =        {Graph-Based Algorithms for Boolean Function Manipulation},
  journal =      {IEEE Transactions on Computers},
  year =         1986,
  volume =       {C-35},
  number =       8,
  pages =        {677--691},
  month =        {August}
}

@Article{BurrowsAbadiNeedham89,
  author =       {Michael Burrows and Mart\'{\i}n Abadi and Roger Needham},
  title =        {A Logic of Authentication},
  journal =      {Proceedings of the Royal Society},
  year =         1989,
  volume =       {Series A, 426},
  number =       1871,
  pages =        {233--271},
  month =        {December},
  OPTnote =      {Also appeared as SRC Research Report 39 and, in a shortened form, in ACM Transactions on Computer
Systems 8, 1 (February 1990), 18-36. }
}

@TechReport{BurrowsAbadiNeedham89a,
  author =       "Michael Burrows and Mart\'{\i}n Abadi and Roger Needham",
  title =        "A Logic of Authentication",
  institution =  "Digital Systems Research Center",
  year =         1989,
  type =         "Technical Report",
  number =       39,
  month =        feb
}

@Article{BurrowsAbadiNeedham90,
  author =       "Michael Burrows and Mart\'{\i}n Abadi and Roger M. Needham",
  title =        "Rejoinder to {Nessett}",
  journal =      "ACM Operating Systems Review",
  year =         1990,
  volume =       24,
  number =       2,
  pages =        "39--40",
  month =        apr
}

@TechReport{BurrowsAbadiNeedham94,
  author =       "Michael Burrows and Mart\'{\i}n Abadi and Roger M. Needham",
  title =        "The Scope of a Logic of Authentication",
  institution =  "Digital Systems Research Center",
  year =         1994,
  type =         "Revised Research Report",
  number =       39
}

@InProceedings{ButtyanEtAl98,
  author =       {Levente Butty{\'a}n and Sebastian Staamann and Uwe Wilhelm},
  title =        {A Simple Logic for Authentication Protocol Design},
  booktitle =    {11th {IEEE} Computer Security Foundations Workshop},
  pages =        {153--162},
  year =         1998
}

@Manual{CCITTX509,
  title =        "The Directory-Authentication Framework",
  author =       "{C. C. I. T. T. Recommendation X.509}",
  organization = "C. C. I. T. T.",
  year =         1988,
  month =        dec,
}

@InProceedings{CampbellSafavi-NainiPleasants92,
  author =       "E. A. Campbell and R. Safavi-Naini and P. A. Pleasants",
  title =        "Partial Belief and Probabilistic Reasoning in the
                  Analysis of Secure Protocols",
  pages =        "84--91",
  booktitle =    "Proceedings 5th IEEE Computer Security Foundations Workshop",
  year =         1992,
  publisher =    "IEEE CS Press"
}

@TechReport{Canetti01,
  author =       {Ran Canetti},
  title =        {Universally Composable Security: A New Paradigm for
                  Cryptographic Protocols},
  institution =  {IACR},
  year =         2001,
  number =       {2000/067},
  month =        Oct,
  note =         {Appeared in FOCS, 2001},
  online =       {http://eprint.iacr.org/2000/067.ps.gz},
}

@InProceedings{CanettiHerzog06,
  author =       {Ran Canetti and Jonathan Herzog},
  title =        {Universally composable symbolic analysis of mutual authentication and key exchange protocols},
  booktitle = {Proceedings, Theory of Cryptography Conference (TCC)},
  year =         2006,
  month =        {March}}

@InProceedings{CanettiKrawczyk01,
  title={Analysis of key-exchange protocols and their use for building secure channels},
  author={Canetti, R. and Krawczyk, H.},
  booktitle={Advances in Cryptology—EUROCRYPT 2001},
  pages={453--474},
  series =       {LNCS},
  year={2001},
  publisher={Springer}
}

@InProceedings{CanettiKrawczyk02,
  author =       {Ran Canetti and Hugo Krawczyk},
  title =        {Universally Composable Notions of Key Exchange and
                  Secure Channels},
  booktitle =    {Eurocrypt 2002},
  pages =        {337--351},
  series =       {LNCS},
  publisher =    {Springer Verlag},
  year =         2002
}

@InProceedings{CarboneEtAl03,
  author =       {Marco Carbone and Mogens Nielsen and Vladimiro Sassone},
  title =        {A Formal Model for Trust in Dynamic Networks},
  booktitle =    {International Conference on Software Engineering and Formal Methods},
  year =         2003,
  editor =       {Antonio Cerone},
  month =        {September},
  publisher =    {{IEEE CS} Press}
}

@inproceedings{CarboneEtAl07,
  author    = {Marco Carbone and
               Kohei Honda and
               Nobuko Yoshida},
  title     = {Structured Communication-Centred Programming for Web Services},
  booktitle = {Programming Languages and Systems, 16th European
                  Symposium on Programming, ESOP 2007},
  year      = 2007,
  pages     = {2-17},
  ee        = {http://dx.doi.org/10.1007/978-3-540-71316-6_2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{Carlsen94a,
  author =       "Ulf Carlsen",
  title =        "Cryptographic Protocol Flaws",
  booktitle =    "Proceedings 7th IEEE Computer Security Foundations Workshop",
  publisher =    "IEEE CS",
  year =         1994,
  pages =        "192--200"
}

@InProceedings{Carlsen94b,
  author =       "Ulf Carlsen",
  title =        "Generating Formal Cryptographic Protocol Specifications",
  booktitle =    "Proceedings 7th IEEE Computer Security Foundations Workshop",
  year =         1994,
  organization = "IEEE CS Press"
}

@Article{Carlsen94c,
  author =       "Ulf Carlsen",
  title =        "Optimal Privacy and Authentication on a Portable
                  Communications System",
  journal =      "Operating Systems Review",
  year =         1994,
  volume =       28,
  number =       3,
  pages =        "16--23"
}

@Article{CarterWegman79,
  author =       {J. Lawrence Carter and Mark N. Wegman},
  title =        {Universal Classes of Hash Functions},
  journal =      {Journal of Computer and System Sciences},
  year =         1979,
  volume =       18,
  pages =        {143--54}
}

@Article{WegmanCarter81,
  author =       {Mark N. Wegman and J. Lawrence Carter},
  title =        {New Hash Functions and Their Use in Authentication and Set Equality},
  journal =      {Journal of Computer and System Sciences},
  year =         1981,
  volume =       22,
  pages =        {265--79}
}

@InProceedings{CederquistEtAl07,
  author =       {Jan Cederquist and Mohammad Torabi Dashti and Sjouke Mauw},
  title =        {A Certified Email Protocol using Key Chains},
  booktitle = {Advanced Information Networking and Applications
                  Workshops/Symposia {(AINA'07)}, Symposium on
                  Security in Networks and Distributed Systems
                  {(SSNDS07)}},
  pages =        {525--530},
  year =         2007,
  volume =       1,
  publisher = {IEEE CS Press}}

@InProceedings{MitchellEtAl99,
  author =       {I. Cervesato and N. A. Durgin and P. D. Lincoln and J. C. Mitchell and A. Scedrov},
  title =        {A Meta-Notation for Protocol Analysis},
  booktitle =    {Proceedings, 12th {IEEE} Computer Security Foundations Workshop},
  year =         1999,
  month =        {June},
  publisher =    {{IEEE} CS Press}
}

@InProceedings{CervesatoEtAl00,
  author =       {I. Cervesato and N. A. Durgin and P. D. Lincoln and J. C. Mitchell and A. Scedrov},
  title =        {Relating Strands and Multiset Rewriting for Security Protocol Analysis},
  booktitle =    {Proceedings, 13th {IEEE} Computer Security Foundations Workshop},
  year =         2000,
  month =        {July},
  publisher =    {{IEEE} CS Press}
}

@Article{CeriGottlobTanca89,
  author =       "Stefano Ceri and Georg Gottlob and Letizia Tanca",
  title =        "What You Always Wanted to Know About Datalog (And Never Dared to Ask)",
  journal =      "IEEE Transactions of Knowledge and Data Engineering",
  year =         1989,
  volume =       1,
  number =       1
}

@InProceedings{ChadhaEtAl01,
  author =       {Rohit Chadha and Max Kanovich and Andr{\'e} Scedrov},
  title =        {Inductive Methods and Contract-Signing Protocols},
  booktitle =    {Proceedings, 8th {ACM} Conference on Computer and Communications Security},
  pages =        {176--185},
  year =         2001,
  editor =       {Pierangela Samarati},
  address =      {New York},
  month =        {November},
  publisher =    {{ACM} Press}
}

@InProceedings{ChadhaEtAl03,
  author =       {Rohit Chadha and John C. Mitchell  and  Andre Scedrov and Vitaly Shmatikov},
  title =        {Contract Signing, Optimism, and Advantage},
  booktitle = {Concur --- Concurrency Theory},
  pages =        {366-382},
  year =         2003,
  series =       {LNCS},
  publisher = {Springer}}

@InProceedings{Chaum83,
  author =       "D. Chaum",
  title =        "Blind Signatures for Untraceable Payments",
  booktitle =    "Advances in Cryptology: proceedings of Crypto 82",
  pages =        "199--203",
  year =         "1983",
  publisher =    "Plenum Press"
}

@InProceedings{ChengGligor90,
  author =       "P.-C. Cheng and Virgil D. Gligor",
  title =        "On the Formal Specification and Verification of a
                  Multiparty Session Protocol",
  pages =        "216--233",
  booktitle =    "Proceedings of the IEEE 1990 Symposium on Research
                  in Security and Privacy",
  year =         1990,
  publisher =    "IEEE CS Press"
}

@Article{ChenSwiftWarren95,
  author =       "W. Chen and T. Swift and D. S. Warren",
  title =        "Efficient Top-Down Computation of Queries under the Well-Founded Semantics",
  journal =      "J. Logic Prog.",
  year =         1995,
  volume =       24,
  number =       3,
  pages =        "161--199"
}

@Article{ChenWarren96,
  author =       "W. Chen and D. S. Warren",
  title =        "Tabled Evaluation with Delaying for General Logic Programs",
  journal =      "J. ACM",
  mon =          jan,
  year =         1996,
  volume =       43,
  number =       1,
  pages =        "20--74"
}

@ARTICLE{CheinMugnier92,
    author = {Michel Chein and Marie-Laure Mugnier},
    title = {Conceptual Graphs: fundamental notions},
    journal = {Revue d'Intelligence Artificielle},
    year = {1992},
    volume = {6},
    pages = {365--406}
}

@inproceedings{CheinMugnier04,
  author    = {Michel Chein and
               Marie-Laure Mugnier},
  title     = {Concept Types and Coreference in Simple Conceptual Graphs},
  booktitle = {Conceptual Structures at Work: 12th International Conference
               on Conceptual Structures, ICCS 2004, Huntsville, AL, USA,
               July 19-23, 2004. Proceedings},
  year      = {2004},
  series    = {LNCS},
  number    = {3127},
  pages     = {303-318},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{chevalier2003deciding,
  title={{Deciding the security of protocols with {Diffie-Hellman} exponentiation and products in exponents}},
  author={Yannick Chevalier and Ralf K{\"u}sters and Micha{\"e}l
                  Rusinowitch and Mathieu Turuani},
  journal={FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science},
  pages={124--135},
  year={2003},
  publisher={Springer}
}

@InProceedings{Choretal85,
  author =       "B. Chor and S. Goldwasser and S. Micali and B. Awerbuch",
  title =        "Verifiable secret sharing and achieving simultaneity in the presence of faults",
  pages =        "383--395",
  booktitle =    "Proceedings of the 26th IEEE Symposium on Foundations of Computer Science",
  year =          1985,
  publisher =     "IEEE"
}

@Manual{CiscoCommandRef10,
  title =        {Router Products Command Reference},
  organization = {Cisco Systems},
  address =      {San Jose, CA},
  edition =      "10th",
  year =         1994,
  note =         {Chapters 10 to 17 (especially Chapter~16).  For more recent information, see~\url{http://www.cisco.com/univercd/}.}
}

@inproceedings{CiobacaCortier2010,
   author = {{\c{S}}tefan Ciob{\^a}c{\u{a}} and V{\'e}ronique Cortier},
   booktitle = {CSF},
   DOI = {10.1109/CSF.2010.29},
   month = jul,
   pages = {322-336},
   publisher = {{IEEE} Computer Society Press},
   title = {Protocol composition for arbitrary primitives},
   url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/ rr-lsv-2010-09.pdf},
   year = {2010},
}

@Article{DClarkeEtAl01,
  author =       {Dwaine Clarke and Jean-Emile Elien and Carl Ellison and Matt Fredette and Alexander Morcos and Ronald L. Rivest},
  title =        {Certificate Chain Discovery in {SPKI/SDSI}},
  journal =      {Journal of Computer Security},
  year =         2001,
  volume =       9,
  number =       4,
  pages =        {285--322}
}

@Book{ClarkeEtAl01,
  author =       {Edmund M. {Clarke, Jr.} and Orna Grumberg and Doron A. Peled},
  title =        {Model Checking},
  publisher =    {{MIT} Press},
  year =         2001
}

@Article{ClarkJacob95,
  author =       "John Clark and Jeremy Jacob",
    title =      "On The Security of Recent Protocols",
      journal =  "Information Processing Letters",
        year =   1995,
          volume =       56,
            number =     3,
              pages =    "151--155",
                month =  nov
                }

@TechReport{ClarkJacob95a,
  author =       "John Clark and Jeremy Jacob",
  title =        "{Security Protocols: An Annotated Bibliography}",
  institution =  "Dept. of Computer Science, University of York",
  year =         1995,
  month =        "June"
}

@TechReport{ClarkJacob95b,
  author =       "John Clark and Jeremy Jacob",
  title =        "{A Library of Security Protocols}",
  institution =  "Dept. of Computer Science, University of York",
  year =         1995,
  month =        "June"
}

@TechReport{ClarkJacob95c,
  author =       "John Clark and Jeremy Jacob",
  title =        "{A Library of Security Protocols with Attacks}",
  institution =  "Dept. of Computer Science, University of York",
  year =         1995,
  month =        "June"
}

@Unpublished{ClarkJacob95d,
  author =       "John Clark and Jeremy Jacob",
  title =        "{Implementation Dependencies in Repeated
                  Authentication Protocols}",
  note =         "",
  OPTcrossref =  "",
  OPTkey =       "",
  OPTyear =      "1995",
  OPTmonth =     "June",
  OPTannote =    ""
}

@Unpublished{ClarkJacob95e,
  author =       "John Clark and Jeremy Jacob",
  title =        "{On the Security of Hwang and Chen's SPLICE/AS
                  Augmented Protocol}",
  year =         1995,
  month =        "June",
  note = "University of York, Department of Computer Science"
}

@Unpublished{ClarkJacob97a,
  author =       "John Clark and Jeremy Jacob",
  title =        "A Survey of Authentication Protocol Literature: Version 1.0",
  year =         1997,
  month =        "November",
  note = "University of York, Department of Computer Science"
}

@Unpublished{ClarkJacob95f,
  author =       "John Clark and Jeremy Jacob",
  title =        "On the {Security of Recent Protocols}",
  note =         "Submitted to Information Processing Letters",
  year =         1995,
  month =        "July",
  annote =       "Submitted to Information Processing Letters"
}

@Unpublished{ClarkJacob96a,
  author =       "John Clark and Jeremy Jacob",
  title =        "Multi-server Spoofing in the {Kerberos} Authentication Protocol",
  note =         "",
  OPTcrossref =  "",
  OPTkey =       "",
  OPTyear =      1996,
  OPTmonth =     jan,
}

@Unpublished{ClarkJacob96b,
  author =       "John Clark and Jeremy Jacob",
  title =        "Freshness is Not Enough",
  note =         "",
  OPTcrossref =  "",
  OPTkey =       "",
  OPTyear =      1996,
  OPTmonth =     jan,
}

@Unpublished{ClarkJacob96c,
  author =       "John Clark and Jeremy Jacob",
  title =        "Non-Repeatability is Not Enough",
  note =         "",
  OPTcrossref =  "",
  OPTkey =       "",
  OPTyear =      1996,
  OPTmonth =     jan,
}

@InProceedings{ClarkeJhaMarrero98,
  author =       {Edmund Clarke and Somesh Jha and Will Marrero},
  title =        {Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols},
  booktitle =    {Proceedings, {IFIP} Working Conference on Programming Concepts and Methods (\textsc{Procomet})},
  year =         1998
}

@Article{CokerEtAl10,
  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},
  title =        {Principles of Remote Attestation},
  journal =      {International Journal of Information Security},
  year =         2011,
  volume = 10,
  number = 2,
  pages = {63--81}}

@Article{ComonCortier04,
  author =       {Hubert Comon and V\'{e}ronique Cortier},
  title =        {Security properties: two agents are sufficient},
  journal =      {Science of Computer Programming},
  year =         2004,
  volume =       50,
  number =       {1-3},
  pages =        {51--71},
  month =        {March}
}

@inproceedings{CortierDelaune07,
        author =        {V{\'e}ronique Cortier and J{\'e}r{\'e}mie Delaitre and St{\'e}phanie Delaune},
        booktitle =     {{F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'07)},
        month = dec,
        publisher =     {Springer},
        series =        {LNCS},
        title = {Safely Composing Security Protocols},
        url =   {\url{http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDD-fsttcs07.pdf}},
        year =  2007,
}

@article{cortier2009safely,
  title={Safely composing security protocols},
  author={V{\'e}ronique Cortier and St{\'e}phanie Delaune},
  journal={Formal Methods in System Design},
  volume={34},
  number={1},
  pages={1--36},
  year={2009},
  publisher={Springer}
}

@TechReport{Coppersmith89,
  author =       "D. Coppersmith",
  title =        "Analysis of {ISO/CCITT} Document {X.509} Annex {D}",
  institution =  "IBM Research Division",
  year =         1989,
  address =      "Yorktown Heights",
  month =        jun
}

@Article{Coppersmith94,
  author =       "D. Coppersmith",
  title =        "The Data Encryption Standard (DES) and its strength
                  against attacks",
  journal =      "IBM Journal of Research and Development",
  year =         1994,
  volume =       38,
  number =       3,
  pages =        "243--250",
  month =        "May"
}

@inproceedings{CorinEtAl07,
  author    = {Ricardo Corin and
               Pierre-Malo Deni{\'e}lou and
               C{\'e}dric Fournet and
               Karthikeyan Bhargavan and
               James J. Leifer},
  title     = {Secure Implementations for Typed Session Abstractions},
  booktitle = {20th IEEE Computer Security Foundations Symposium {CSF}},
  year      = {2007},
  pages     = {170-186},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{BhargavanEtAl09,
  author    = {Karthikeyan Bhargavan and Ricardo Corin and
               Pierre-Malo Deni{\'e}lou and
               C{\'e}dric Fournet and
               James J. Leifer},
  title     = {Cryptographic Protocol Synthesis and Verification for Multiparty Sessions},
  booktitle = {IEEE Computer Security Foundations Symposium},
  year      = 2009
}

@conference{blake1999authenticated,
  title={{Authenticated {Diffe-Hellman} key agreement protocols}},
  author={Simon Blake-Wilson and Alfred Menezes},
  booktitle={Selected Areas in Cryptography},
  pages={630--630},
  year={1999},
  organization={Springer}
}

@article{boneh1998decision,
  title={The decision {Diffie-Hellman} problem},
  author={Dan Boneh},
  journal={Algorithmic Number Theory},
  pages={48--63},
  year={1998},
  publisher={Springer}
}

@article{boreale2003symbolic,
  title={{Symbolic analysis of crypto-protocols based on modular exponentiation}},
  author={Boreale, M. and Buscemi, M.G.},
  journal={Mathematical Foundations of Computer Science},
  pages={269--278},
  year={2003},
  publisher={Springer}
}

@InCollection{BressonEtAl11,
  author =       {Emmanuel Bresson and Yassine Lakhnech and Laurent
                  Mazar{\'e} and Bogdan Warinschi},
  title =        {Computational Soundness:  The Case of
                  {Diffie-Hellman} Keys},
  booktitle =    {Formal Models and Techniques for Analyzing Security Protocols},
  key =          {CortierKremer2011},
  publisher = {{IOS} Press},
  year =         2011,
  editor =       {Veronique Cortier and Steve Kremer},
  series =       {Cryptology and Information Security Series}
}

@InProceedings{Ciobaca10,
  author = 	 {Stefan Ciobaca and V\'eronique Cortier},
  title = 	 {Protocol Composition for Arbitrary Primitives},
  booktitle = {{CSF} '10},
  pages = 	 {322-336},
  year = 	 2010,
  publisher = {{IEEE} {CS} Press}}

@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 = {1-19},
   url = {http://dx.doi.org/10.1007/s10207-011-0124-7},
   year = {2011}
}

@InProceedings{CrazzolaraMilicia02,
  author =       {Federico Crazzolara and Giuseppe Milicia},
  title =        {Developing Security Protocols in $\chi$-Spaces},
  booktitle =    {Proceedings, 7th Nordic Workshop on Secure {IT} Systems},
  year =         2002,
  address =      {Karlstad, Sweden},
  month =        {November}
}

@InProceedings{CrazzolaraWinskel01,
  author =       {Federico Crazzolara and Glynn Winskel},
  title =        {Events in Security Protocols},
  booktitle =    {Proceedings, 8th {ACM} Conference on Computer and Communications Security},
  pages =        {96--105},
  year =         2001,
  address =      {Philadelphia},
  month =        {November},
  publisher =    {{ACM} Press}
}

@InProceedings{CrazzolaraWinskel02,
  author =       {Federico Crazzolara and Glynn Winskel},
  title =        {Composing Strand Spaces},
  booktitle =    {Proceedings, Foundations of Software Technology and Theoretical Computer Science},
  pages =        {97--108},
  year =         2002,
  number =       2556,
  series =       {LNCS},
  address =      {Kanpur},
  month =        {December},
  publisher =    {Springer Verlag}
}

@phdthesis{Cremers06,
  Author    = {C.J.F. Cremers},
  Title     = {Scyther - Semantics and Verification of Security Protocols},
  School    = {Eindhoven University of Technology},
  Publisher = {University Press Eindhoven},
  Year      = 2006,
  Type      = {{Ph.D.} dissertation},
  ISBN      = {978-90-386-0804-4},
}

@inproceedings{Cremers2008,
 author = {Cas J.F. Cremers},
 title = {Unbounded verification, falsification, and characterization of security protocols by pattern refinement},
 booktitle = {{ACM} Conference on Computer and Communications Security
                  ({CCS})},
 year = 2008,
 isbn = {978-1-59593-810-7},
 pages = {119--128},
 location = {Alexandria, Virginia, USA},
 doi = {http://doi.acm.org/10.1145/1455770.1455787},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@misc{CremersFeltz2011,
    author = {Cas Cremers and Michele Feltz},
    title = {One-round Strongly Secure Key Exchange with Perfect Forward Secrecy and Deniability},
    howpublished = {Cryptology ePrint Archive, Report 2011/300},
    year = {2011},
    note = {\url{http://eprint.iacr.org/2011/300}},
}

@article{Cremers12,
  title={Automated analysis of {Diffie-Hellman} protocols and advanced security properties},
  author={Benedikt Schmidt and Simon Meier and Cas Cremers and David A. Basin},
  journal={Computer Security Foundations, ({CSF})},
  pages= {25--27},
  year= 2012
}

@Proceedings{Crypto93,
  title =        "Efficient DES Key Search",
  year =         1993
}

@PhdThesis{TorabiDashti07,
  author =       {Mohammad Torabi Dashti},
  title =        {Keeping Fairness Alive},
  school =       {Vrije Universiteit},
  year =         2007,
  address =      {Amsterdam}}

@inproceedings{DattaEtAl03a,
  author =       "Anupam Datta and Ante Derek and John C. Mitchell and Dusko Pavlovic",
  title =        "Secure protocol composition",
  booktitle =    "Proceedings, Formal Methods in Security Engineering",
  editor =       "Michael Backes and David Basin and Michael Waidner",
  publisher =    "ACM",
  pages =        "11--23",
  year =         2003
}

@inproceedings{DattaEtAl03,
  author =       "Anupam Datta and Ante Derek and John C. Mitchell and Dusko Pavlovic",
  title =        "A derivation system for security protocols and its logical formalization",
  booktitle =    "Proceedings, 16th Computer Security Foundations Workshop",
  editor =       "Dennis Volpano",
  publisher =    "IEEE CS Press",
  pages =        "109--125",
  year =         "2003",
  url =          "ftp://ftp.kestrel.edu/pub/papers/pavlovic/CSFW03.pdf",
}

@InProceedings{DattaEtAl04,
  author =       {Anupam Datta and Ante Derek and John C. Mitchell and Dusko Pavlovic},
  title =        {Abstraction and Refinement in Protocol Derivation},
  booktitle = {{IEEE} Computer Security Foundations Workshop},
  year =         2004,
  publisher = {{IEEE} {CS} Press}}

@Article{DattaEtAl05,
  author =       {Anupam Datta and Ante Derek and John C. Mitchell and Dusko Pavlovic},
  title =        {A Derivation System and Compositional Logic for
     Security Protocols},
  journal =      {Journal of Computer Security},
  year =         2005,
  volume =       13,
  number =       3,
  pages =        {423--482}
}

@inproceedings{DBLP:conf/csfw/DattaDMW06,
  author    = {Anupam Datta and
               Ante Derek and
               John C. Mitchell and
               Bogdan Warinschi},
  title     = {Computationally Sound Compositional Logic for Key Exchange
               Protocols},
  booktitle = {Computer Security Foundations Workshop},
  year      = 2006,
  pages     = {321-334},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/csfw/2006,
  title     = {19th IEEE Computer Security Foundations Workshop, (CSFW-19
               2006), 5-7 July 2006, Venice, Italy},
  booktitle = {CSFW},
  publisher = {IEEE CS},
  year      = {2006},
  isbn      = {0-7695-2615-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{DavisSwick90,
  author =       "D Davis and R Swick",
  title =        "Network Security via Private-Key Certificates",
  year =         1990,
  journal =      "Operating Systems Review",
  pages =        "64--67"
}

@Booklet{Dedekind1888,
  title =        {Was Sind und Was Sollen die Zahlen?},
  author =       {Richard Dedekind},
  address =      {Brunschweig},
  year =         1888,
  note =         {Translated as ``The Nature and Meaning of Numbers,'' in Richard Dedekind, \emph{Essays on the Theory of Numbers}, New York:  Dover, 1963.}
}

@InProceedings{DelauneEtAl2011,
  author =       {St{\'e}phanie Delaune and Steve Kremer and Mark D. Ryan and Graham Steel},
  title =        {Formal analysis of protocols based on {TPM} state registers},
  booktitle = {{IEEE} Symposium on Computer Security Foundations},
  year =         2011,
  month =        {June},
  publisher = {{IEEE CS} Press}}

@Book{Denning82,
author =       "D. E. Denning",
title =        "Cryptography and Data Security",
publisher =    "Addison Wesley",
year =         "1982",
}

@Article{DenningSacco81,
  author =       "Dorothy Denning and G. Sacco",
  title =        "Timestamps in Key Distribution Protocols",
  journal =      "Communications of the ACM",
  year =         1981,
  volume =       24,
  number =       8,
  month =        aug
}

@Misc{DOD5200.28,
  title =        {{Department of Defense} Trusted Computer System Evaluation Criteria},
  howpublished = {{DOD} 5200.28-{STD}},
  month =        {December},
  year =         1985,
  key =          {Department of Defense}
}

@Misc{DES,
  author =       "National Bureau of Standards",
  title =        "Data Encryption Standard",
  howpublished = "Federal Information Processing Standards Publication 46",
  month =        "January",
  year =         1977
}

@Misc{DierksEtAl99,
  author =       {T. Dierks and C. Allen},
  title =        {The {TLS} Protocol},
  howpublished = {{RFC} 2246},
  month =        {January},
  year =         1999
}

@Misc{RFC2104,
  author =       {H. Krawczyk and M. Ballare and R. Canetti},
  title =        {{HMAC}: Keyed--Hashing for Message Authentication},
  howpublished = {{RFC} 2104},
  month =        {February},
  year =         1997
}

@Misc{rfc2246,
  author =       {T. Dierks and C. Allen},
  title =        {The {TLS} Protocol},
  howpublished = {{RFC} 2246},
  month =        {January},
  year =         1999
}

@Article{Diffie88,
  author =       "Whitfield Diffie",
  title =        "The First Ten Years in Public Key Cryptography",
  journal =      "Proceedings of the IEEE",
  year =         1988,
  volume =       76,
  number =       5,
  pages =        "560-577",
  month =        may,
}

@Article{DiffieHellman76,
  author =       "W. Diffie and M. Hellman",
  title =        "New Directions in Cryptography",
  journal =      "IEEE Transactions on Information Theory",
  year =         1976,
  volume =       22,
  number =       6,
  pages =        "644--654",
  month =        nov
}

@article{diffie1992authentication,
  title={{Authentication and authenticated key exchanges}},
  author={Whitfield Diffie and Paul C. {van Oorschot} and Michael J. Wiener},
  journal={Designs, Codes and Cryptography},
  volume=2,
  number=2,
  pages={107--125},
  issn={0925-1022},
  year=1992,
  publisher={Springer}
}

@inproceedings{dilloway2008specifying,
  title={Specifying secure transport channels},
  author={Christopher Dilloway and Gavin Lowe},
  booktitle={CSF},
  pages={210--223},
  year=2008,
  organization={IEEE}
}

@article{DoughertyGuttman2012,
  title={Symbolic Protocol Analysis for {Diffie-Hellman}},
  author={Daniel J. Dougherty and Joshua D. Guttman},
  journal={Arxiv preprint arXiv:1202.2168},
  note = {At \url{http://arxiv.org/abs/1202.2168v1}},
  year={2012}
}

@InProceedings{DoughertyGuttman2012a,
 author = 	 {Daniel J. Dougherty and Joshua D. Guttman},
  title = 	 {An Algebra for
  Symbolic {Diffie-Hellman} Protocol Analysis},
  booktitle = {Trustworthy Global
  Computing},
  year = 	 2012,
  editor = 	 {C. Palamidessi and M. Ryan},
  volume    = {8191},
  pages     = {164--181},
  series = 	 {LNCS}}

@TechReport{DoghmiGuttmanThayer04,
  author =       {Shaddin Doghmi and Joshua Guttman and F. Javier Thayer},
  title =        {The Shapes of Bundles},
  institution =  {The MITRE Corp.},
  year =         2004,
  type =         {MTR},
  number =       {05 B 02}
}

@TechReport{DoghmiGuttmanThayer05,
  author =       {Shaddin Doghmi and Joshua Guttman and F. Javier Thayer},
  title =        {Skeletons and the Shapes of Bundles},
  institution =  {The MITRE Corp.},
  year =         2005,
  type =         {MTR},
  number =       {05 B 02, Revision 1}
}

@TechReport{DoghmiGuttmanThayer05a,
  author =       {Shaddin Doghmi and Joshua Guttman and F. Javier Thayer},
  title =        {Skeletons and the Shapes of Bundles},
  institution =  {The MITRE Corp.},
  year =         2005,
  note =         {Available at \url{http://www.ccs.neu.edu/home/guttman/skeletons.pdf}}
}

@Unpublished{DoghmiGuttmanThayer06,
  author =       {Shaddin F. Doghmi and Joshua D.~Guttman and F. Javier
  Thayer},
  title =        {Skeletons, Homomorphisms, and Shapes: Characterizing Protocol Executions},
  note =         {Submitted for publication},
  month =        {June},
  year =         2006}

@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 =        {November},
  year =         2006}

@InProceedings{DoghmiGuttmanThayer07a,
  author =       {Shaddin F. Doghmi and Joshua D.~Guttman and F. Javier
  Thayer},
  title =        {Skeletons, Homomorphisms, and Shapes: Characterizing Protocol Executions},
  booktitle = {Proceedings, Mathematical Foundations of Program Semantics},
  year =         2007,
  editor =       {M. Mislove},
  OPTseries =    {Electronic Lecture Notes in Theoretical Computer Science},
  month =        {April}}

@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},
  formernote =   {Extended version at \url{http://eprint.iacr.org/2006/435}.  {CPSA} is available at \url{http://hackage.haskell.org/package/cpsa}}}

@InProceedings{DoghmiGuttmanThayer07b,
  author =       {Shaddin F. Doghmi and Joshua D.~Guttman and F. Javier Thayer},
  title =        {Completeness of the Authentication Tests},
  booktitle =    {European Symposium on Research in Computer Security ({ESORICS})},
  pages =        {106--121},
  year =         2007,
  editor =       {J. Biskup and J. Lopez},
  number =       4734,
  series =       {LNCS},
  month =        {September},
  publisher =    {Springer-Verlag}}

@InProceedings{DoghmiGuttmanThayer07c,
  author =       {Shaddin~F. Doghmi and Joshua~D. Guttman and F.~Javier Thayer},
  title =        {Skeletons and the Shapes of Bundles},
  booktitle = {Workshop on Issues in the Theory of Security ({WITS})},
  year =         2007,
  month =        {March},
  note =         {Workshop associated with ETAPS, Braga, Portugal}}

@Article{DolevYao83,
  author =       {Daniel Dolev and Andrew Yao},
  title =        {On the Security of Public-Key Protocols},
  journal =      {{IEEE} Transactions on Information Theory},
  year =         1983,
  volume =       29,
  pages =        {198--208}
}

@Article{DolevEvenKarp82,
  author =       {D. Dolev and S. Even and R. M. Karp},
  title =        {On the Security of Ping-Pong Protocols},
  journal =      {Information and Control},
  year =         1982,
  volume =       55,
  pages =        {57--68}
}

@TechReport{DTOS97,
  author =       "Secure Computing Corporation",
  title =        "DTOS General System Security and Assurability Assessment Report",
  institution =  "MD A904-93-C-4209 CDRL A011",
  year =         1997,
  month =        "June",
  note =         "(http://www.securecomputing.com/randt/HTML/dtos.html)"
}

@InProceedings{DurginEtAl99,
  author =       {N. A. Durgin and P. D. Lincoln and J. C. Mitchell and A. Scedrov},
  title =        {Undecidability of Bounded Security Protocols},
  booktitle =    {Proceedings of the Workshop on Formal Methods and Security Protocols --- FMSP},
  year =         1999,
  note =         {Final version appears in \emph{Journal of Computer Security}, 2004}
}

@Article{DurginEtAl04a,
  author =       {Nancy Durgin and Patrick Lincoln and John Mitchell and Andre Scedrov},
  title =        {Multiset Rewriting and the Complexity of Bounded Security Protocols},
  journal =      {Journal of Computer Security},
  year =         2004,
  volume =       12,
  number =       2,
  pages =        {247--311},
  note =         {Initial version  appeared in \emph{Workshop on Formal Methods and Security Protocols}, 1999}
}

@Article{DurginEtAl04,
  author =       {Nancy Durgin and Patrick Lincoln and John Mitchell and Andre Scedrov},
  title =        {Multiset Rewriting and the Complexity of Bounded Security Protocols},
  journal =      {Journal of Computer Security},
  year =         2004,
  volume =       12,
  number =       2,
  pages =        {247--311},
  note =         {Initial version  appeared in \emph{Workshop on Formal Methods and Security Protocols}, 1999}
}

@Unpublished{DurginEtAl00,
  author =       {Nancy Durgin and John C. Mitchell and Dusko Pavlovic},
  title =        {Protocol Composition and Correctness},
  note =         {Short talk delivered at \emph{Logic in Computer Science}},
  month =        {June},
  year =         2000
}

@InProceedings{DurginEtAl01,
  author =       {Nancy Durgin and John Mitchell and Dusko Pavlovic},
  title =        {A Compositional Logic for Protocol Correctness},
  booktitle =    {Proceedings, 14th Computer Security Foundations Workshop},
  year =         2001,
  publisher =    {{IEEE} CS Press},
  month =        {June}
}

@Article{DurginEtAl03,
  author =       {Nancy Durgin and John Mitchell and Dusko Pavlovic},
  title =        {A Compositional Logic for proving security properties of protocols},
  journal =      {Journal of Computer Security},
  year =         2003,
  volume =       11,
  number =       4,
  pages =        {677--721}
}

@Misc{Eastlake99,
  author =       {D. Eastlake},
  title =        {Domain Name Security Extensions},
  howpublished = {{RFC} 2535},
  month =        {March},
  year =         1999
}

@Misc{RFC2535,
  author =       {D. Eastlake},
  title =        {Domain Name Security Extensions},
  howpublished = {{RFC} 2535},
  month =        {March},
  year =         1999
}

@Misc{Eastlake98,
  author =       {Donald Eastlake},
  title =        {Secret Key Establishment for {DNS}},
  howpublished = {Internet--Draft draft-ietf-dnssec-tkey-01.txt},
  month =        {September},
  year =         1998
}

@Misc{Eastlake98a,
  author =       {Donald E. Eastlake},
  title =        {Secure Domain Name System Dynamic Update},
  howpublished = {Internet--Draft draft-ietf-dnssec-update2-00.txt},
  month =        {August},
  year =         1998
}

@Misc{Ellison99,
  author =       {Carl Ellison},
  title =        {{SPKI}  Requirements},
  howpublished = {{IETF RFC} 2692},
  month =        {September},
  year =         1999
}

@Misc{EllisonEtAl99,
  author =       {Carl Ellison and Bill Frantz and Butler Lampson and Ron Rivest and Brian Thomas and Tatu Ylonen},
  title =        {{SPKI} Certificate Theory},
  howpublished = {{IETF RFC} 2693},
  month =        {September},
  year =         1999
}

@Misc{ElzBush97,
  author =       {R. Elz and R.  Bush},
  title =        {Clarifications to the {DNS} Specification},
  howpublished = {{RFC} 2182},
  month =        {July},
  year =         1997
}

@Misc{RFC2182,
  author =       {R. Elz and R.  Bush},
  title =        {Clarifications to the {DNS} Specification},
  howpublished = {{RFC} 2182},
  month =        {July},
  year =         1997
}

@article{escobar2008state,
  title={{State space reduction in the Maude-{NPA} protocol analyzer}},
  author={Santiago Escobar and Catherine Meadows and Jos\'e Meseguer},
  journal={Computer Security-ESORICS 2008},
  pages={548--562},
  year={2008},
  publisher={Springer}
}

@article{escobar2009maude,
  title={{Maude-{NPA}: Cryptographic protocol analysis modulo
                  equational properties}},
  author={Santiago Escobar and Catherine Meadows and Jos\'e Meseguer},
  journal={Foundations of Security Analysis and Design V},
  pages={1--50},
  year={2009},
  publisher={Springer}
}

@inproceedings{DBLP:conf/fosad/EscobarMM07,
  author    = {Santiago Escobar and
               Catherine Meadows and
               Jos\'e Meseguer},
  title     = {Maude-{NPA}: Cryptographic Protocol Analysis Modulo Equational
               Properties},
  booktitle = {Foundations of Security Analysis and Design {V}, {FOSAD}
                  2007--2009 Tutorial Lectures},
  pages     = {1-50},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = 5705,
  year      = 2009,
  isbn      = {978-3-642-03828-0},
  ee        = {http://dx.doi.org/10.1007/978-3-642-03829-7_1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TechReport{EvenYacobi80,
  title={Relations among public key signature systems},
  author={Shimon Even and Yacov Yacobi},
  institution={Computer Science Department, Technion},
  number=175,
  year =         1980
}

@InProceedings{EvenEtAl85,
  author =       {Shimon Even and Oded Goldreich and Adi Shamir},
  title =        {On the Security of Ping-Pong Protocols when Implemented using the {RSA}},
  booktitle =    {Advances in Cryptology---{\sc crypto} '85},
  pages =        {58--72},
  year =         1985,
  series =       {LNCS},
  publisher =    {Springer Verlag}
}

@InProceedings{FarmerEtAl92,
    author = {William M. Farmer and Joshua D. Guttman and F. Javier Thayer},
    title = {Little theories},
    booktitle = {Automated Deduction:  CADE-11},
    number =     607,
    series =     {LNCS},
    year = 1992,
    pages = {567--581},
    publisher = {Springer-Verlag}
}

@InProceedings{,
  author =       {},
  title =        {},
  OPTcrossref =  {},
  OPTkey =       {},
  OPTbooktitle = {},
  OPTpages =     {},
  OPTyear =      {},
  OPTeditor =    {},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote =      {},
  OPTannote =    {}
}

@Article{FarmerEtAl93,
  author =       {William M.~Farmer and Joshua D.~Guttman and F.~Javier Thayer},
  title =        {{\sc imps}: An {I}nteractive {M}athematical {P}roof {S}ystem},
  journal =      {Journal of Automated Reasoning},
  year =         1993,
  volume =       11,
  pages =        {213--248}}

@Article{FarmerGuttman00,
  author =       {W. M. Farmer and J. D. Guttman},
  title =        {A Set Theory with Support for Partial Functions},
  journal =      {Studia Logica},
  year =         2000,
  volume =       65,
  pages =        {59--70}
}

@InProceedings{Failure98,
  author =       {P.A. Loscocco and S.D. Smalley and P.A. Muckelbauer and R.C. Taylor and S.J. Turner and J.F. Farrell},
  title =        {The Inevitability of Failure: The Flawed Assumption of Security in Modern Computing Environments},
  booktitle =    {Proceedings of the 21st National Information Systems Security Conference},
  pages =        {303--314},
  year =         1998,
  month =        {October}
}

@InProceedings{Feldman87,
 author =       "P. Feldman",
 title =        "A practical scheme for non-interactive verifiable secret sharing",
 booktitle =    "Proceedings of the 28th IEEE Symposium on the Foundations of Computer Science",
 pages =        "427-438",
 year =         1987,
 publisher =    "IEEE"
}

@InProceedings{FerraioloKuhn92,
  author =       "David Ferraiolo and Richard Kuhn",
  title =        "Role-Based Access Control",
  booktitle =    "Proceedings of the 15th National Computer Security Conference",
  year =         1992
}

@Book{Feller,
  author =      "W. Feller",
  title =       "An Introduction to Probability Theory and its Applications",
  publisher =   "John Wiley and Sons, Inc.",
  year =        "1958",
  OPTeditor =   "",
  OPTvolume =   "",
  OPTseries =   "",
  address =     "New York",
  OPTedition =  "",
  OPTmonth =    "",
  OPTnote =     ""
}

@Book{Dudley,
  author =      "R.  M. Dudley",
  title =       "Real Analysis and Probability",
  publisher =   "Wadsworth and Brookscole",
  year =        "1989",
  OPTeditor =   "",
  OPTvolume =   "",
  OPTseries =   "",
  address =     "Pacific Grove",
  OPTedition =  "",
  OPTmonth =    "",
  OPTnote =     ""
}

@Manual{FIPS,
  title =        "Security Requirements for Cryptographic Modules",
  note =         "FIPS PUB 140-1",
  author =       "Federal Information Processing Standards Publication",
  organization = "National Institue of Standards and Technology",
  note =         "US Department of Commerce",
  month =        "January",
  year =         1994
}

@Manual{FIPS4676,
title =        "Federal Information Processing Standard 46 -- the
    Data Encryption Standard",
OPTcrossref =  "",
OPTkey =       "",
OPTauthor =    "",
OPTorganization = "",
OPTaddress =   "",
OPTedition =   "",
OPTyear =      "1976",
OPTmonth =     "",
OPTnote =      "",
OPTannote =    ""
}

@Article{FocardiGorrieri97,
  author =       {Riccardo Focardi and Roberto Gorrieri},
  title =        {The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties},
  journal =      {IEEE Transactions on Software Engineering},
  year =         1997,
  volume =       23,
  number =       9,
  month =        {September},
  annote =    {Retrieved from http://www.cs.unibo.it/\~focardi/www/biblio2.html}
}

@InProceedings{DuranteFocardiGorrieri99,
  author =       {Antonio Durante and Riccardo Focardi and Roberto Gorrieri},
  title =        {{CVS}: A Compiler for the Analysis of Cryptographic Protocols},
  booktitle =    {12th Computer Security Foundations
                  Workshop Proceedings},
  pages =        {203--212},
  year =         1999,
  month =        {June},
  publisher =    {{IEEE} CS Press}
}

@TechReport{FDR2,
  author =       {Formal Systems (Europe) Ltd.},
  title =        {Failures-Divergence Refinement: {FDR}~2 User Manual},
  institution =  {Formal Systems (Europe) Ltd.},
  year =         {1997},
  OPTkey =       {},
  OPTtype =      {},
  OPTnumber =    {},
  address =      {http: //www.formal.demon.co.uk/},
  OPTmonth =     {},
  OPTnote =      {},
  OPTannote =    {}
}

@InProceedings{FournetEtAl05,
  author =       {C\'{e}dric Fournet and Andrew Gordon and Sergei Maffeis},
  title =        {A Type Discipline for Authorization Policies},
  booktitle =    {European Symposium on Programming},
  year =         2005,
  editor =       {Mooly Sagiv},
  volume =       {LNCS No},
  series =       {LNCS},
  publisher =    {Springer Verlag}
}

@Misc{FrierEtAl96,
  author =       {Alan Frier and Philip Karlton and Paul Kocher},
  title =        {The {SSL} 3.0 Protocol},
  year =         1996,
  key =          {draft-freier-ssl-version3-02.txt},
  howpublished = {Internet Draft},
  month =        nov
}

@InProceedings{Froeschle08,
  author = {Sibylle Fr{\"o}schle},
  title = {Adding Branching to the Strand Space Model},
  booktitle = {Proceedings of {EXPRESS'08}},
  series = {ENTCS},
  publisher = {Elsevier},
  year =         2008
}

@Article{FumyLandrock93,
  author =       "W. Fumy and P. Landrock",
  title =        "Principles of Key Management",
  journal =      "IEEE Journal on Selected Areas in Communications",
  year =         1993,
  pages =        "785--793",
  month =        jun
}

@inproceedings{GarayEtAl99,
 author = {Juan A. Garay and Markus Jakobsson and Philip D. MacKenzie},
 title = {Abuse-Free Optimistic Contract Signing},
 booktitle = {CRYPTO '99: Proceedings of the 19th Annual International Cryptology Conference on Advances in Cryptology},
 year = {1999},
 isbn = {3-540-66347-9},
 pages = {449--466},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@InCollection{Gentzen35,
  author =      "G. Gentzen",
  title =       "Investigations into Logical Deduction (1935)",
  booktitle =   "The Collected Works of Gerhard Gentzen",
  publisher =   "North Holland",
  year =        1969}

@InProceedings{GeometricLogic,
  author =       {NN},
  title =        {Geometric Logic},
  booktitle = {Whatever volume contains it},
  year =         {200?}}

@misc{ghcUsersGuide,
  title = {{GHC} User's Guide Documentation, release 8.2.1},
  author = {The {GHC} Team},
  note = {\url{https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf}},
  month = {July},
  year = {2017},
  day = 21,
}

@InProceedings{GoguenMeseguer82,
  author =       {Joseph A. Goguen and Jos\'e Meseguer},
  title =        {Security Policies and Security Models},
  booktitle =    {{IEEE} Symposium on Security and Privacy},
  year =         1982
}

@article{GoguenMeseguer92,
 author = {Joseph A. Goguen and Jos\'{e} Meseguer},
 title = {Order-sorted algebra {I}: equational deduction for multiple inheritance, overloading, exceptions and partial operations},
 journal = {Theoretical Computer Science},
 volume = {105},
 number = {2},
 year = {1992},
 pages = {217--273},
 doi = {http://dx.doi.org/10.1016/0304-3975(92)90302-V},
 publisher = {Elsevier Science Publishers Ltd.},
 address = {Essex, UK},
 }

@Article{GongAuth,
  author =       "Li Gong",
  title =        "Increasing Availability and Security of an Authentication Service",
  journal =      "IEEE Journal on Selected Areas in Communications",
  year =         1993,
  volume =       11,
  number =       5,
  month =        jun
}

@Article{Gong89,
  author =       "Li Gong",
  title =        "Using One-way Functions for Authentication ",
  journal =      "Computer Communication Review",
  year =         1989,
  volume =       19,
  number =       5,
  pages =        "8-11",
  month =        oct
}

@Unpublished{GoldwasserBellare,
  author =       {Shafi Goldwasser and Mihir Bellare},
  title =        {Lecture Notes on Cryptography},
  note =         {Avaliable at http://www.cs.ucsd.edu/users/mihir/papers/gb.html},
  month =        {August},
  year =         1999
}

@InProceedings{Gong90a,
  author =       "Li Gong",
  title =        "Verifiable-Text Attacks in Cryptographic Protocols",
  pages =        "686--693",
  booktitle =    "Proceedings {IEEE} {INFOCOM'90} ",
  year =         1990,
  publisher =    "IEEE CS",
  month =        jun,
}

@Article{Gong90b,
  author =       "Li Gong",
  title =        "A Note on Redundancy in Encrypted Messages",
  journal =      "Computer Communication Review",
  year =         1990,
  volume =       20,
  number =       5,
  pages =        "18-22",
  month =        oct,
}

@InProceedings{Gong91,
  author =       "Li Gong",
  title =        "Handling Infeasible Specifications of Cryptographic
                  Protocols",
  pages =        "99--102",
  booktitle =    "Proceedings of The 4th {IEEE} Computer Security
                  Foundations Workshop",
  year =         1991,
  publisher =    "IEEE CS",
  month =        jun
}

@InProceedings{Gong93,
  author =       "Li Gong",
  title =        "Variations on the Themes of Message Freshness and
                  Replay and Replay or, the Difficulty of of Devising
                  Formal Nethods to Analyse Cryptographic Protocols",
  pages =        "131--136",
  booktitle =    "Proceedings 6th Computer Security Foundations Workshop",
  year =         1993,
  publisher =    "IEEE CS Press"
}

@Article{GongLomasNeedhamSaltzer93,
  author =       "Li Gong and A. Lomas and Roger M. Needham and Jerry
                  H. Saltzer",
  title =        "Protecting Poorly Chosen Secrets from Guessing Attacks",
  journal =      "IEEE Journal on Selected Areas in Communications",
  year =         1993,
  volume =       11,
  number =       5,
  month =        jun
}

@InProceedings{GongNeedhamYahalom90,
  author =       "Li Gong and Roger Needham and Raphael Yahalom",
  title =        "Reasoning About Belief in Cryptographic Protocols",
  editor =       "Deborah Cooper and Teresa Lunt",
  pages =        "234--248",
  booktitle =    "Proceedings 1990 IEEE Symposium on Research in
                  Security and Privacy",
  year =         1990,
  publisher =    "IEEE CS",
  month =        may
}

@InProceedings{GongSyverson95,
  author =       {Li Gong and Paul Syverson},
  title =        {Fail-Stop Protocols: An Approach to Designing Secure Protocols},
  booktitle =    {5th International Working Conference on Dependable Computing for Critical Applications},
  pages =        {44--55},
  year =         1995,
  month =        {September}
}

@InProceedings{Gordon84,
  title =        "Public Key Cryptosystems",
  author =       "John Gordon",
  booktitle =    "Proceedings of Networks '84",
  year =         1984
}

@InProceedings{GordonJeffrey01a,
  author =       {Andrew D. Gordon and Alan Jeffrey},
  title =        {Authentication by Typing},
  booktitle =    {Proceedings, 14th Computer Security Foundations Workshop},
  year =         2001,
  month =        {June},
  publisher =    {{IEEE} CS Press}
}

@InProceedings{GordonJeffrey02,
  author =       {Andrew D. Gordon and Alan Jeffrey},
  title =        {Types and Effects for Asymmetric Cryptographic Protocols},
  booktitle =    {Proceedings, 15th Computer Security Foundations Workshop},
  year =         2002,
  month =        {June},
  publisher =    {{IEEE} CS Press}
}

@Article{GordonJeffrey03,
  author =       {Andrew D. Gordon and Alan Jeffrey},
  title =        {Authenticity by typing for security protocols},
  journal =      {Journal of Computer Security},
  year =         2003,
  volume =       11,
  number =       4,
  pages =        {451-–521}}

@Article{GordonJeffrey03a,
  author =       {Andrew D. Gordon and Alan Jeffrey},
  title =        {Types and effects for asymmetric cryptographic protocols},
  journal =      {Journal of Computer Security},
  year =         2004,
  volume =       12,
  number =       {3/4},
  pages =        {435–-484}}

@article{goubault2005abstraction,
  title={{Abstraction and resolution modulo AC: How to verify {Diffie-Hellman}-like protocols automatically}},
  author={Jean Goubault-Larrecq and Muriel Roger and Kumar Verma},
  journal={Journal of Logic and Algebraic Programming},
  volume={64},
  number={2},
  pages={219--251},
  issn={1567-8326},
  year={2005},
  publisher={Elsevier}
}
 @inproceedings{GoubaultLarrecq08,
  author    = {Jean Goubault-Larrecq},
  title     = {Towards Producing Formally Checkable Security Proofs, Automatically},
  booktitle = {Computer Security Foundations Workshop},
  year      = {2008},
  pages     = {224-238},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/CSF.2008.21},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{gross2011vertical,
  title={Vertical protocol composition},
  author={Thomas Gro{\ss} and Sebastian M{\"o}dersheim},
  booktitle={CSF},
  pages={235--250},
  year={2011},
  organization={IEEE}
}

@Article{VLispIntro95,
  author =       {Joshua~D. Guttman and John~D. Ramsdell and Mitchell Wand},
  title =        {{VLISP}: A verified implementation of {Scheme}},
  journal =      {Lisp and Symbolic Computation},
  year =         1995,
  volume =       8,
  number =       {1/2},
  pages =        {5--32}}

@Article{VLispScheme95,
  author =       {Joshua~D. Guttman and John~D. Ramsdell and Vipin Swarup},
  title =        {The {VLISP} verified {Scheme} system},
  journal =      {Lisp and Symbolic Computation},
  year =         1995,
  volume =       8,
  number =       {1/2},
  pages =        {33--110}}

@TECHREPORT{Guttman96,
        AUTHOR = "Joshua D. Guttman",
        TITLE = "Filtering Postures: Local Enforcement for Global Policies",
        NUMBER = "MTR 97B0000007",
        INSTITUTION = "The MITRE Corporation, Center for Integrated Intelligence Systems",
        ADDRESS = "Bedford, Massachusets",
        MONTH = "November",
        YEAR = "1996" }

@InProceedings{Guttman97,
  author =       {Joshua D. Guttman},
  title =        {Filtering Postures:  Local Enforcement for Global Policies},
  booktitle =    {Proceedings, 1997 {IEEE} Symposium on Security and Privacy},
  pages =        {120--29},
  year =         1997,
  month =        {May},
  publisher =    {{IEEE} CS Press}
}

@Unpublished{Guttman99,
  author =       {Joshua D. Guttman},
  title =        {Packet Filters and their Atoms},
  note =         {Lecture at University of Pennsylvania, host C.~Gunter},
  month =        {April},
  year =         1999
}

@InCollection{Guttman01,
  author =       {Joshua D. Guttman},
  title =        {Security Goals: Packet Trajectories and Strand Spaces},
  booktitle =    {Foundations of Security Analysis and Design},
  publisher =    {Springer Verlag},
  year =         2001,
  editor =       {Roberto Gorrieri and Riccardo Focardi},
  volume =       2171,
  series =       {LNCS},
  pages =        {197--261},
  note =         {}
}

@Article{Guttman01a,
  author =       {Joshua D. Guttman},
  title =        {Key Compromise and the Authentication Tests},
  journal =      {Electronic Notes in Theoretical Computer Science},
  year =         2001,
  volume =       47,
  note =         {Editor, M. Mislove.  URL~\url{http://www.elsevier.nl/locate/entcs/volume47.html}, 21 pages}
}

@InProceedings{Guttman02,
  author =       {Joshua D. Guttman},
  title =        {Security Protocol Design via Authentication Tests},
  booktitle =    {Proceedings, 15th Computer Security Foundations Workshop},
  year =         2002,
  month =        {June},
  publisher =    {{IEEE} CS Press}
}

@Article{Guttman04,
  author =       {Joshua D. Guttman},
  title =        {Authentication Tests and Disjoint Encryption: a Design Method for Security Protocols},
  journal =      {Journal of Computer Security},
  year =         2004,
  volume =       12,
  number =       {3/4},
  pages =        {409--433}
}

@Article{Guttman04old,
  author =       {Joshua D. Guttman},
  title =        {Authentication Tests and Disjoint Encryption: a Design Method for Security Protocols},
  journal =      {Journal of Computer Security},
  year =         2004,
  volume =       12,
  number =       {3/4},
  note =        {Extended version of ``Security Protocol Design via Authentication Tests,'' CSFW 2002.},
  pages =        {409--433}
}

@InProceedings{Guttman04a,
  author =       {Joshua D. Guttman},
  title =        {Security, Protocols, and Trust},
  booktitle =    {VMCAI 2004:  Verification, Model Checking, and Abstract Interpretation},
  year =         2004,
  editor =       {G. Levi and B. Steffen},
  volume =       2937,
  series =       {LNCS},
  publisher =    {Springer Verlag},
  note =         {(abstract of tutorial)}
}

@Unpublished{Guttman08,
  author =       {Joshua D. Guttman},
  title =        {Cryptographic Protocol Composition, via the
                  Authentication Tests},
  note =         {Submitted for publication},
  month =        {January},
  year =         2008}

@InProceedings{Guttman09,
  author =       {Joshua D. Guttman},
  title =        {Cryptographic Protocol Composition via the
                  Authentication Tests},
  booktitle = {Foundations of Software Science and Computation Structures ({FOSSACS})},
  year =         2009,
  editor =       {Luca de Alfaro},
  series =       {LNCS},
  number =       5504,
  pages =        {303--317},
  month =        {March},
  publisher = {Springer}}

@InProceedings{Guttman09a,
  author =       {Joshua D. Guttman},
  title =        {Transformations between Cryptographic Protocols},
  booktitle = {Automated Reasoning in Security Protocol Analysis, and Workshop on Issues in the Theory of Security ({ARSPA-WITS})},
  year =         2009,
  pages =        {107--123},
  number =       5511,
  editor =       {P. Degano and L. Vigan{\`o}},
  series =       {LNCS},
  publisher = {Springer}}

@InProceedings{Guttman09b,
  author =       {Joshua D. Guttman},
  title =        {Fair Exchange in Strand Spaces},
  booktitle = {SecCo: 7th International Workshop on Security Issues
                  in Concurrency},
  year =         2009,
  editor =       {M. Boreale and S. Kremer},
  series =       {EPTCS},
  month =        {Sep},
  publisher = {Electronic Proceedings in Theoretical Computer
                  Science}}

@Article{Guttman09c,
  author = {Joshua D. Guttman},
  title = {Security Theorems via Model Theory},
  journal = {EXPRESS:  Expressiveness in Concurrency (EPTCS)},
  volume = {8},
  pages = {51},
  url = {http://cgi.cse.unsw.edu.au/~rvg/eptcs/content.cgi?EXPRESS2009},
  note = {doi:10.4204/EPTCS.8.5},
  year = {2009}
}

@Article{Guttman12,
  author = 	 {Joshua D. Guttman},
  title = 	 {State and Progress in Strand Spaces:  Proving Fair
                  Exchange},
  journal = 	 {Journal of Automated Reasoning},
  year = 	 2012,
  volume = 	 48,
  number = 	 2,
  pages = 	 {159--195},
  url =         {http://www.springerlink.com/content/p87u245036468165/},
  doinote = 	 {DOI: 10.1007/s10817-010-9202-1}}

@Article{Guttman11a,
  author =       {Joshua D. Guttman},
  title =        {State and Progress in Strand Spaces:  Proving Fair
                  Exchange},
  journal =      {Journal of Automated Reasoning},
  year =         2012,
  url =         {http://www.springerlink.com/content/p87u245036468165/},
  note =         {Accepted, March 2010.  DOI: 10.1007/s10817-010-9202-1}}

@Book{CortierKremer2011,
  editor =       {Veronique Cortier and Steve Kremer},
  title =        {Formal Models and Techniques for Analyzing Security Protocols},
  publisher =    {IOS Press},
  year =         2011,
  series =       {Cryptology and Information Security Series}}

@InCollection{Guttman10,
  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,
  editor =       {Veronique Cortier and Steve Kremer},
  series =       {Cryptology and Information Security Series}}

@InProceedings{Guttman11,
  author =       {Joshua D. Guttman},
  title =        {Security Goals and Protocol Transformations},
  booktitle = {Tosca:  Theory of Security and Applications},
  year =         2011,
  editor =       {Sebastian M{\"o}dersheim and Catuscia Palamidessi},
  series =       {LNCS},
  month =        {March},
  publisher = {Springer}}

@InProceedings{GuttmanEtAl00,
  author =       {Joshua Guttman and Amy L. Herzog and F. Javier Thayer},
  booktitle =    {Proceedings, ESORICS 2000},
  pages =        {255-272},
  year =         {2000},
  month =        {October},
  publisher =    {Springer},
  note =         {Lecture Notes in Computer Science 1895}
}

@InProceedings{GuttmanHerzog02,
  author =       "Joshua D. Guttman and Amy L. Herzog",
  title =        "Eager Formal Methods for Security Management",
  booktitle =    "Proceedings, VERIFY '02",
  pages =        "91--101",
  year =         2002,
  month =        "July"
}

@Article{GuttmanHerzog05,
  author =       {Joshua D. Guttman and Amy L. Herzog},
  title =        {Rigorous Automated Network Security Management},
  journal =      {International Journal for Information Security},
  year =         2005,
  volume =       5,
  number =       {1--2},
  pages =        {29--48}
}

@Article{GuttmanHerzog03,
  author =       {Joshua D. Guttman and Amy L. Herzog},
  title =        {Rigorous Automated Network Security Management},
  journal =      {International Journal for Information Security},
  year =         2004,
  note =         {Forthcoming}
}

@Misc{GuttmanHerzogRamsdell03,
  author =       {Joshua D. Guttman and Amy L. Herzog and John D. Ramsdell},
  title =        {Information Flow in Operating Systems: Eager Formal Methods},
  howpublished = {Submitted for publication},
  month =        {January},
  year =         2003
}

@Article{GuttmanHerzogRamsdell04,
  author =       {Joshua D. Guttman and Amy L. Herzog and John D. Ramsdell and Clement W. Skorupka},
  title =        {Verifying Information Flow Goals in {Security-Enhanced Linux}},
  journal =      {Journal of Computer Security},
  year =         2005,
  volume =       13,
  number =       1,
  pages =        {115--134},
  note =         {Preliminary version appeared in the Workshop on Issues in the Theory of Security (IFIP WG 1.7), April 2003.}
}

@TechReport{GuttmanHerzogThayer00ab,
  author =       {Joshua D. Guttman and Amy L. Herzog and F. Javier Thayer},
  title =        {Authentication and Confidentiality via {IPsec}},
  institution =  {The {MITRE} Corporation},
  year =         2000,
  month =        {March}
}

@InProceedings{GuttmanHerzogThayer00,
  author =       {Joshua D. Guttman and Amy L. Herzog and F. Javier Thayer},
  title =        {Authentication and Confidentiality via {IPsec}},
  booktitle =    {ESORICS 2000: European Symposium on Research in Computer Security},
  year =         2000,
  number =       1895,
  editor =       {D. Gollman},
  series =       {LNCS},
  publisher =    {Springer Verlag}
}

@InProceedings{GuttmanEtAl05,
  author =       {Joshua D. Guttman and Jonathan C. Herzog and John D. Ramsdell and Brian T. Sniffen},
  title =        {Programming Cryptographic Protocols},
  booktitle =    {Trust in Global Computing},
  pages =        {116--145},
  year =         2005,
  editor =       {Rocco De Nicola and Davide Sangiorgi},
  number =       3705,
  series =       {LNCS},
  publisher =    {Springer}
}

@inproceedings{McCarthyEtAl07,
  author    = {Jay A. McCarthy and
               Shriram Krishnamurthi and
               Joshua D. Guttman and
               John D. Ramsdell},
  title     = {Compiling cryptographic protocols for deployment on the web},
  booktitle = {World Wide Web Conference},
  pages     = {687--696},
  publisher = {{ACM}},
  year      = {2007},
  url       = {https://doi.org/10.1145/1242572.1242665},
  doi       = {10.1145/1242572.1242665},
  timestamp = {Tue, 06 Nov 2018 16:57:07 +0100},
  biburl    = {https://dblp.org/rec/conf/www/McCarthyKGR07.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Unpublished{GuttmanThayer99,
  author =       {Joshua D. Guttman and F. Javier {\textsc{Thayer} F\'abrega}},
  title =        {Disjoint Encryption and the Normal Penetrator},
  note =         {Unpublished},
  month =        {September},
  year =         1999
}

@InProceedings{GuttmanThayer00,
  author =       {Joshua D. Guttman and F. Javier {Thayer}},
  title =        {Authentication Tests},
  booktitle =    {Proceedings, 2000 IEEE Symposium on Security and Privacy},
  year =         2000,
  organization = {May},
  publisher =    {IEEE CS Press}
}

@TechReport{GuttmanThayer00a,
  author =       {Joshua D. Guttman and F. Javier {\textsc{Thayer} F{\'a}brega}},
  title =        {Authentication Tests and the Normal Penetrator},
  institution =  {The {MITRE} Corporation},
  year =         2000,
  type =         {MTR},
  number =       {00B04},
  month =        {February},
  note =         {Also submitted for publication.{\typeout{ERROR:  Don't cite this anymore, use GuttmanThayer00c.}}}
}

@Article{GuttmanThayer00caca,
  author =       {Joshua D. Guttman and F. Javier {\textsc{Thayer} F{\'a}brega}},
  title =        {Authentication Tests and the Structure of Bundles},
  journal =      {Theoretical Computer Science},
  year =         2002,
  note =         {To appear}
}

@Article{GuttmanThayer00c,
  author =       {Joshua D. Guttman and F. Javier {{Thayer}}},
  title =        {Authentication Tests and the Structure of Bundles},
  journal =      {Theoretical Computer Science},
  year =         2002,
  month =        {June},
  pages =        {333--380},
  volume =       283,
  number =       2
}

@Article{GuttmanThayer02,
  author =       {Joshua D. Guttman and F. Javier {{Thayer}}},
  title =        {Authentication Tests and the Structure of Bundles},
  journal =      {Theoretical Computer Science},
  year =         2002,
  month =        {June},
  pages =        {333--380},
  volume =       283,
  number =       2
}

@InProceedings{GuttmanThayer00b,
  author =       {Joshua D. Guttman and F. Javier {{Thayer}}},
  title =        {Protocol Independence through Disjoint Encryption},
  booktitle =    {Computer Security Foundations Workshop},
  year =         2000,
  publisher =    {{IEEE} {CS} Press}
}

@Unpublished{GuttmanThayer00ba,
  author =       {Joshua D. Guttman and F. Javier {\textsc{Thayer} F{\'a}brega}},
  title =        {Protocol Independence through Disjoint Encryption},
  note =         {In preparation.},
  OPTkey =       {},
  OPTmonth =     {},
  OPTyear =      {},
  OPTannote =    {}
}

@TechReport{GuttmanThayer05,
  author =       {Joshua D. Guttman and F. Javier Thayer},
  title =        {The Sizes of Skeletons:  Decidable Cryptographic Protocol
  Authentication and Secrecy Goals},
  institution =  {The MITRE Corporation},
  year =         2005,
  type =         {MTR},
  number =       {05B09 Revision~1},
  month =        {March}
}

@TechReport{GuttmanThayer05a,
  author =       {Joshua D. Guttman and F. Javier Thayer},
  title =        {Protocol Security Goals and the Size of Skeletons},
  institution =  {The MITRE Corp.},
  year =         2005,
  note =         {Available at \url{http://www.ccs.neu.edu/home/guttman/sizes_of_skeletons.pdf}, submitted for publication}
}

@InProceedings{GuttmanThayerZuck01,
  author =       {Joshua D. Guttman and F. Javier Thayer and Lenore D. Zuck},
  title =        {The Faithfulness of Abstract Protocol Analysis:  Message Authentication},
  booktitle =    {Proceedings, Eighth ACM Conference on Computer and Communications Security},
  year =         2001,
  month =        {November},
  organization = {{ACM}}
}

@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 =    {Programming Languages and Systems: 13th European Symposium on Programming},
  pages =        {325--339},
  year =         2004,
  editor =       {David Schmidt},
  number =       2986,
  series =       {LNCS},
  publisher =    {Springer}
}

@Article{GuttmanThayerZuck03,
  author =       {Joshua D. Guttman and F. Javier Thayer and Lenore D. Zuck},
  title =        {The Faithfulness of Abstract Protocol Analysis:  Message Authentication},
  journal =      {Journal of Computer Security},
  year =         2004,
  volume =       12,
  number =       6,
  pages =        {865--891}
}

@Article{GuttmanThayerZuck04,
  author =       {Joshua D. Guttman and F. Javier Thayer and Lenore D. Zuck},
  title =        {The Faithfulness of Abstract Protocol Analysis:  Message Authentication},
  journal =      {Journal of Computer Security},
  year =         2004,
  volume =       12,
  number =       6,
  pages =        {865--891}
}

@proceedings{DBLP:conf/ifip1-7/2008,
  editor    = {Pierpaolo Degano and
               Joshua D. Guttman and
               Fabio Martinelli},
  title     = {Formal Aspects in Security and Trust, 5th International
               Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008,
               Revised Selected Papers},
  booktitle = {Formal Aspects in Security and Trust},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5491},
  year      = {2009},
  ee        = {http://dx.doi.org/10.1007/978-3-642-01465-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InCollection{Halpern95,
  author =       {Joseph Y. Halpern},
  title =        {Reasoning about Knowledge:  A Survey},
  booktitle =    {Handbook of Logic in Artificial Intelligence and Logic Programming},
  pages =        {1--34},
  publisher =    {Oxford University Press},
  year =         1995,
  editor =       {D. Gabbay and C. J. Hogger and J. A Robinson},
  volume =       4
}

@Article{HalpernvanderMeyden01,
  author =       {Joseph Y. Halpern and Ron {van der Meyden}},
  title =        {A Logic for {SDSI}'s Linked Local Name Spaces},
  journal =      {Journal of Computer Security},
  year =         2001,
  volume =       9,
  number =       {1--2},
  pages =        {47--74}
}

@Book{HalpernEtAl95,
  author =       {Ronald Fagin and Joseph Y. Halpern and Yoram Moses and Moshe Y. Vardi},
  title =        {Reasoning about Knowledge},
  publisher =    {{MIT} Press},
  year =         1995,
  address =      {Cambridge, MA}
}

@Article{HalpernPucella03,
  author =       {Joseph Y. Halpern and Riccardo Pucella},
  title =        {On the Relationship between Strand Spaces and Multi-Agent Systems},
  journal =      {{ACM} Transactions on Information and System Security},
  year =         2003,
  volume =       6,
  number =       1,
  pages =        {43--70},
  month =        {February}
}

@InProceedings{HauserJansenMolvaTsudikHerreweghen94,
  author =       "R. Hauser and P. Jansen and R. Molva and G. Tsudik
                  and E. van Herreweghen",
  title =        "Robust and Secure Pasword and Key Change Method",
  editor =       "Dieter Gollmann",
  number =       875,
  series =       "Lecture Notes in Computer Science",
  pages =        "107--122",
  booktitle =    "Computer Security---{ESORICS} '94",
  year =         1994,
  publisher =    "Springer"
}

@InProceedings{HeatherEtAl00,
  author =       {James Heather and Gavin Lowe and Steve Schneider},
  title =        {How to Prevent Type Flaw Attacks on Security Protocols},
  booktitle =    {Proceedings, 13th Computer Security Foundations Workshop},
  year =         2000,
  month =        {July},
  publisher =    {{IEEE} CS Press}
}

@InProceedings{HeatherSchneider00,
  author =       {James Heather and Steve Schneider},
  title =        {Toward Automatic Verification of Authentication Protocols on an Unbounded Network},
  booktitle =    {Proceedings, 13th Computer Security Foundations Workshop},
  year =         2000,
  month =        {July},
  publisher =    {{IEEE} CS Press}
}

@Article{HeatherSchneider05,
  author =       {James A. Heather and Steve A. Schneider},
  title =        {A Decision Procedure for the Existence of a Rank Function},
  journal =      {Journal of Computer Security},
  year =         2005,
  note =         "Forthcoming."
}

@Unpublished{HeatherSchneider05a,
  author =       {James A. Heather and Steve A. Schneider},
  title =        {Infinite/Finite ???},
  note =         {Submitted for publication},
  month =        {April},
  year =         2005
}

@Article{Hellman79,
  author =       "Martin E Hellman",
  title =        "The Mathematics of Public Key Cryptography",
  journal =      "Scientific American",
  year =         1979,
  pages =        "130-139",
  month =        aug
}

@TechReport{HerzogGuttman02,
  author =       {Amy L. Herzog and Joshua D. Guttman},
  title =        {Security Goal Achievement In A Heterogeneous Environment},
  institution =  {The MITRE Corporation},
  year =         2002
}

@Unpublished{HerzogEtAl98,
  author =       {Jonathan Herzog and Joshua Guttman and Fred Chase},
  title =        {A Strand Space Analysis of the {SSH} Version 2 Protocol},
  note =         {{MITRE} Product {MP} 98B0000056},
  month =        {September},
  year =         1998
}

@Unpublished{HerzogEtAl99,
  author =       {Jonathan Herzog and Fred Chase and Joshua Guttman},
  title =        {A Saying-Logic Analysis of core {DNS} Security},
  note =         {{MITRE} Product {MP} 99{B}0000039},
  year =         1999
}

@Unpublished{Herzog00,
  author =       {Jonathan Herzog},
  title =        {Some Security Concerns Regarding {PPP}--{EAP}--{TLS}},
  note =         {{MITRE} Product {MP} 00{B}0000019},
  year =         2000
}

@Unpublished{HerzogEtAl00,
  author =       {Jonathan Herzog and Laura Feinstein and Joshua Guttman},
  title =        {A Strand Space Analysis of {TLS} 1.0},
  note =         {{MITRE} Document {MTR} 0{B}0000011},
  year =         2000
}

@Unpublished{Herzog00b,
  author =       {Jonathan Herzog},
  title =        {Mobile {IP} Security},
  note =         {{MITRE} Product {MP} 00{B}0000063},
  year =         2000
}

@MastersThesis{Herzog02,
  author =       {Jonathan Herzog},
  title =        {Computational Soundness of Formal Adversaries},
  school =       {Massachusetts Institute of Technology},
  year =         2002
}

@InProceedings{Herzog03,
  author =       {Jonathan C. Herzog},
  title =        {The {Diffie-Hellman} Key-Agreement Scheme in the Strand-Space Model},
  booktitle =    {16th Computer Security Foundations Workshop},
  pages =        {234--247},
  year =         2003,
  address =      {Asilomar, CA},
  month =        {June},
  publisher =    {{IEEE CS} Press}
}

@TechReport{HerzogEtAl04,
  author =       {Jonathan Herzog and Brian Sniffen and Jay Carlson and Joshua D. Guttman and John D. Ramsdell},
  title =        {Trust Management with Cryptographic Hardware Assistance},
  institution =  {The MITRE Corp.},
  year =         2003,
  type =         {MTR},
  number =       {03B0082},
  address =      {Bedford, MA},
  month =        {September}
}

@PhdThesis{Herzog04,
  author =       {Jonathan Herzog},
  title =        {Computational Soundess for Standard Assumption of Formal Cryptography},
  school =       {Massachusetts Institute of Technology},
  year =         2004
}

@Misc{Hitchcock53,
  author =       {Alfred Hitchcock},
  title =        {I Confess},
  howpublished = {Warner Brothers},
  month =        {March},
  year =         1953,
  note =         {\url{http://www.imdb.com/title/tt0045897/}}}

@Article{Hoare78,
  author =       {C. A. R. Hoare},
  title =        {Communicating Sequential Processes},
  journal =      {CACM},
  year =         1978,
  volume =       21,
  number =       8,
  pages =        {666--77}
}

@Book{Hoare85,
  author =      "C. A. R. Hoare",
  title =       "Communicating Sequential Processes",
  publisher =   "Prentice-Hall International",
  year =        1985,
  address =     "Englewood Cliffs, New Jersey",
  patron =      "Guttman"
}

@Book{Holzmann91,
  author =       {Gerard Holzmann},
  title =        {Design and Validation of Computer Protocols},
  publisher =    {Prentice Hall},
  year =         1991
}

@Misc{HouselyEtAl99,
  author =       {R. Housley and W. Ford and W. Polk and D. Solo},
  title =        {Internet {X.509} Public Key Infrastructure Certificate and {CRL} Profile},
  howpublished = {{RFC} 2459},
  month =        {January},
  year =         1999
}

@Misc{RFC2459,
  author =       {R. Housley and W. Ford and W. Polk and D. Solo},
  title =        {Internet X.509 Public Key Infrastructure Certificate and CRL Profile},
  howpublished = {{RFC} 2459},
  month =        {January},
  year =         1999
}

@Misc{RFC3280,
  author =       {R. Housley and W. Polk and W. Ford and D. Solo},
  title =        {Internet X.509 Public Key Infrastructure Certificate and CRL Profile},
  howpublished = {{RFC} 3280},
  month =        {April},
  year =         2002
}

@InProceedings{HuiLowe99,
  author =       {Mei Lin Hui and Gavin Lowe},
  title =        {Safe Simplifying Transformations for Security Protocols},
  booktitle =    {12th Computer Security Foundations
                  Workshop Proceedings},
  year =         1999,
  publisher =    {{IEEE} CS Press},
  pages =        {32--43},
  month =        {June}
}

@article{HuiLowe01,
  author    = {Mei Lin Hui and
               Gavin Lowe},
  title     = {Fault-Preserving Simplifying Transformations for Security
               Protocols},
  journal   = {Journal of Computer Security},
  volume    = 9,
  number    = {1/2},
  year      = 2001,
  pages     = {3-46},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{HwangChen95,
   author =       "Tzonelih Hwang and Yung-Hsiang Chen",
   title =        "On the security of {SPLICE/AS}: The
                authentication system in {WIDE Internet}",
   journal =      "Information Processing
                   Letters",
    year =         1995,
    volume =       53,
    pages =        "97--101"
}

@Article{HwangLeeLiKoChen95,
  author =       "Tzonelih Hwang and Narn-Yoh Lee and Chuang-Ming Li
                  and Ming-Yung Ko and Yung-Hsiang Chen",
  title =        "Two Attacks on {Neuman-Stubblebine}
                  Authentication Protocols",
  journal =      "Information Processing Letters",
  year =         1995,
  volume =       53,
  pages =        "103--107"
}

@InProceedings{Integrating01,
  author =       {P. Loscocco and S. Smalley},
  title =        {Integrating Flexible Support for Security Policies into the {Linux} Operating System},
  booktitle =    {Proceedings of the FREENIX Track of the 2001 USENIX Annual Technical Conference},
  year =         2001
}

@Misc{ikev2:id:17,
  author =       {Charlie {Kaufman, ed.}},
  title =        {Internet Key Exchange ({IKEv2}) Protocol},
  howpublished = {Internet Draft},
  month =        {September},
  year =         2004,
  note =         {Available at \url{http://www.ietf.org/internet-drafts/draft-ietf-ipsec-ikev2-17.txt}}
}

@Misc{IPchains00,
  key =          {IPchains00},
  author =       {Rusty Russell},
  title =        {Linux IP Firewalling Chains},
  howpublished = {Linux Howto},
  month =        {October},
  year =         2000,
  note =         {URL~\url{http://www.netfilter.org/ipchains/}}
}

@Misc{IPfilter00,
  key =          {IPfilter00},
  author =       {Darren Reed},
  title =        {IP Filter},
  howpublished = {Download Web Page},
  month =        {December},
  year =         2002,
  note =         {URL~\url{http://coombs.anu.edu.au/~avalon/}}
}

@Manual{ISOIEC9798-1,
  title =        "Information Technology - Security techniques ---
                  Entity Authentication Mechanisms Part 1: General Model",
  organization = "ISO/IEC",
  year =         1991
}

@Manual{ISOIECDIS9798-2,
  title =        "Information Technology - Security techniques ---
                  Entity Authentication Mechanisms Part 2: Entity
                  authentication using symmetric techniques",
  organization = "ISO/IEC",
  year =         1993
}

@Manual{ISOIECDIS9798-3,
  title =        "Information Technology - Security techniques ---
                  Entity Authentication Mechanisms Part 3: Entity
                  authentication using a public key algorithm",
  organization = "ISO/IEC",
  year =         1993
}

@Misc{ITUMSC99,
  author =       {ITU},
  title =        {Message Sequence Chart ({MSC})},
  howpublished = {Recommendation Z.120},
  year =         1999}

@Unpublished{ITTCweb,
  author =       "D. Boneh and T. Raj and M. Malkin and T. Wu",
  title =        "Intrustion Tolerance via Threshold Cryptography",
  note =         "http://crypto.stanford.edu/\~dabo/ITTC"
}

@InProceedings{JiwaSeberryZheng94,
  author =       "A Jiwa and J Seberry and Y Zheng",
  title =        "Beacon Based Authentication",
  editor =       "Dieter Gollmann",
  number =       875,
  series =       "Lecture Notes in Computer Science",
  pages =        "125--142",
  booktitle =    "Computer Security --- {ESORICS} '94",
  year =         1994,
  publisher =    "Springer"
}

@Article{Jones83,
  author =       {Cliff B. Jones},
  title =        {Tentative Steps toward a Development Method for Interfering Programs},
  journal =      {{ACM} Transactions on Programming Languages and Systems},
  year =         {1983},
  OPTkey =       {},
  OPTvolume =    {5},
  OPTnumber =    {4},
  OPTpages =     {596--619},
  OPTmonth =     {},
  OPTnote =      {},
  OPTannote =    {}
}

@Unpublished{JurjensWimmel01,
  author = {Jan {J{\"u}rjens} and Guido Wimmel},
  title =        {Specification-Based Testing of Firewalls},
  note =         {Submitted for publication},
  year =         {2001},
}

@InProceedings{KailarGligor91,
  author =       "R. Kailar and Virgil D. Gligor",
  title =        "On Belief Evolution in Authentication Protocols",
  pages =        "103--116",
  booktitle =    "Proceedings of the Computer Security Foundations
                  Workshop IV",
  year =         1991,
  publisher =    "IEEE CS Press"
}

@article{kaliski2001unknown,
  title={{An unknown key-share attack on the MQV key agreement protocol}},
  author={Burton S. Kaliski},
  journal={{ACM} Transactions on Information and System Security},
  volume=4,
  number=3,
  pages={275--288},
  issn={1094-9224},
  year=2001,
  publisher={ACM}
}

@article{kapur2003unification,
  title={{An E-unification algorithm for analyzing protocols that use modular exponentiation}},
  author={Deepak Kapur and Paliath Narendran and Lida Wang},
  journal={Rewriting Techniques and Applications},
  year={2003},
  publisher={Springer}
}

@article{DBLP:journals/joc/KatzY07,
  author    = {Jonathan Katz and
               Moti Yung},
  title     = {Scalable Protocols for Authenticated Group Key Exchange},
  journal   = {J. Cryptology},
  volume    = {20},
  number    = {1},
  year      = {2007},
  pages     = {85-113},
  ee        = {http://dx.doi.org/10.1007/s00145-006-0361-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{KehneSchoenwalderLangendorfer92,
  author =       "A. Kehne and J. Sch{\"{o}}enw{\"{a}}lder and H.
                  Langend{\"{o}}rfer",
  title =        "A Nonce-Based Protocol for Multiple Authentication",
  journal =      "Operating Systems Review",
  year =         1992,
  volume =       26,
  number =       4,
  pages =        "84--89"
}

@InProceedings{KelseySchneierWagner97,
  author = "John Kelsey and Bruce Schneier and David Wagner",
  title = " Protocol Interactions and the Chosen Protocol Attack",
  booktitle = "Security Protocols Workshop",
  year = 1998,
  ignorepages = "91--104",
  publisher = "Springer"
}

@InProceedings{Kemmerer87,
  author =       "R. A. Kemmerer",
  title =        "Using Formal
                  Verification Techniques to Analyse Encryption Protocols",
  pages =        "134--139",
  booktitle =    "Proceedings of the 1987 IEEE Symposium on Research
                  in Security and Privacy",
  year =         1987,
  publisher =    "IEEE CS Press"
}

@Article{Kemmerer89,
  author =       "R. A. Kemmerer",
  title =        "Analysing Encryption Protocols Using Formal
                  Verification Techniques",
  journal =      "IEEE Journal on Selected Areas in Communications",
  year =         1989,
  volume =       7,
  number =       4,
  pages =        "448--457"
}

@InProceedings{KesslerWedel94,
  author =       "V. Kessler and G. Wedel",
  title =        "AUTLOG --- An advanced logic of authentication",
  pages =        "90--99",
  booktitle =    "Proceedings of the Computer Security Foundations
                  Workshop VII",
  year =         1994
}

@InProceedings{Kocher96,
  author =       "Paul C. Kocher",
  title =        "Timing Attacks on Implementations of {Diffie-Hellman}, {RSA}, {DSS}, and Other Systems",
  pages =        "104--113",
  editor =       "Neal Koblitz",
  number =       1109,
  series =       "Lecture Notes in Computer Science",
  booktitle =    "Advances in Cryptology --- {CRYPTO} '96",
  year =         1996,
  publisher =    "Springer"
}

@inproceedings{KlayVigneron08,
  author    = {Francis Klay and
               Laurent Vigneron},
  title     = {Automatic Methods for Analyzing Non-repudiation Protocols
               with an Active Intruder},
  booktitle = {Formal Aspects in Security and Trust},
  year      = {2008},
  pages     = {192-209},
  ee        = {http://dx.doi.org/10.1007/978-3-642-01465-9_13},
  crossref  = {DBLP:conf/ifip1-7/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{KocherJaffeJun99,
  author =       "Paul Kocher and Joshua Jaffe and Benjamin Jun",
  title =        "Differential Power Analysis",
  journal =      "Lecture Notes in Computer Science",
  volume =       "1666",
  pages =        "388--397",
  year =         "1999"
}

@Misc{KohlNeuman93,
  author= "J. Kohl and C. Neuman",
  title=  "The {Kerberos} Network Authentication Service (V5)",
  howpublished="{RFC} 1510",
  month=sep,
  year= 1993
}

@Misc{RFC1510,
  author= "J. Kohl and C. Neuman",
  title=  "The {Kerberos} Network Authentication Service (V5)",
  howpublished="{RFC} 1510",
  month=sep,
  year= 1993
}

@InProceedings{KommerlingKuhn99,
  author =       "Oliver K{\"{o}}mmerling and Markus G. Kuhn",
  title =        "Design Principles for Tamper-Resistant Smartcard Processors",
  pages =        "9--20",
  booktitle =    "Proceedings of the USENIX Workshop on Smartcard Technology",
  year =         1999
}

@conference{krawczyk2005hmqv,
  title={{HMQV: A high-performance secure {Diffie-Hellman} protocol}},
  author={Krawczyk, H.},
  booktitle={Advances in Cryptology--CRYPTO 2005},
  pages={546--566},
  year={2005},
  organization={Springer}
}

@InProceedings{KremerRaskin02,
  author =       {Steve Kremer and Jean-Fran{\c{c}}ois Raskin},
  title =        {Game Analysis of Abuse-Free Contract Signing},
  booktitle =    {Proceedings, 15th Computer Security Foundations
                  Workshop},
  year =         2002,
  month =        {June},
  publisher =    {{IEEE} CS Press}
}

@InProceedings{kuesters2009using,
  title={Using {ProVerif} to analyze protocols with {Diffie-Hellman} exponentiation},
  author={Ralf K{\"u}sters and Tomasz Truderung},
  booktitle={{IEEE} Computer Security Foundations Symposium},
  pages={157--171},
  issn={1063-6900},
  year=2009,
  organization={IEEE}
}

@inproceedings{kusters2011composition,
  title={Composition theorems without pre-established session identifiers},
  author={K{\"u}sters, R. and Tuengerthal, M.},
  booktitle={CCS},
  pages={41--50},
  year={2011},
  organization={ACM}
}

@article{kunz2006security,
  title={{About the Security of MTI/C0 and MQV}},
  author={Sebastian Kunz-Jacques and David Pointcheval},
  journal={Security and Cryptography for Networks},
  pages={156--172},
  year={2006},
  publisher={Springer}
}

@Article{LadkinLeue94,
  author =       {Peter B. Ladkin and Stefan Leue},
  title =        {Interpreting Message Flow Graphs},
  journal =      {Formal Aspects of Computing},
  year =         1994,
  volume =       3,
  number =       1
}

@InProceedings{LakhnechEtAl03,
  author =       {L. Bozga and Y. Lakhnech and M. Perin},
  title =        {Pattern-based Abstraction for Verifying Secrecy in Protocols},
  booktitle = {Tools and Algorithms for Construction and Analysis of Systems {(TACAS)}},
  year =         2003,
  number =       2619,
  series =       {LNCS},
  publisher = {Springer}}

@article{lamacchia2007stronger,
  title={Stronger security of authenticated key exchange},
  author={LaMacchia, B. and Lauter, K. and Mityagin, A.},
  journal={Provable Security},
  volume = 4784,
  series =       {LNCS},
  note = {DOI: \url{dx.doi.org/10.1007/978-3-540-75670-5_1}},
  year=2007,
  publisher={Springer}
}

@Article{Lamport78,
  author =       {Leslie Lamport},
  title =        {Time, clocks and the ordering of events in a
distributed system},
  journal =      {CACM},
  year =         1978,
  volume =       21,
  number =       7,
  pages =        {558–-565}}

@Article{LampsonEtAl92,
  author =       {Butler Lampson and Mart{\'\i}n Abadi and Michael Burrows and Edward Wobber},
  title =        {Authentication in  Distributed Systems:  Theory and Practice},
  journal =      {{ACM} Transactions on  Computer Systems},
  year =         1992,
  volume =       10,
  number =       4,
  pages =        {265--310},
  month =        {November}
}

@article{law2003efficient,
  title={{An efficient protocol for authenticated key agreement}},
  author={Law, L. and Menezes, A. and Qu, M. and Solinas, J. and Vanstone, S.},
  journal={Designs, Codes and Cryptography},
  volume={28},
  number={2},
  pages={119--134},
  issn={0925-1022},
  year={2003},
  publisher={Springer}
}

@Manual{Leroy00,
  title =        {The Objective Caml System},
  author =       {Xavier Leroy and Damien Doligez and Jacques Garrigue and Didier R\'emy and J\'er\^ome Vouillon},
  organization = {{INRIA}},
  address =      {\texttt{http://caml.inria.fr/}},
  note =         {Version 3.00},
  year =         2000
}

@Misc{LeroyCryptokit05,
  author =       {Xavier Leroy},
  title =        {Cryptokit},
  howpublished = {Sofwtare available via \url{http://pauillac.inria.fr/~xleroy/software.html}},
  month =        {April},
  year =         2005,
  note =         {Version 1.3}
}

@article{li2012secure,
  author = 	 {Ming Li and Sucheng Yu and Joshua D. Guttman and
                  Wenjing Lou and Kui Ren},
  title = 	 {Secure ad-hoc trust initialization and key management in
    wireless body area networks},
  journal = 	 {ACM Transactions on Sensor
    Networks (TOSN)},
  volume    = 9,
  number    = 2,
  pages     = 18,
  year      = 2013
}

@InProceedings{LiEtAl02,
  author =       {Ninghui Li and John C. Mitchell and William H. Winsborough},
  title =        {Design of a Role-Based Trust Management Framework},
  booktitle =    {Proceedings, 2002 IEEE Symposium on Security and Privacy},
  year =         2002,
  organization = {May},
  pages =        {114--130},
  publisher =    {IEEE CS Press}
}

@InProceedings{LiEtAl03a,
  author =       {Ninghui Li  and William H. Winsborough and John C. Mitchell},
  title =        {Beyond Proof-of-Compliance: Safety and Availability Analysis on Trust Management},
  booktitle =    {Proceedings, 2003 IEEE Symposium on Security and Privacy},
  year =         2003,
  organization = {May},
  publisher =    {IEEE CS Press}
}

@Article{LiEtAl03,
  author =       {Ninghui Li and William H. Winsborough and John C. Mitchell},
  title =        {Distributed Credential Chain Discovery in Trust Management},
  journal =      {Journal of Computer Security},
  year =         2003,
  month =        feb,
  volume =       11,
  number =       1,
  pages =        {35--86}
}

@Article{Liebl93,
  author =       "Armin Liebl",
  title =        "Authentication in Distributed Systems: A Bibliography",
  journal =      "Operating Systems Review",
  year =         1993,
  volume =       27,
  number =       4,
  pages =        "122--136",
  month =        oct
}

@Article{Lowe95,
   author =      "Gavin Lowe",
   title =       "An Attack on the {Needham-Schroeder}
                    Public Key  Authentication Protocol",
   journal =     "Information Processing   Letters",
   year =        1995,
   volume =      56,
   number =      3,
   pages =       "131--136",
   month =       nov
}

@InProceedings{Lowe96,
  author =       {Gavin Lowe},
  title =        {Some New Attacks upon Security Protocols},
  booktitle =    {Proceedings of the Computer Security Foundations
                  Workshop IX},
  year =         1996,
  publisher =    {{IEEE} CS Press}
}

@InProceedings{Lowe96a,
  author =       {Gavin Lowe},
  title =        {Breaking and Fixing the {Needham-Schroeder} Public-Key
                  Protocol using {FDR}},
  booktitle =    {Proceeedings of {\sc tacas}},
  volume =       1055,
  series =       {LNCS},
  year =         1996,
  pages =        {147--166}
}

@InProceedings{Lowe97,
  author =       {Gavin Lowe},
  title =        {A Hierarchy of Authentication Specifications},
  booktitle =    {10th Computer Security Foundations
                  Workshop Proceedings},
  year =         1997,
  publisher =    {{IEEE} CS Press},
  pages =        {31--43}
}

@InProceedings{Lowe97a,
  author =       {Gavin Lowe},
  title =        {Casper:  A Compiler for the Analysis of Security Protocols},
  booktitle =    {10th Computer Security Foundations
                  Workshop Proceedings},
  year =         1997,
  publisher =    {{IEEE} CS Press},
  pages =        {18--30}
}

@InProceedings{Lowe98,
  author =       {Gavin Lowe},
  title =        {Toward a Completeness Result for Model Checking of Security Protocols},
  booktitle =    {11th Computer Security Foundations
                  Workshop Proceedings},
  year =         1998,
  publisher =    {{IEEE} CS Press},
  pages =        {96--105}
}

@InProceedings{Lowe02,
  author =       {Gavin Lowe},
  title =        {Analyzing Protocols subject to Guessing Attacks},
  booktitle =    {WITS:  Workshop on Issues in the Theory of Security},
  year =         2002,
  month =        {January},
  note =         {Available at http://www.dsi.unive.it/IFIPWG1\_7/wits2002.html}
}

@Article{Lowe03,
  author =       {Gavin Lowe},
  title =        {Analyzing Protocols subject to Guessing Attacks},
  journal =      {Journal of Computer Security},
  year =         2003,
  note =         {Forthcoming}
}

@TechReport{LoweAuty07,
  author =       {Gavin Lowe and Michael Auty},
  title =        {A Calculus for Security Protocol Development},
  institution =  {Oxford University Computing Laboratory},
  year =         2007,
  month =        {March}}

@InProceedings{WuMalkinBoneh99,
  author =       "T. Wu and M. Malkin and D. Boneh",
  title =        "Building Intrusion Tolerant Applications",
  pages =        "79--91",
  booktitle =    "Proceedings of the 8th USENIX Security Symposium",
  year =         1999
}

@InProceedings{MalkinWuBoneh99,
  author =       "M. Malkin and T. Wu and D. Boneh",
  title =        "Experimenting with Shared Generation of RSA Keys",
  pages =        "43--56",
  booktitle =    "Proceedings of the Internet Society's 1999 Symposium on Network and Distributed System Security (SNDSS)",
  year =         1999
}

@InProceedings{MaoBoyd93,
  author =       "Wenbo Mao and Colin Boyd",
  title =        "Towards the Formal Analysis of Security Protocols",
  pages =        "147--158",
  booktitle =    "Proceedings of the Computer Security Foundations
                  Workshop VI",
  year =         1993,
  publisher =    "IEEE CS Press"
}

@InProceedings{Maneki99,
  author =       {Al Maneki},
  title =        {Honest functions and their Application to the Analysis of
Cryptographic Protocols},
  booktitle =    {Proceedings of the 12th Computer Security Foundations
                  Workshop},
  year =         1999,
  month =        {June},
  publisher =    {IEEE CS Press}
}

@InProceedings{MaoBoyd94a,
  author =       "Wenbo Mao and Colin Boyd",
  title =        "Development of Authentication Protocols: Some
                  Misconceptions and a New Approach",
  booktitle =    "Proceedings 7th Computer Security Foundations Workshop",
  publisher =    "IEEE CS Press",
  year =         1994,
  pages =        "178--186"
}

@InProceedings{MaoBoyd94b,
  author =       "Wenbo Mao and Colin Boyd",
  title =        "On Strengthening Authentication protocols
                  to Foil Cryptanalysis",
  editor =       "Dieter Gollmann",
  number =       875,
  series =       "Lecture Notes in Computer Science",
  pages =        "193--204",
  booktitle =    "Computer Security---ESORICS 94",
  year =         1994,
  publisher =    "Springer",
  month =        nov
}

@InProceedings{MarreroEtAl97,
  author =       {Will Marrero and Edmund Clarke and Somesh Jha},
  title =        {A Model Checker for Authentication Protocols},
  booktitle =    {Proceedings of the {DIMACS} Workshop on Design and Verification of Security Protocols},
  year =         1997,
  editor =       {Cathy Meadows and Hilary Orman},
  month =        {September},
  organization = {{DIMACS}, Rutgers University}
}

@Article{MaurerMassey93,
  author =       {Ueli Maurer and James Massey},
  title =        {Cascade Ciphers: The Importance of Being First},
  journal =      {Journal of Cryptology},
  year =         1993,
  volume =       6,
  number =       1,
  pages =        {55-61}
}

@Article{Massey88,
  author =       "James L. Massey",
  title =        "An Introduction to Contemporary Cryptology",
  journal =      "Proceedings of the IEEE",
  year =         1988,
  volume =       76,
  number =       5,
  pages =        "533-549",
  month =        may
}

@Article{Meadows92,
  author =       "Catherine Meadows",
  title =        "Applying Formal Methods to the Analysis of a Key
                  Management Protocol",
  journal =      "Journal of Computer Security",
  year =         1992,
  volume =       1,
  number =       1,
  pages =        "5--35",
  ISSN =         "0926-227X"
}

@article{meadows1996nrl,
  title={The {NRL} protocol analyzer: An overview},
  author={Meadows, C.},
  journal={The Journal of Logic Programming},
  volume={26},
  number={2},
  pages={113--131},
  year={1996},
  publisher={Elsevier}
}

@InProceedings{MayerEtAl00,
  author =       {Alain Mayer and Avishai Wool and Elisha Ziskind},
  title =        {Fang:  A Firewall Analysis Engine},
  booktitle =    {Proceedings, {IEEE} Symposium on Security and Privacy},
  pages =        {177--187},
  year =         2000,
  month =        {May},
  publisher =    {IEEE CS Press}
}

@InProceedings{Meadows94,
  author =       {Catherine Meadows},
  title =        {A Model of Computation for the {NRL} Protocol Analyzer},
  booktitle =    {Proceedings of the Computer Security Foundations
                  Workshop VII},
  year =         1994,
  organization = {{IEEE}},
  publisher =    {{IEEE} CS Press},
  pages =        {84--89}
}

@InProceedings{Meadows99,
  author =       {Catherine Meadows},
  title =        {Analysis of the {Internet} {Key} {Exchange} Protocol using the {NRL} Protocol Analyzer},
  booktitle =    {Proceedings, 1999 IEEE Symposium on Security and Privacy},
  year =         1999,
  month =        {May},
  publisher =    {IEEE CS Press}
}

@InProceedings{Meadows00,
  author =       {Catherine Meadows},
  title =        {Open Issues in Formal Methods for Cryptographic Protocol Analysis},
  booktitle =    {{DISCEX} Workshop},
  year =         2000,
  month =        {January},
  organization = {DARPA}
}

@InProceedings{Meadows00a,
  author =       {Catherine Meadows},
  title =        {Invariant Generation Techniques in Cryptographic Protocol Analsyis},
  booktitle =    {Proceedings, 13th Computer Security Foundations
                  Workshop},
  year =         2000,
  month =        {July},
  publisher =    {{IEEE} CS Press}
}

@inproceedings{cervesato2005encapsulated,
  title={An encapsulated authentication logic for reasoning about key distribution protocols},
  author={Cervesato, I. and Meadows, C. and Pavlovic, D.},
  booktitle={Computer Security Foundations, 2005. CSFW-18 2005. 18th IEEE Workshop},
  pages={48--61},
  year={2005},
  organization={IEEE}
}

@article{pavlovic2006deriving,
  title={Deriving secrecy in key establishment protocols},
  author={Pavlovic, D. and Meadows, C.},
  journal={Computer Security--ESORICS 2006},
  pages={384--403},
  year={2006},
  publisher={Springer}
}

@book{menezes2005another,
  title={{Another look at HMQV}},
  author={Menezes, A. and University of Waterloo. Dept. of Combinatorics and Optimization and University of Waterloo. Faculty of Mathematics},
  year={2005},
  publisher={Citeseer}
}

@Article{menezes2007another,
  author =       {Alfred Menezes},
  title =        {Another look at {HMQV}},
  journal =      {Journal of Mathematical Cryptology},
  year =         2007,
  volume =       1,
  pages =        {47--64}
}

@Article{MillenClarkFreedman87,
  author =       "J. K. Millen and S. C. Clark and S. B. Freedman",
  title =        "The {Interrogator}: Protocol Security Analysis",
  journal =      "IEEE Transactions on Software Engineering",
  year =         1987,
  volume =       13,
  number =       2,
  pages =        "274--288",
  month =        feb
}

@InProceedings{Millen95,
  author =       {Jonathan K. Millen},
  title =        {The {Interrogator} Model},
  booktitle =    {Proceedings of the 1995 IEEE Symposium on Security and
                  Privacy},
  year =         1995,
  pages =        {251--60}
}

@Article{Millen03,
  author =       {Jonathan K. Millen},
  title =        {On the Freedom of Encryption},
  journal =      {Information Processing Letters},
  year =         2003,
  volume =       86,
  number =       6,
  pages =        {329--333}
}

@TechReport{MillenMuller01,
  author =       {Jonathan Millen and Frederic Muller},
  title =        {Cryptographic Protocol Generation from {CAPSL}},
  institution =  {{SRI} International},
  year =         2001,
  number =       {SRI-CSL-01-07},
  month =        {December}
}

@InProceedings{MillenRuess00,
  author =       {Jonathan K. Millen and Harald Ruess},
  title =        {Protocol-Independent Secrecy},
  booktitle =    {Proceedings, 2000 IEEE Symposium on Security and
                  Privacy},
  year =         2000,
  month =        {May},
  publisher =    {IEEE CS Press}
}

@InProceedings{MillenShmatikov01,
  author =       {Jonathan K. Millen and  Vitaly Shmatikov},
  title =        {Constraint Solving for Bounded-Process Cryptographic Protocol Analysis},
  booktitle =    {CCS},
  pages =        {166--175},
  year =         2001,
  organization = {ACM}
}

@TechReport{MillerNeumanSchillerSaltzer87,
  author =       "S. P. Miller and C. Neuman and J. I. Schiller and
                  Jerry H. Saltzer",
  title =        "Project Athena Technical Plan (Section E.2.1)",
  institution =  "MIT",
  year =         1987,
  month =        jul
}

@Book{Milner89,
  author =       "Robin Milner",
  title =        "Communication and Concurrency",
  publisher =    "Prentice-Hall International",
  year =         1989,
  address =      "Englewood Cliffs",
  patron =      "Guttman"
}

@InProceedings{Minear95,
  author =       "Spencer E. Minear",
  title =        "Providing Policy Control Over Object Operations in a Mach Based System",
  booktitle =    "Proceedings of the Fifth USENIX UNIX Security Symposium",
  pages =        "141--156",
  year =         1995,
  month =        "June"
}

@Misc{Mockapetris87,
  author =       {P. Mockapetris},
  title =        {Domain Names - Concepts and Facilities},
  howpublished = {{RFC} 1034},
  month =        {November},
  year =         1987
}

@Misc{RFC1034,
  author =       {P. Mockapetris},
  title =        {Domain Names - Concepts and Facilities},
  howpublished = {{RFC} 1034},
  month =        {November},
  year =         1987
}

@Misc{Mockapetris87a,
  author =       {P. Mockapetris},
  title =        {Domain Names - Implementation and Specification},
  howpublished = {{RFC} 1035},
  month =        {November},
  year =         1987
}

@Misc{RFC1035,
  author =       {P. Mockapetris},
  title =        {Domain Names - Implementation and Specification},
  howpublished = {{RFC} 1035},
  month =        {November},
  year =         1987
}

@article{modersheim2009secure,
  title={Secure pseudonymous channels},
  author={M{\"o}dersheim, S. and Vigan{\`o}, L.},
  journal={ESORICS},
  pages={337--354},
  year={2009},
  series={LNCS}
}

@Article{Moore88,
  author =       "Judy H. Moore",
  title =        "Protocol Failures in Cryptosystems",
  journal =      "Proceedings of the IEEE",
  year =         1988,
  volume =       76,
  number =       5,
  month =        may
}

@InProceedings{MooreAndersonKuhn00,
  author =       "S. Moore and R. Anderson and M. Kuhn",
  title =        "Improving Smartcard Security using Self-Timed Circuit Technology",
  booktitle =    "Fourth AciD-WG Workshop",
  year =         2000
}

@InProceedings{MooreEtAl02,
  author =       "Simon Moore and Ross Anderson and Paul Cunningham and Robert Mullins and George Taylor",
  title =        "Improving Smart Card Security using Self-Timed Circuits",
  booktitle =    "Eigth International Symposium on Advanced Research in Asynchronous Circuits and Systems",
  year =         2002
}

@InProceedings{Moser89,
  author =       "Louise E. Moser",
  title =        "A Logic of Knowledge and Belief about Computer Security",
  editor =       "J Thomas Haigh",
  pages =        "57--63",
  booktitle =    "Proceedings of the Computer Security Foundations
                  Workshop III",
  organization = "IEEE",
  publisher =    "CS Press of the IEEE",
  year =         1989
}

@InProceedings{MitchellEtAl97,
  author =       {John C. Mitchell and Mark Mitchell and Ulrich Stern},
  title =        {Automated Analysis of Cryptographic Protocols using {Mur}$\varphi$},
  booktitle =    {Proceedings, 1997 IEEE Symposium on Security and Privacy},
  pages =        {141--151},
  year =         1997,
  organization = {IEEE},
  publisher =    {CS Press of the IEEE}
}

@InProceedings{MostrousEtAl09,
  author =       {Dimitris Mostrous and Nobuko Yoshida and Kohei Honda},
  title =        {Global principal typing in partially commutative
asynchronous sessions},
  booktitle = {{ESOP} Proceedings},
  year =         2009,
  series =       {LNCS},
  month =        {March}}

@Misc{rfc2560,
  author =       {M.Myers and R.Ankney and A.Malpani and S.Galperin and C. Adams},
  title =        {X.509 Internet Public Key Infrastructure: Online Certificate Status Protocol - OCSP},
  howpublished = {Internet Request for Comments 2560},
  month =        {June},
  year =         1999,
  note =         {Available at \texttt{http://www.ietf.org/rfc/rfc2560.txt}}
}

@Article{NeedhamSchroeder78,
  author =       "Roger Needham and Michael Schroeder",
  title =        "Using Encryption for Authentication in Large
                  Networks of Computers",
  journal =      "{CACM}",
  year =         1978,
  volume =       21,
  number =       12,
  pages=         {993--999},
  month =        dec
}

@Article{NeedhamSchroeder87,
  author =       "Roger M. Needham and M. D. Schroeder",
  title =        "Authentication Revisited",
  journal =      "Operating Systems Review",
  year =         1987,
  volume =       21,
  number =       7,
  pages =        "7--7",
  month =        jan
}

@Article{Nessett90,
  author =       "Daniel M. Nessett",
  title =        "A Critique of the {Burrows}, {Abadi} and {Needham} Logic",
  journal =      "ACM Operating Systems Review",
  year =         1990,
  volume =       24,
  number =       2,
  pages =        "35--38",
  month =        apr
}

@Article{NeumanStubblebine93,
  author =       "B. Clifford Neuman and Stuart G. Stubblebine",
  title =        "A Note on the Use of Timestamps as Nonces",
  journal =      "Operating Systems Review",
  year =         1993,
  volume =       27,
  number =       2,
  pages =        "10--14",
  month =        apr
}

@Article{Ng03,
  author =       {Siaw-Lynn Ng},
  title =        {Posets and protocols:  Picking the right three-party protocol},
  journal =      {{IEEE} Journal on Selected Areas in Communication},
  month =        {January},
  pages =        "55--61",
  year =         2003
}

@Misc{NuSMV01,
  key =          {NuSMV},
  title =        {{NuSMV}: a new symbolic model checker},
  howpublished = {URL \url{http://sra.itc.it/tools/nusmv}},
  year =         2001
}

@InProceedings{OlawskyEtAl96,
  author =       "D. Olawsky and T. Fine and E. Schneider and R. Spencer",
  title =        "Developing and Using a Policy Neutral Access Control Policy",
  booktitle =    "Proceedings of the New Security Paradigms Workshop",
  year =         1996,
  month =        "September"
}

@InProceedings{Ottawa01,
  author =       {P. Loscocco and S. Smalley},
  title =        {Meeting Critical Security Objectives with Security-Enhanced {Linux}},
  booktitle =    {Proceedings of the 2001 Ottawa Linux Symposium},
  year =         2001
}

@Article{OtwayRees87,
  author =       "D. Otway and O. Rees",
  title =        "Efficient and Timely Mutual Authentication",
  journal =      "Operating Systems Review",
  year =         1987,
  volume =       21,
  number =       1,
  pages =        "8--10",
  month =        jan
}

@Misc{PCKS1,
  author =       {{RSA} Laboratories},
  title =        {{PCKS} \#1: {RSA} Encryption Standard},
  month =        {November},
  year =         1993,
  note =         {Version 1.5}
}

@InProceedings{Patel97,
  author =       {Sarvar Patel},
  title =        {Number Theoretic Attacks on Secure Password Schemes},
  booktitle =    {Proceedings of the 1997 {IEEE} Symposium on Security and
                  Privacy},
  pages =        {236--247},
  year =         1997,
  month =        {May},
  publisher =    {{IEEE} CS Press}
}

@Book{Paulson94,
  author =       {L. C. Paulson},
  title =        {Isabelle:  A Generic Theorem Prover},
  publisher =    {Springer Verlag},
  year =         1994,
  number =       828,
  series =       {LNCS}
}

@InProceedings{Paulson97,
  author =       {Lawrence C. Paulson},
  title =        {Proving Properties of Security Protocols by Induction},
  booktitle =    {10th {IEEE} Computer Security Foundations Workshop},
  year =         1997,
  publisher =    {IEEE CS Press},
  pages =        {70--83}
}

@InProceedings{Paulson97a,
  author =       {Lawrence C. Paulson},
  title =        {Mechanized Proofs of a Recursive Authentication Protocol},
  booktitle =    {10th {IEEE} Computer Security Foundations Workshop},
  year =         1997,
  publisher =    {IEEE CS Press},
  pages =        {84--94}
}

@TechReport{Paulson97b,
  author =       {Lawrence C. Paulson},
  title =        {On Two Formal Analyses of the {Yahalom} Protocol},
  institution =  {Cambridge University Computer Laboratory},
  year =         1997,
  number =       432,
  month =        {July},
  annote =       {http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html}
}

@Article{Paulson97c,
  author =       {Lawrence C. Paulson},
  title =        {Relations between secrets: Two Formal Analyses of the {Yahalom} Protocol},
  journal =      {Journal of Computer Security},
  year =         2001,
  annote =       {http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html}
}

@Article{Paulson97d,
  author =       {Lawrence C. Paulson},
  title =        {Relations between secrets: Two Formal Analyses of the {Yahalom} Protocol},
  journal =      {Journal of Computer Security},
  year =         2001,
  note =         {Also available as Cambridge University Computer Laboratory Technical Report 432 (1997)},
  annote =       {http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html}
}

@Article{Paulson98,
  author =       {Lawrence C. Paulson},
  title =        {The Inductive Approach to Verifying Cryptographic Protocols},
  journal =      {Journal of Computer Security},
  year =         1998,
  note =         {Also Report 443, Cambridge University Computer Lab},
  annote =       {From http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html}
}

@Article{Paulson99,
  author =       {Lawrence C. Paulson},
  title =        {Inductive analysis of the {Internet} protocol {TLS}},
  journal =      {ACM Transactions on Computer and System Security},
  year =         1999,
  annote =       {From http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html}
}

@Article{PfitzmannEtAl00,
  author =       {Birgit Pfitzmann and Matthias Schunter and Michael Waidner},
  title =        {Cryptographic Security of Reactive Systems},
  journal =      {Electronic Notes in Theoretical Computer Science},
  year =         2000,
  volume =       32
}

@InProceedings{PfitzmannSchunterWaidner1998,
  Author =       {Birgit Pfitzmann and Matthias Schunter and Michael
                  Waidner},
  Title =        {Optimal Efficiency of Optimistic Contract Signing},
  BookTitle =    {Seventeenth Annual {ACM} Symposium on Principles of
                  Distributed Computing},
  Pages =        {113--122},
  Address =      {New York},
  Organization = {ACM},
  month =        may,
  added-by =     {aso},
  year =         1998,
}

@InProceedings{PfitzmannWaidner00,
  author =       {Birgit Pfitzmann and Michael Waidner},
  title =        {Composition and Integrity Preservation of Secure Reactive Systems},
  booktitle =    {Proceedings, Seventh ACM Conference of Communication and Computer Security},
  year =         2000,
  month =        {November},
  organization = {{ACM}}
}

@InProceedings{PfitzmannWaidner01,
  author =       {Birgit Pfitzmann and Michael Waidner},
  title =        {A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission},
  booktitle =    {Proceedings, 2001 IEEE Symposium on Security and Privacy},
  year =         2001,
  month =        May,
  publisher =    {{IEEE CS} Press},
  url = "citeseer.nj.nec.com/pfitzmann00model.html",
  note =         {Preprint at \url{http://iacr.org/2000/066.ps.gz}}
}

@Book{Prawitz65,
  author =       {Dag Prawitz},
  title =        {Natural Deduction:  A Proof-Theoretic Study},
  publisher =    {Almqvist and Wiksel},
  year =         1965,
  address =      {Stockholm}
}

@Unpublished{prover9,
  author = 	 {Bill W. McCune},
  title = 	 {Prover9},
  note = 	 {\url{http://www.cs.unm.edu/~mccune/mace4/}},
  OPTkey = 	 {},
  OPTmonth = 	 {},
  OPTyear = 	 {},
  OPTannote = 	 {}
}

@InProceedings{PurdyEtAl82,
  author =       {G. B. Purdy and G. J. Simmons and J. A. Studier},
  title =        {A Software Protection Scheme},
  booktitle =    {1982 IEEE Symposium on Security and Privacy},
  year =         1982,
  pages =        {99--103}
}

@Book{PearsonEtAl03,
  author =       {Boris Balacheff and Liqun Chen and Siani Pearson and David Plaquin and Graeme Proudler},
  title =        {Trusted Computing Platforms: {TCPA} Technology in Context},
  publisher =    {Prentice Hall PTR},
  year =         2003,
  address =      {Upper Saddle River, NJ}
}

@InProceedings{QuisquaterSamyde01,
  author =       "J.J. Quisquater and D. Samyde",
  title =        "ElectroMagnetic Analysis (EMA): Measures and Countermeasures for Smart Cards",
  booktitle =    "International Conference on Research in Smart Cards (E-smart 2001)",
  pages =        "200--210",
  month =        "September",
  year =         2001
}

@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 = 	 {}
}

@Misc{cpsa09,
  author =       {John D. Ramsdell and Joshua D. Guttman},
  title =        {{CPSA}: A cryptographic protocol shapes analyzer},
  booktitle =    {Hackage},
  publisher =    {The MITRE Corporation},
  year =         2009,
  note =         {\url{http://hackage.haskell.org/package/cpsa}}}

@Misc{cpsa16,
  author =       {John D. Ramsdell and Joshua D. Guttman and Moses Liskov},
  title =        {{CPSA}: A cryptographic protocol shapes analyzer},
  booktitle =    {Hackage},
  publisher =    {The MITRE Corporation},
  year =         2016,
  note =         {\url{http://hackage.haskell.org/package/cpsa}}}

@Misc{cpsa17,
  author =       {John D. Ramsdell and Joshua D. Guttman},
  title =        {{CPSA4}: A cryptographic protocol shapes analyzer},
  booktitle =    {Hackage},
  publisher =    {The MITRE Corporation},
  year =         2017,
  note =         {\url{https://github.com/mitre/cpsaexp}}}

@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}}}

@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/}}}

@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{rfc1661,
  author =       {W. Simpson},
  title =        {The Point--to--Point Protocol},
  howpublished = {RFC 1661},
  month =        {July},
  year =         1994
}

@Misc{rfc2420,
  author =       {H. Jummert},
  title =        {The {PPP} Triple--{DES} Encryption Protocol},
  howpublished = {RFC 2420},
  month =        {September},
  year =         1998
}

@Misc{rfc2419,
  author =       {K Sklower and G. Meyer},
  title =        {The {PPP} {DES} Encryption Protocol, Version 2},
  howpublished = {{RFC} 2419},
  month =        {September},
  year =         1998
}

@Misc{rfc1968,
  author =       {G. Meyer},
  title =        {The {PPP} Encryption Control Protocol},
  howpublished = {{RFC} 1968},
  month =        {June},
  year =         1996
}

@Misc{rfc2284,
  author =       {L. Blunk},
  title =        {{PPP} Extensible Authentication Protocol},
  howpublished = {RFC 2284},
  month =        {March},
  year =         1998
}

@Misc{rfc2716,
  author =       {B. Aboba and D. Simon},
  title =        {{PPP} {EAP} {TLS} Authentication Protocol},
  howpublished = {{RFC} 2716},
  month =        {October},
  year =         1999
}

@MANUAL{rfc:2401,
        TITLE = "Security Architecture for the Internet Protocol",
        ORGANIZATION = "{IETF} Network Working Group {RFC} 2401",
        AUTHOR = "S. Kent and R. Atkinson",
        MONTH = "November",
        YEAR = "1998" }

@MANUAL{rfc:2402,
        TITLE = "IP Authentication Header",
        ORGANIZATION = "IETF Network Working Group {RFC} 2402",
        AUTHOR = "S. Kent and R. Atkinson",
        MONTH = "November",
        YEAR = "1998" }

@MANUAL{rfc:2406,
        TITLE = "IP Encapsulating Security Payload",
        ORGANIZATION = "IETF Network Working Group {RFC} 2406",
        AUTHOR = "S. Kent and R. Atkinson",
        MONTH = "November",
        YEAR = "1998" }

@MANUAL{rfc:2407,
        TITLE = "The Internet IP Security Domain of Interpretation for ISAKMP",
        ORGANIZATION = "IETF Network Working Group {RFC} 2407",
        AUTHOR = "D. Piper",
        MONTH = "November",
        YEAR = "1998" }

@MANUAL{rfc:2408,
        TITLE = "Internet Security Association and Key Management Protocol (ISAKMP)",
        ORGANIZATION = "IETF Network Working Group {RFC} 2408",
        AUTHOR = "D. Maughan and M. Schertler and M. Schneider and J. Turner",
        MONTH = "November",
        YEAR = "1998" }

@MANUAL{rfc:2409,
        TITLE = "The Internet Key Exchange (IKE)",
        ORGANIZATION = "IETF Network Working Group {RFC} 2409",
        AUTHOR = "D. Harkins and D. Carrel",
        MONTH = "November",
        YEAR = "1998" }

@techreport{Rabin81,
  title={How to exchange secrets by oblivious transfer},
  author={Michael Rabin},
  year={1981},
  institution={Technical Report TR-81, Harvard Aiken Computation Laboratory},
note = "Available at \url{http://eprint.iacr.org/2005/187}"
}

@Article{RivestShamirAdleman78,
  author =       "R. Rivest and A. Shamir and L. Adleman",
  title =        "A Method for Obtaining Digital Signatures and Public
                  Key Cryptosystems",
  journal =      "Communications of the ACM",
  year =         1978,
  volume =       21,
  number =       2,
  pages =        "120--126",
  month =        feb
}

@InCollection{Roscoe94,
  author =       {A. W. Roscoe},
  title =        {Model-Checking {CSP}},
  booktitle =    {A Classical Mind:  Essays in Honour of C. A. R. Hoare},
  publisher =    {Prentice-Hall},
  year =         1994,
  editor =       {A. W. Roscoe}
}

@InProceedings{Roscoe95,
  author =       {A. W. Roscoe},
  title =        {Modeling and Verifying Key-Exchange Protocols Using {CSP} and {FDR}},
  booktitle =    {Proceedings of the 8th {IEEE} Computer Security Foundations
                  Workshop},
  year =         1995,
  pages =        {98--107}
}

@inproceedings{Roscoe1995csp,
  title={{CSP} and Determinism in Security Modelling},
  author={Roscoe, A William},
  booktitle={{IEEE} Security and Privacy},
  pages={114--127},
  year={1995},
  organization={IEEE}
}

@InProceedings{Roscoe96,
  author =       {A. W. Roscoe},
  title =        {Intensional Specifications of Security Protocols},
  booktitle =    {Proceedings of the 9th {IEEE} Computer Security Foundations
                  Workshop},
  year =         1996,
  pages =        {28--38}
}

@Book{Roscoe97,
  author =       {A. W. Roscoe},
  title =        {The Theory and Practice of Concurrency},
  publisher =    {Prentice-Hall},
  year =         1997
}

@InProceedings{RoscoeGoldsmith99,
  author =       {A. W. Roscoe and M. H. Goldsmith},
  title =        {What is Intransitive Noninterference?},
  booktitle =    {12th {IEEE} Computer Security Foundations Workshop},
  pages =        {228--238},
  year =         1999,
  month =        {June},
  publisher =    {{IEEE} {CS} Press}
}

@TechReport{RubinHoneyman93,
  author =       "A. D. Rubin and P. Honeyman",
  title =        "Formal Methods for the Analysis of Authentication Protocols",
  institution =  "CITI",
  year =         1993,
  number =       "Technical report 93--7",
  month =        nov
}

@InProceedings{RubinHoneyman94,
  author =       "A. D. Rubin and P. Honeyman",
  title =        "Nonmonotonic Crytpographic Protocols",
  pages =        "100--115",
  booktitle =    "Proceedings of the Computer Security Foundations
                  Workshop VII",
  year =         1994,
  publisher =    "IEEE CS Press"
}

@inproceedings{RusinowitchTuruani01,
  author    = {Micha{\"e}l Rusinowitch and
               Mathieu Turuani},
  title     = {Protocol Insecurity with Finite Number of Sessions is {NP}-Complete},
  booktitle = {Computer Security Foundations Workshop},
  year      = 2001,
  pages     = {174-},
  ee        = {http://csdl.computer.org/comp/proceedings/csfw/2001/1146/00/11460174abs.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{RusinowitchTuruani03,
  author    = {Micha{\"e}l Rusinowitch and
               Mathieu Turuani},
  title     = {Protocol insecurity with a finite number of sessions, composed
               keys is NP-complete},
  journal   = {Theor. Comput. Sci.},
  volume    = {1-3},
  number    = {299},
  year      = {2003},
  pages     = {451-475},
  ee        = {http://dx.doi.org/10.1016/S0304-3975(02)00490-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{RyanSchneider98,
  author =       {Peter Y. A. Ryan and Steve Schneider},
  title =        {An Attack on {APM}'s Recursive Authentication Protocol---a Cautionary Tale},
  journal =      {Information Processing Letters},
  year =         1998,
  volume =       65
}

@article{RyanSchneider2001,
 author = {Peter Ryan and Steve Schneider},
 title = {Process Algebra and Non-interference},
 journal = {J. Comput. Secur.},
 volume = {9},
 number = {1-2},
 month = jan,
 year = {2001},
 pages = {75--103}
}

@Article{SabelfeldMyers03,
  author =       {Andrei Sabelfeld and Andrew C. Myers},
  title =        {Language-based Information-Flow Security},
  journal =      {{IEEE} Journal on Selected Areas in Communication},
  year =         2003,
  volume =       21,
  number =       1,
  pages =        {5--19},
  month =        {January}
}

@TechReport{Satyanarayanan87,
  author =       "N. Satyanarayanan",
  title =        "Integrating Security in a Large Distributed System",
  institution =  "CMU",
  year =         1987,
  number =       "iCMU-CS-87-179",
  month =        "nov"
}

@InProceedings{Schneider96,
  author =       {Steve Schneider},
  title =        {Security Properties and {CSP}},
  booktitle =    {Proceedings, 1996 {IEEE} Symposium on Security and Privacy},
  pages =        {174--87},
  year =         1996,
  month =        {May},
  publisher =    {{IEEE} CS Press}
}

@InProceedings{Schneider97,
  author =       {Steve Schneider},
  title =        {Verifying Authentication Protocols with {CSP}},
  booktitle =    {Proceedings of the 10th {IEEE} Computer Security Foundations
                  Workshop},
  year =         1997,
  publisher =    {IEEE CS Press},
  pages =        {3--17}
}

@Article{Schneier93,
  author =       "B. Schneier",
  title =        "The IDEA Encryption Algorithm",
  journal =      "Dr. Dobb's Journal",
  year =         1993,
  pages =        "50--56",
  month =        "December"
}

@Book{Schneier94,
  author =       "Bruce Schneier",
  title =        "Applied Cryptography",
  publisher =    "Wiley",
  year =         1994
}

@unpublished{SchneierShostack99,
  author =      "Bruce Schneier and Adam Shostack",
  title =       "Breaking Up Is Hard To Do: Modeling Security Threats for Smart Cards",
  note =        "Counterpane Systems and Netect, Inc., available at http://www.counterpane.com/smart-card-threats.html",
  year =        1999
}

@UNPUBLISHED{FergusonSchneier99,
         AUTHOR = "Niels Ferguson and Bruce Schneier",
         TITLE = "A Cryptographic Evaluation of IPsec",
         NOTE = "Counterpane Internet Security, Inc., available at http://www.counterpane.com/ipsec.html",
         year = 1999
}

@article{Selinger01,
  author    = {Peter Selinger},
  title     = {Models for an adversary-centric protocol logic},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {55},
  number    = {1},
  year      = {2001},
  ee        = {http://www.elsevier.com/gej-ng/31/29/23/83/27/show/Products/notes/index.htt\#007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Misc{SELinux03,
  author =       {{National Security Agency}},
  title =        {Security-Enhanced {Linux}},
  howpublished = {At URL \url{http://www.nsa.gov/selinux/index.html}},
  month =        {April},
  year =         2003
}

@Misc{SetSpec97,
  key =          {SET},
  title =        {{SET} Secure Electronic Transaction Specification},
  month =        {May},
  year =         1997,
  note =         {Available at {http://www.setco.org/download.html}}
}

@TechReport{SELTechRep,
  author =       "P. Loscocco and S. Smalley",
  title =        "Integrating Flexible Support for Security Policies into the Linux Operating System",
  institution =  "NSA, NAI Labs",
  year =         "2001",
  month =        "April"
}

@Unpublished{sendmail01,
  author =       "Franklin Haskell",
  title =        "Confining Sendmail Using Security-Enhanced Linux",
  month =        "October",
  year =         2001
}

@InProceedings{Shamir00,
  author =       "A. Shamir",
  title =        "Protecting Smart Cards from Passive Power Analysis with Detached Power Supplies",
  booktitle =    "CHES 2000, Springer-Verlag",
  year =         2000,
  pages =        "71--77"
}

@TechReport{Shoup99,
  author =       {Victor Shoup},
  title =        {On Formal Models for Secure Key Exchange},
  institution =  {IBM Research},
  year =         1999,
  type =         {Research Report},
  number =       {RZ 3120 (\#93166)},
  month =        Apr,
  day =          19,
  note =         {A revised version 4, dated November 15, 1999, is
                  available from \url{http://www.shoup.net/papers/}}
}

@InProceedings{Simmons85,
  author =       {Gustavus J. Simmons},
  title =        {How to (Selectively) Broadcast a Secret},
  booktitle =    {1985 IEEE Symposium on Security and Privacy},
  year =         1985,
  pages =        {108--113}
}

@Article{Simmons88,
  author =       "G.J. Simmons",
  title =        "How to Insure that Data Aquired to Verify Treaty
                  Compliance are Trustworthy",
  journal =      "Proceedings of the IEEE",
  year =         1988,
  volume =       76,
  number =       5,
  pages =        "621--627",
  month =        "May"
}

@Unpublished{SkoroAnderson02,
  author =       "Sergei Skorobogatov and Ross Anderson",
  title =        "Optical Fault Induction Attacks",
  year =         2002,
  note =         "University of Cambridge, Computer Laboratory. Available at http://www.ftp.cl.cam.ac.uk/ftp/users/rja14/faultpap3.pdf"
}

@Article{SmidBranstad88,
  author =       "Miles E. Smid and Dennis K. Branstad",
  title =        "The Data Encryption Standard: Past and Future",
  journal =      "Proceedings of the IEEE",
  year =         1988,
  volume =       76,
  number =       5,
  pages =        "550--559",
  month =        may
}

@InProceedings{Snekkenes91,
  author =       "Einar Snekkenes",
  title =        "Exploring the BAN Approach to Protocol Analysis",
  pages =        "171--181",
  booktitle =    "1991 IEEE Symposium on Research in Security and Privacy",
  year =         1991,
  publisher =    "IEEE CS Press"
}

@InProceedings{Snekkenes92,
  author =       "E. Snekkenes",
  title =        "Roles in Cryptographic protocols",
  booktitle =    "Proceedings of the 1992 IEEE Symposium  on Security
                  and Privacy",
  year =         1992,
  publisher =    "IEEE CS Press"
}

@InProceedings{Song99,
  author =       {Dawn Xiaodong Song},
  title =        {Athena: a New Efficient Automated Checker for Security Protocol Analysis},
  booktitle =    {Proceedings of the 12th {IEEE} Computer Security Foundations Workshop},
  year =         1999,
  month =        {June},
  publisher =    {{IEEE} CS Press}
}

@InProceedings{PerrigSong00,
  author =       {Adrian Perrig and Dawn Xiaodong Song},
  title =        {Looking for Diamonds in the Desert:  Extending Automatic Protocol Generation to Three-Party Authentication and Key Agreement Protocols},
  booktitle =    {Proceedings of the 13th {IEEE} Computer Security Foundations Workshop},
  year =         2000,
  month =        {July},
  publisher =    {{IEEE} CS Press}
}

@InProceedings{PerrigSong00a,
  author =       {Adrian Perrig and Dawn Xiaodong Song},
  title =        {A First Step Toward the Automatic Generation of Security Protocols},
  booktitle =    {Network and Distributed System Security Symposium},
  year =         2000,
  month =        {February},
  publisher =    {Internet Society}
}

@InProceedings{SpiessensVanRoy05,
  author =       {Fred Spiessens and Peter {Van Roy}},
  title =        {A Practical Formal Model for Safety Analysis in Capability-Based Systems},
  booktitle =    {Trust in Global Computing},
  year =         2005,
  editor =       {Rocco De Nicola and Davide Sangiorgi},
  number =       3705,
  series =       {LNCS},
  publisher =    {Springer}
}

@InProceedings{RamanujamSuresh03,
  author =       {R. Ramanujam and S. P. Suresh},
  title =        {A Decidable Subclass of Unbounded Security Protocol},
  booktitle =    {WITS '03: Workshop on Issues in the Theory of Security},
  pages =        {11--20},
  year =         2003,
  editor =       {R. Gorrieri},
  address =      {Warsaw},
  month =        {April}
}

@incollection{ramanujam2003tagging,
  title={Tagging makes secrecy decidable with unbounded nonces as well},
  author={Ramaswamy Ramanujam and S P Suresh},
  booktitle={FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science},
  pages={363--374},
  year={2003},
  publisher={Springer}
}

@Article{RamanujamSuresh05,
  author =       {R. Ramanujam and S. P. Suresh},
  title =        {Decidability of Context-Explicit Security Protocols},
  journal =      {Journal of Computer Security},
  year =         2005,
  volume =       13,
  number =       1,
  pages =        {135--166},
  note =         {Preliminary version appeared in WITS '03, \emph{Workshop on Issues in the Theory of Security}, Warsaw, April 2003}
}

@Unpublished{Ramsdell12a,
 author =       {John D. Ramsdell},
 title =        {Deducing Security Goals From Shape Analysis Sentences},
 note =         {\url{http://arxiv.org/abs/1204.0480}},
 OPTkey =       {},
 month =        apr,
 year =         2012,
 OPTannote =    {}
}

@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}}}

@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{SegallGuttman08,
  author =       {Ariel Segall and Joshua Guttman},
  title =        {A Strand Space/Multiset Rewriting Model of {TPM}
                  Commands},
  institution =  {The MITRE Corporation},
  year =         2008,
  type =         {MTR},
  number =       080181,
  address =      {Bedford, MA},
  month =        {July}}

@InProceedings{SpencerSmalleyEtAl99,
  author =       "R. Spencer and S. Smalley and P. Loscocco and M. Hibler and D. Anderson and J. Lepreau",
  title =        "The Flask Security Architecture: System Support for Diverse Security Policies",
  booktitle =    "Proceedings of the Eighth USENIX Security Symposium",
  year =         1999,
  month =        "August",
  pages =        "123--139"
}

@InProceedings{Stoller99,
  author =       {Scott Stoller},
  title =        {A Reduction for Automated Verification of Authentication Protocols},
  booktitle =    {Workshop on Formal Methods and Security Protocols},
  year =         1999,
  month =        {July},
  note =         {Available at http://www.cs.indiana.edu/\~{ }stoller/}
}

@Unpublished{Stoller99a,
  author =       {Scott Stoller},
  title =        {A Bound on Attacks on Authentication Protocols},
  note =         {Available at http://www.cs.indiana.edu/\~{ }stoller/},
  month =        {July},
  year =         1999
}

@InProceedings{StubblebineGligor92,
  author =       "Stuart G. Stubblebine and Virgil D. Gligor",
  title =        "On Message Integrity in Cryptographic Protocols",
  pages =        "85-104",
  booktitle =    "Proceedings of the 1992 IEEE Symposium on Research
                  in Security and Privacy",
  year =         1992,
  publisher =    "IEEE"
}

@InProceedings{Sutherland86,
  author =       {David Sutherland},
  title =        {A Model of Information},
  booktitle =    {9th National Computer Security Conference},
  year =         1986,
  organization = {National Institute of Standards and Technology}
}

@InProceedings{Syverson91,
  author =       "Paul Syverson",
  title =        "The Use of Logic in the Analysis of Cryptographic Protocols",
  booktitle =    "Proceedings of the 1991 IEEE Symposium on Security
                  and Privacy",
  publisher =    "IEEE CS",
  year =         1991,
  editor =       "Teresa F. Lunt and John McLean",
  pages =        "156--170",
  month =        may
}

@InProceedings{Syverson94a,
  author =       "Paul Syverson",
  title =        "A Taxonomy Of Replay Attacks",
  pages =        "131--136",
  booktitle =    "Proceedings of the 7th IEEE  Computer Security
                  Foundations Workshop",
  year =         1994,
  publisher =    "IEEE CS Press"
}

@InProceedings{Syverson94b,
  author =       "Paul Syverson",
  title =        "On Key Distribution for Repeated Authentication",
  pages =        "24--30",
  booktitle =    "Operating Systems Review",
  year =         1994
}

@Article{Syverson99,
  author =       {Paul Syverson},
  title =        {Towards a Strand Semantics for Authentication Logic},
  journal =      {Electronic Notes in Theoretical Computer Science},
  year =         1999,
  volume =       20
}

@InProceedings{SyversonMeadows93,
  author =       "Paul Syverson and Catherine Meadows",
  title =        "A Logic language for Specifying Cryptographic
                  Protocol Requirements",
  pages =        "165--177",
  booktitle =    "Proceedings of the 1993 IEEE Symposium on Research
                  in Security and Privacy",
  year =         1993,
  publisher =    "IEEE CS Press",
  month =        May
}

@InCollection{Tarski28,
  author =      "A. Tarski",
  title =       "On some Fundamental Concepts of Metamathematics",
  booktitle =   "Logic, Semantics, Meta-Mathematics",
  publisher =   "Hackett Publishing Company",
  year =        1983,
  editor =      "J. Corcoran",
  chapter =     "III",
  pages =       "30--37"
}

@InCollection{Tarski35,
  author =      "A. Tarski",
  title =       "On the Concept of Logical Consequence",
  booktitle =   "Logic, Semantics, Meta-Mathematics",
  publisher =   "Hackett Publishing Company",
  year =        1983,
  editor =      "J. Corcoran",
  chapter =     "XVI",
  pages =       "409--420"
}

@InProceedings{TatebayashiEtAl90,
  author =       {M. Tatebayashi and N. Matsuzaki and D. Newman},
  title =        {Key Distribution Protocol for Digital Mobile Communication
                  Systems},
  booktitle =    {Advances in Cryptology:  {\sc crypto} '89},
  editor =       {G. Brassard},
  volume =       435,
  series =       {Lecture Notes in Computer Science},
  year =         1990,
  publisher =    {Springer Verlag},
  pages =        {324--331}
}

@TechReport{ThayerHerzogGuttman97,
  author =       {F. Javier {\textsc{Thayer} F\'{a}brega} and Jonathan C. Herzog and Joshua D. Guttman},
  title =        {Strand Spaces},
  institution =  {The {\sc Mitre} Corporation},
  year =         1997,
  month =        {November}
}

@InProceedings{ThayerHerzogGuttman98,
  author =       {F. Javier {\textsc{Thayer} F\'{a}brega} and Jonathan C. Herzog and Joshua D. Guttman},
  title =        {Strand Spaces:  Why is a Security Protocol Correct?},
  booktitle =    {1998 {IEEE} Symposium on Security and Privacy},
  year =         1998,
  month =        {May},
  publisher =    {{IEEE} CS Press}
}

@InProceedings{ThayerHerzogGuttman98a,
  author =       {F. Javier {\textsc{Thayer} F\'{a}brega} and Jonathan C. Herzog and Joshua D. Guttman},
  title =        {Honest Ideals on Strand Spaces},
  booktitle =    {Proceedings of the 11th {IEEE} Computer Security Foundations Workshop},
  year =         1998,
  month =        {June},
  publisher =    {{IEEE} CS Press}
}

@Unpublished{ThayerHerzogGuttman98b,
  author =       {F. Javier {\textsc{Thayer} F\'{a}brega} and Jonathan C. Herzog and Joshua D. Guttman},
  title =        {Strand Space Pictures},
  note =         {Presented at the {LICS Workshop on Formal Methods and Security Protocols}},
  month =        {June},
  year =         1998
}

@Article{ThayerHerzogGuttman99,
  author =       {F. Javier Thayer and Jonathan C. Herzog and Joshua D. Guttman},
  title =        {Strand Spaces:  Proving Security Protocols Correct},
  journal =      {Journal of Computer Security},
  year =         1999,
  volume =       7,
  number =       {2/3},
  pages =        {191--230}
}

@InProceedings{ThayerHerzogGuttman99a,
  author =       {F. Javier Thayer and Jonathan C. Herzog and Joshua D. Guttman},
  title =        {Mixed Strand Spaces},
  booktitle =    {Proceedings of the 12th {IEEE} Computer Security Foundations Workshop},
  year =         1999,
  month =        {June},
  publisher =    {{IEEE} CS Press}
}

@Manual{TCGspec01,
  title =        {Trusted Computing Group Main Specification},
  key =          {Trusted Computing Group},
  organization = {Trusted Computing Group},
  edition =      {Version 1.1b},
  month =        sep,
  year =         2001,
  note =         {URL \url{https://www.trustedcomputinggroup.org/downloads/tcg_spec_1_1b.zip}}
}

@Manual{TCGArch04,
  title =        {TCG Specification Architecture Overview},
  organization = {Trusted Computing Group},
  address =      {\url{https://www.trustedcomputinggroup.org/downloads/TCG_1_0_Architecture_Overview.pdf}},
  edition =      {Revision 1.2},
  month =        {April},
  year =         2004
}

@Manual{TCGMainDesign05,
  title =        {{TPM} Main:  Part {I} Design Principles},
  organization = {Trusted Computing Group},
  address =      {\url{https://www.trustedcomputinggroup.org/downloads/specifications/mainP1DP_rev85.zip}},
  edition =      {Specification Version 1.2, Revision 85},
  month =        {February},
  year =         2005
}

@Misc{VixieEtAl97,
  author =       {P. Vixie and S. Thompson and Y. Rekhter and J. Bound},
  title =        {Dynamic Updates in the Domain Name System},
  howpublished = {RFC 2136},
  month =        {April},
  year =         1997
}

@Article{VolpanoEtAl96,
  author =       {Cynthia Irvine and Dennis Volpano and Geoffrey Smith},
  title =        {A Sound Type System for Secure Flow Analysis},
  journal =      {Journal of Computer Security},
  year =         1996,
  volume =       4,
  number =       3,
  pages =        {1--21}
}

@Article{VoydockKent83,
  author =       "Victor L. Voydock and Stephen T. Kent",
  title =        "Security Mechanisms in High-Level Network Protocols",
  journal =      "Computing Surveys",
  year =         1983,
  volume =       15,
  number =       2,
  pages =        "135--171",
  month =        jun
}

@InProceedings{WagnerSchneier96,
  author =       {D. Wagner and B. Schneier},
  title =        {Analysis of the {SSL} 3.0 Protocol},
  booktitle =    {Proceedings, Second USENIX Workshop on Electronic Commerce},
  pages =        {29--40},
  year =         1996,
  note =         {Available at http://www.counterpane.com/ssl.html}
}

@InProceedings{WallachFelten98,
  author =       {Daniel S. Wallach and Edward W. Felten},
  title =        {Understanding Java Stack Inspection},
  booktitle =    {{IEEE} Symposium on Security and Privacy},
  pages =        {52--63},
  year =         1998
}

@article{Wang2006,
  title={Generic non-repudiation protocols supporting transparent off-line {TTP}},
  author={Guilin Wang},
  journal={Journal of Computer Security},
  volume={14},
  number={5},
  pages={441--467},
  year={2006},
  publisher={IOS Press}
}

@Proceedings{Wiener93,
title =        "Efficient DES Key Search ",
year =         1993,
series =       "Crypto 93",
month =        aug
}

@Article{Willet82,
  author =       "Michael Willet",
  title =        "Cryptography Old and New",
  journal =      "Computers and Security",
  volume =       "Vol 1",
  pages =        "177--186",
  year =         1982
}

@Article{WooLam92,
  author =       "T. Y. C. Woo and S. S. Lam",
  title =        "Authentication for Distributed Systems",
  journal =      "Computer",
  year =         1992,
  volume =       25,
  number =       1,
  pages =        "39--52",
  month =        jan
}

@Article{WooLam92a,
  author =       {Thomas Y. C. Woo and Simon S. Lam},
  title =        {Authentication for Distributed Systems},
  journal =      {Computer},
  year =         1992,
  volume =       25,
  number =       1,
  pages =        {39--52},
  month =        {January}
}

@InProceedings{WooLam93,
  author =       {Thomas Y. C. Woo and Simon S. Lam},
  title =        {Verifying authentication protocols: Methodology and example},
  booktitle =    {Proc. Int. Conference on Network Protocols},
  year =         1993,
  month =        {October}
}

@Article{WooLam94,
  author =       "Thomas Y. C. Woo and Simon S. Lam",
  title =        "A Lesson on Authentication Protocol Design",
  journal =      "Operating Systems Review",
  year =         1994,
  pages =        "24--37"
}

@InProceedings{Wray91,
  author =       {John C. Wray},
  title =        {An Analysis of Covert Timing Channels},
  booktitle =    {Proceedings, 1991 {IEEE} Symposium on Research in Security and Privacy},
  pages =        {2--7},
  year =         1991,
  month =        {May},
  organization = {{IEEE} CS}
}

@InProceedings{YamaguchiOkayamaMiyahara90,
  author =       "S. Yamaguchi and K. Okayama and H. Miyahara",
  title =        "Design and Implementation of an Authentication System
                in {WIDE Internet} Environment",
  booktitle =    "Proceedings of the 10th Regional
                  Conference on Computers
                and Communication Systems",
  year =         1990
}

@InProceedings{WoolEtAl00,
  author =       {Alain Mayer and Avishai Wool and Elisha Ziskind},
  title =        {Fang:  A Firewall Analysis Engine},
  booktitle =    {Proceedings, IEEE Symposium on Security and Privacy},
  year =         2000
}

@Unpublished{YasinacWulf93,
  author =       "Alec F Yasinsac and William A Wulf",
  title =        "A Formal Semantics for Evaluating Cryptographic Protocols",
  note =         "The paper has been superceeded by a later version
                  published in the IEEE Symposium on Security and
                  Privacy 1994.",
  year =         1993
}

@Misc{SSHArch,
  author =       {T. Ylonen and T. Kivinen and M. Saarinen},
  title =        {{SSH} Prototcol Architecture},
  howpublished = {Internet draft},
  month =        {November},
  year =         {1997},
  note =         {Also named draft-ietf-secsh-architecture-01.txt}
}

@Misc{SSHConn,
  author =       {T. Ylonen and T. Kivinen and M. Saarinen},
  title =        {{SSH} Connection Prototcol},
  howpublished = {Internet draft},
  month =        {November},
  year =         {1997},
  note =         {Also named draft-ietf-secsh-connect-03.txt}
}

@Misc{SSHTrans,
  author =       {T. Ylonen and T. Kivinen and M. Saarinen},
  title =        {{SSH} Transport Layer Prototcol},
  howpublished = {Internet draft},
  month =        {November},
  year =         {1997},
  note =         {Also named draft-ietf-secsh-transport-01.txt}
}

@Misc{SSHAuth,
  author =       {T. Ylonen and T. Kivinen and M. Saarinen},
  title =        {{SSH} Authentication Prototcol},
  howpublished = {Internet draft},
  month =        {November},
  year =         {1997},
  note =         {Also named draft-ietf-secsh-userauth-01.txt}
}

@Book{ReedSimon80,
  author =      {M. Reed and B. Simon},
  title =       {Functional Analysis},
  publisher =   {Academic Press},
  year =        {1980},
  address =     {Orlando}
}

@Book{billingsley1,
  author =      "Patrick Billingsley Jr.",
  title =       "Convergence of Probability Measures",
  publisher =   "John Wiley and Sons",
  year =        "1968",
  OPTeditor =   "",
  OPTvolume =   "",
  OPTseries =   "",
  address =     "New York",
  OPTedition =  "",
  OPTmonth =    "",
  OPTnote =     ""
}

@Book{DaemenRijmen,
    author ={J. Daemen and V. Rijmen},
    title = {The Design of Rijndael},
    publisher = {Springer-Verlag},
    year = {2002},
    address = {Berlin}
}

@InProceedings{LincolnEtAl99,
  author =       {Lincoln,P.D. and Mitchell, J.C. and Mitchell, M. and Scedrov, A.},
  title =        {Probabilistic polynomial-time equivalence and security protocols},
  booktitle =    {{FM}'99 World Congress On Formal Methods in the Development of Computing Systems},
  year =         1999,
  month =        {September}
}

@InProceedings{LincolnEtAl98,
  author =       {Lincoln, P.D. and Mitchell, J.C. and Mitchell, M. and Scedrov, A.},
  title =        {A Probabilistic Poly-time Framework for Protocol Analysis},
  booktitle =    {{ACM} Computer and Communication Security ({CCS}-5)},
  pages =        {112-121},
  year =         1998
}

@InProceedings{MitchelEtAl98,
  author =       {J. C. Mitchell and M. Mitchell and A. Scedrov},
  title =        {A linguistic characterization of bounded oracle computation and probabilistic polynomial time},
  booktitle =    {{IEEE} Foundations of Computer Science},
  pages =        {725-733},
  year =         1998
}

@InProceedings{PereiraO:2001:CSFW,
  author       = "Olivier Pereira and Jean-Jacques Quisquater",
  title        = "A Security Analysis of the Cliques Protocols Suites",
  booktitle    = "14th IEEE Computer Security Foundations
                  Workshop --- CSFW'01",
  year         = 2001,
  pages        = "73--81",
  address      = "Cape Breton, Canada",
  month        = "11--13 June",
  publisher    = "IEEE CS Press"
}

@inproceedings{pereira2004generic,
  title={Generic insecurity of cliques-type authenticated group key agreement protocols},
  author={Olivier Pereira and J-J Quisquater},
  booktitle={Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE},
  pages={16--29},
  year={2004},
  organization={IEEE}
}

@article{pereira2006impossibility,
  title={On the impossibility of building secure cliques-type authenticated group key agreement protocols},
  author={Olivier Pereira and Jean-Jacques Quisquater},
  journal={Journal of Computer Security},
  volume={14},
  number={2},
  pages={197--246},
  year={2006},
  publisher={IOS Press}
}

@InProceedings{PereiraO:2001:CSFW,
  author       = "Olivier Pereira and Jean-Jacques Quisquater",
  title        = "A Security Analysis of the Cliques Protocols Suites",
  booktitle    = "14th IEEE Computer Security Foundations
                  Workshop --- CSFW'01",
  year         = 2001,
  pages        = "73--81",
  address      = "Cape Breton, Canada",
  month        = "11--13 June",
  publisher    = "IEEE CS Press"
}

@Unpublished{BackesEtAl2003,
  author =       {Michael Backes and Birgit Pfitzmann and Michael Waidner},
  title =        {A Universally Composable Cryptographic Library},
  note =         {Available at \texttt{http://eprint.iacr.org/2003/015/}},
  month =        {January},
  year =         2003
}

@inproceedings{DBLP:conf/esorics/CortierWZ07,
  author    = {V{\'e}ronique Cortier and
               Bogdan Warinschi and
               Eugen Zalinescu},
  title     = {Synthesizing Secure Protocols},
  booktitle = {{ESORICS}:  European Symposium
               On Research In Computer Security},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4734},
  year      = {2007},
  pages     = {406-421},
  ee        = {http://dx.doi.org/10.1007/978-3-540-74835-9_27},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{LiEtAl2012,
  author = 	 {Ming Li and Sucheng Yu and Joshua D. Guttman and
                  Wenjing Lou and Kui Ren},
  title = 	 {Secure ad-hoc trust initialization and key management in
    wireless body area networks},
  journal = 	 {ACM Transactions on Sensor
    Networks (TOSN)},
  volume    = 9,
  number    = 2,
  pages     = 18,
  year      = 2013}

@inproceedings{DenielouYoshida2011,
  author    = {Pierre-Malo Deni{\'e}lou and
               Nobuko Yoshida},
  title     = {Dynamic multirole session types},
  booktitle = {POPL},
  year      = 2011,
  pages     = {435-446},
  ee        = {http://doi.acm.org/10.1145/1926385.1926435},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{CG09b,
  author = {Marco Carbone and Joshua Guttman},
  title = {Choreographies with Secure Boxes and Compromised Principals},
  booktitle = {{Proc. of Interaction and Concurrency Experience (ICE'09)}},
  publisher = {EPTCS},
  volume = {12},
  pages = {1--15},
  year = {2009},
  url = {http://arxiv.org/abs/0911.5444}
}

@article{KL11,
  author    = {Allaa Kamil and
               Gavin Lowe},
  title     = {Analysing {TLS} in the strand spaces model},
  journal   = {Journal of Computer Security},
  volume    = {19},
  number    = {5},
  year      = {2011},
  pages     = {975-1025},
  ee        = {http://dx.doi.org/10.3233/JCS-2011-0429},
}

@Misc{onlineappendix,
  author = {Marco Carbone and Joshua Guttman},
  title =        {Online Appendix},
  howpublished = {\url{http://www.itu.dk/people/maca/separation}}
}

@InProceedings{ADK08,
  author =       "Myrto Arapinis and Stephanie Delaune and Steve Kremer",
  title =        "From one Session to many: Dynamic Tags for Security Protocols",
  booktitle =    "Proc. of LPAR'08",
  year =         "2008"
}

@inproceedings{DKR08,
   author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.},
   booktitle = {{P}roceedings of the 21st {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'08)},
   DOI = {10.1109/CSF.2008.6},
   month = jun,
   pages = {239-251},
   publisher = {{IEEE} Computer Society Press},
   title = {Composition of Password-based Protocols},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csf08.pdf},
   year = {2008},
}

@techreport{KL08,
  title = "Analysing TLS in the Strand Spaces Model",
  author = "Allaa Kamil and Gavin Lowe",
  year = "2008",
}

@InProceedings{HYC08,
  author =       "K. Honda and N. Yoshida and M. Carbone",
  title =        "Multiparty Asynchronous Session Types",
  booktitle =    "Proc. of POPL",
  year =         "2008",
  pages =     {273--284},
  volume    = {43(1)},
  publisher = {ACM},
}

@InProceedings{sessiontypes,
  author       = {Kohei Honda and Vasco Vasconcelos and Makoto Kubo},
  title        = {Language primitives and type disciplines for structured
                 communication-based programming},
  booktitle    = "ESOP'98",
  series       = "LNCS",
  volume       = "1381",
  pages        = {22--138},
  year        = {1998},
   publisher =    {Springer-Verlag},
}

@InProceedings{DoughertyGuttman12,
  author = 	 {Daniel J. Dougherty and Joshua D. Guttman},
  title = 	 {An Algebra for
  Symbolic {Diffie-Hellman} Protocol Analysis},
  booktitle = {Trustworthy Global
  Computing},
  year = 	 2012,
  volume    = {8191},
  pages     = {164--181},
  series = 	 {LNCS}}

@Article{Guttman12a,
  author = 	 {Joshua D. Guttman},
  title = 	 {Establishing and Preserving Protocol Security Goals},
  journal = 	 {Journal of Computer Security},
  year = 	 2014,
  volume = 	 22,
  number = 	 2,
  pages = 	 {203--267}}

@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}}

@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}

@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}

@TechReport{cpsatheory11,
  title = 	 {Completeness of {CPSA}},
  author = 	 {Moses D.~Liskov and Paul D.~Rowe and F.~Javier Thayer},
  institution = {The MITRE Corporation},
  year = 	 2011,
  month =        mar,
  number = 	 {MTR110479},
  note =         {\url{http://www.mitre.org/publications/technical-papers/completeness-of-cpsa}}
}

@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}},
}

@inproceedings{cade92-pvs,
    AUTHOR = {{S.} Owre and {J.} {M.} Rushby and and {N.} Shankar},
    TITLE = {{PVS:} {A} Prototype Verification System},
    BOOKTITLE = {11th International Conference on Automated Deduction (CADE)},
    YEAR = {1992},
    EDITOR = {Deepak Kapur},
    SERIES = {Lecture Notes in Artificial Intelligence},
    VOLUME = {607},
    PAGES = {748--752},
    ADDRESS = {Saratoga, {NY}},
    MONTH = jun,
    PUBLISHER = {Springer-Verlag},
    URL = {http://pvs.csl.sri.com/papers/cade92-pvs/},
    note = {\url{http://pvs.csl.sri.com}}
}

@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}
    }

@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{DBLP:conf/csfw/SchmidtMCB12,
  author    = {Benedikt Schmidt and
               Simon Meier and
               Cas J. F. Cremers and
               David A. Basin},
  title     = {Automated Analysis of {Diffie-Hellman} Protocols and Advanced
               Security Properties},
  booktitle = {{IEEE} Symposium on Computer Security Foundations},
  year      = {2012},
  pages     = {78-94},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/CSF.2012.25},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{chevalier2008complexity,
  title={Complexity results for security protocols with {Diffie-Hellman} exponentiation and commuting public key encryption},
  author={Yannick Chevalier and Ralf K{\"u}sters and Micha{\"e}l Rusinowitch and Mathieu Turuani},
  journal={ACM Transactions on Computational Logic (TOCL)},
  volume={9},
  number={4},
  pages={24},
  year={2008},
  publisher={ACM}
}

@incollection{gurgens2007security,
  title={Security evaluation of scenarios based on the {TCG's TPM} specification},
  author={Sigrid G{\"u}rgens  and Carsten Rudolph and Dirk Scheuermann and Marion Atts and Rainer Plaga},
  booktitle={Computer Security--ESORICS 2007},
  pages={438--453},
  year={2007},
  publisher={Springer}
}

@inproceedings{datta2009logic,
  title={A logic of secure systems and its application to trusted computing},
  author={Anupam Datta and Jason Franklin and Deepak Garg and Dilsun Kaynar},
  booktitle={Security and Privacy, 2009 30th IEEE Symposium on},
  pages={221--236},
  year={2009},
  organization={IEEE}
}

@inproceedings{youn2007robbing,
  title={Robbing the bank with a theorem prover},
  author={Paul Youn and Ben Adida and Mike Bond and Jolyon Clulow and Jonathan Herzog and Amerson Lin and Ronald Rivest and Ross Anderson},
  booktitle={Security Protocols Workshop},
  note={Available at \url{http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-644.pdf}},
  year=2007
}

@incollection{cortier2007automatic,
  title={Automatic analysis of the security of XOR-based key management schemes},
  author={V{\'e}ronique Cortier and Gavin Keighren and Graham Steel},
  booktitle={Tools and Algorithms for the Construction and Analysis of Systems},
  pages={538--552},
  year={2007},
  publisher={Springer}
}

@incollection{cortier2009generic,
  title={A generic security API for symmetric key management on cryptographic devices},
  author={V{\'e}ronique Cortier and Graham Steel},
  booktitle={Computer Security--ESORICS 2009},
  pages={605--620},
  year={2009},
  publisher={Springer}
}

@incollection{froschle2011reasoning,
  title={Reasoning with past to prove {PKCS\# 11} keys secure},
  author={Sibylle Fr{\"o}schle and Nils Sommer},
  booktitle={Formal Aspects of Security and Trust},
  pages={96--110},
  year={2011},
  publisher={Springer}
}

@article{modersheim2010abstraction,
  title={Abstraction by set-membership: verifying security protocols and web services with databases},
  author={Sebastian M{\"o}dersheim},
  journal={ACM Conference on Computer and Communications Security},
  pages={351--360},
  year={2010}
}

@inproceedings{arapinis2011statverif,
  title={Statverif: Verification of stateful processes},
  author={Myrto Arapinis and Eike Ritter and Mark Dermot Ryan},
  booktitle={Computer Security Foundations Symposium (CSF)},
  pages={33--47},
  year={2011},
  organization={IEEE}
}

@incollection{delaune2011formal,
  title={A formal analysis of authentication in the {TPM}},
  author={Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D and Steel, Graham},
  booktitle={Formal Aspects of Security and Trust},
  pages={111--125},
  year={2011},
  publisher={Springer}
}

@article{herzog2006applying,
  title={Applying protocol analysis to security device interfaces},
  author={Jonathan Herzog},
  journal={IEEE Security \& Privacy},
  volume={4},
  number={4},
  pages={84--87},
  year={2006},
  publisher={IEEE}
}

@incollection{sampaio2002refinement,
  title={Refinement in {Circus}},
  author={Augusto Sampaio and Jim Woodcock and Ana Cavalcanti},
  booktitle={FME 2002: Formal Methods},
  pages={451--470},
  year={2002},
  publisher={Springer}
}

@incollection{butler2005combining,
  title={Combining {CSP} and {B} for specification and property verification},
  author={Michael Butler and Michael Leuschel},
  booktitle={FM 2005: Formal Methods},
  pages={221--236},
  year={2005},
  publisher={Springer}
}

@inproceedings{Clulow03,
  author    = {Jolyon Clulow},
  title     = {On the Security of {PKCS}\#11},
  booktitle = {Cryptographic Hardware and Embedded Systems - {CHES} 2003},
  year      = {2003},
  pages     = {411-425},
  ee        = {http://dx.doi.org/10.1007/978-3-540-45238-6_32},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2779},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{meier2013efficient,
  title={Efficient construction of machine-checked symbolic protocol security proofs},
  author={Simon Meier and Cas Cremers and David Basin},
  journal={Journal of Computer Security},
  volume={21},
  number={1},
  pages={41--87},
  year={2013},
  publisher={IOS Press}
}

@book{cremers2012operational,
  title={Operational semantics and verification of security protocols},
  author={Cas Cremers and Sjouke Mauw},
  year={2012},
  publisher={Springer}
}

@article{jacobs2009semantics,
  title={Semantics and logic for security protocols},
  author={Bart Jacobs and Ichiro Hasuo},
  journal={Journal of Computer Security},
  volume={17},
  number={6},
  pages={909--944},
  year={2009},
  publisher={IOS Press}
}

@techreport{LiskovThayer13,
  author = {Moses D. Liskov and F. Javier Thayer},
title = {Formal Modeling of {Diffie-Hellman} Derivability for Exploratory Automated Analysis},
  institution = {{MITRE} },
  year = {2013},
  month = {June},
  note = {TR 13-0411}
}

@article{Comon-LundhCZ10,
  author    = {Hubert Comon-Lundh and
               V{\'e}ronique Cortier and
               Eugen Zalinescu},
  title     = {Deciding security properties for cryptographic protocols.
               {A}pplication to key cycles},
  journal   = {ACM Trans. Comput. Log.},
  volume    = {11},
  number    = {2},
  year      = {2010},
  ee        = {http://doi.acm.org/10.1145/1656242.1656244},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{BoydMathuria03,
  title={Protocols for authentication and key establishment},
  author={Boyd, Colin and Mathuria, Anish},
  year={2003},
  publisher={Springer}
}

@Article{MTI86,
  author = 	 {T. Matsumoto and Y. Takashima and H. Imai},
  title = 	 {On Seeking Smart Public-key Distribution Systems},
  journal = 	 {Transactions of the IECE of Japan},
  year = 	 1986,
  volume = 	 {E69},
  pages = 	 {99--106}}

@article{clarkson2010hyperproperties,
  title={Hyperproperties},
  author={Michael R. Clarkson and Fred B. Schneider},
  journal={Journal of Computer Security},
  volume={18},
  number={6},
  pages={1157--1210},
  year={2010},
  publisher={IOS Press}
}

@inproceedings{sprenger2010developing,
  title={Developing security protocols by refinement},
  author={Christoph Sprenger and David Basin},
  booktitle={{ACM CCS}},
  pages={361--374},
  year={2010}
}

@inproceedings{sprenger2012refining,
  title={Refining key establishment},
  author={Christoph Sprenger and David Basin},
  booktitle={{IEEE CSF}},
  pages={230--246},
  year={2012}
}

@incollection{maurer1994calculus,
  title={A calculus for secure channel establishment in open networks},
  author={{\"U}li Maurer and Pierre Schmid},
  booktitle={{ESORICS} 94},
  pages={173--192},
  year={1994},
  publisher={Springer}
}

@incollection{Cremers11keyexchange,
  title={Key exchange in {IPsec} revisited: Formal analysis of {IKEv1} and {IKEv2}},
  author={Cremers, Cas},
  year={2011},
  publisher={Springer},
  booktitle={Computer Security--ESORICS 2011},
}

@Misc{cdgk2014,
  key = 	 {ckgk2014},
  author = 	 {V{\'e}ronique Cortier and Daniel J. Dougherty and
                  Joshua D. Guttman and Steve Kremer},
  title = 	 {The Real-or-Random Property for Lightweight
                  {Diffie-Hellman} Protocols},
  howpublished = {Meetings},
  month = 	 {January},
  year = 	 2014}

@Misc{whatever,
  key = 	 {whatever},
  author = 	 {Someone somewhere},
  title = 	 {Good citation for undecidability of unification in rings}}

@article{MillenShmatikov05,
  author    = {Jonathan K. Millen and
               Vitaly Shmatikov},
  title     = {Symbolic protocol analysis with an Abelian group operator
               or Diffie-Hellman exponentiation},
  journal   = {Journal of Computer Security},
  volume    = {13},
  number    = {3},
  year      = {2005},
  pages     = {515-564},
  ee        = {http://iospress.metapress.com/openurl.asp?genre=article{\&}issn=0926-227X{\&}volume=13{\&}issue=3{\&}spage=515},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{cortier2006survey,
  title={A survey of algebraic properties used in cryptographic protocols},
  author={V{\'e}ronique Cortier and St{\'e}phanie Delaune and Pascal
                  Lafourcade},
  journal={Journal of Computer Security},
  volume={14},
  number={1},
  pages={1--43},
  year={2006},
  publisher={IOS Press}
}

@article{kremer2010computationally,
  title={Computationally sound analysis of protocols using bilinear pairings},
  author={Steve Kremer and  Laurent Mazar{\'e}},
  journal={Journal of Computer Security},
  volume={18},
  number={6},
  pages={999--1033},
  year={2010},
  publisher={IOS Press}
}

@InProceedings{DoughertyGuttman2014,
  author = 	 {Daniel J. Dougherty and Joshua D. Guttman},
  title = 	 {Decidability for Lightweight {Diffie-Hellman}
                  Protocols},
  booktitle = {{IEEE} Symposium on Computer Security Foundations},
  year = 	 2014}

@article{jacobs2009semantics,
  title={Semantics and logic for security protocols},
  author={Bart Jacobs and Ichiro Hasuo},
  journal={Journal of Computer Security},
  volume={17},
  number={6},
  pages={909--944},
  year={2009},
  publisher={IOS Press}
}

@article{meier2013efficient,
  title={Efficient construction of machine-checked symbolic protocol security proofs},
  author={Simon Meier and Cas Cremers and David Basin},
  journal={Journal of Computer Security},
  volume={21},
  number={1},
  pages={41--87},
  year={2013},
  publisher={IOS Press}
}

@InProceedings{Adida2008,
  author = 	 {Ben Adida},
  title = 	 {Helios:  Web-based Open-Audit Voting},
  booktitle = {Usenix Security Symposium},
  year = 	 2008,
  organization = {Usenix Association}}

@article{gottlob2008efficient,
  title={Efficient core computation in data exchange},
  author={Gottlob, Georg and Nash, Alan},
  journal={{JACM}},
  volume={55},
  number={2},
  pages={9},
  year={2008},
  publisher={ACM}
}

@inproceedings{mccullough1987specifications,
  title={Specifications for multi-level security and a hook-up property},
  author={Daryl McCullough},
  booktitle={{IEEE} Symposium on Security and Privacy},
  pages={161--161},
  year={1987}
}

@inproceedings{mccullough1988noninterference,
  title={Noninterference and the composability of security properties},
  author={Daryl McCullough},
  booktitle={{IEEE} Symposium on Security and Privacy},
  pages={177--186},
  year={1988}
}

@article{zdancewic2002secure,
  title={Secure program partitioning},
  author={Steve Zdancewic and Lantian Zheng and Nathaniel Nystrom and
                  Andrew C Myers},
  journal={ACM Transactions on Computer Systems (TOCS)},
  volume={20},
  number={3},
  pages={283--328},
  year={2002},
  publisher={ACM}
}

@inproceedings{LiZdancewic05,
  author    = {Peng Li and
               Steve Zdancewic},
  title     = {Downgrading policies and relaxed noninterference},
  booktitle = {Principles of Programming Languages {POPL}},
  pages     = {158--170},
  year      = {2005},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/popl/LiZ05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{chong2007secure,
  title={Secure web applications via automatic partitioning},
  author={Stephen Chong and Jed Liu and Andrew C Myers and Xin Qi and Krishnaprasad Vikram and Lantian Zheng and Xin Zheng},
  booktitle={{ACM SIGOPS} Operating Systems Review},
  volume={41},
  pages={31--44},
  year={2007},
  organization={ACM}
}

@inproceedings{bohannon2009reactive,
  title={Reactive noninterference},
  author={Bohannon, Aaron and Pierce, Benjamin C and Sj{\"o}berg, Vilhelm and Weirich, Stephanie and Zdancewic, Steve},
  booktitle={{ACM} conference on Computer and Communications Security},
  pages={79--90},
  year={2009},
  organization={ACM}
}

@article{sabelfeld2009declassification,
  title={Declassification: Dimensions and principles},
  author={Andrei Sabelfeld and David Sands},
  journal={Journal of Computer Security},
  volume={17},
  number={5},
  pages={517--548},
  year={2009}
}

@inproceedings{chong2009deriving,
  title={Deriving epistemic conclusions from agent architecture},
  author={Stephen Chong and Ron {van der Meyden}},
  booktitle={Theoretical Aspects of Rationality and Knowledge},
  pages={61--70},
  year={2009},
  organization={ACM}
}

@InProceedings{RafnssonSabelfeld14,
  author = 	 {Willard Rafnsson and Andrei Sabelfeld},
  title = 	 {Compositional Information-Flow Security for Interactive Systems},
  booktitle = {{IEEE} Symp.~{CSF}},
  year = 	 2014,
  pages = 	 {277--292},
  month = 	 {July},
}

@article{ryan2009pret,
  title={Pr{\^e}t {\`a} voter: a voter-verifiable voting system},
  author={Peter YA Ryan and David Bismark and James Heather and Steve Schneider and Zhe Xia},
  journal={Information Forensics and Security, IEEE Transactions on},
  volume={4},
  number={4},
  pages={662--673},
  year={2009},
  publisher={IEEE}
}

@article{jacob1992basic,
  title={Basic theorems about security},
  author={Jeremy Jacob},
  journal={Journal of Computer Security},
  volume={1},
  number={3},
  pages={385--411},
  year={1992},
  publisher={IOS Press}
}

@inproceedings{morgan2006shadow,
  title={The shadow knows: Refinement of ignorance in sequential programs},
  author={Carroll Morgan},
  booktitle={Mathematics of program construction},
  pages={359--378},
  year={2006},
  organization={Springer}
}

@Article{ArapinisEtAl14,
  author = 	 {Myrto Arapinis and St{\'e}phanie Delaune and Steve
                  Kremer},
  title = 	 {Dynamic Tags for Security Protocols},
  journal = 	 {Logical Methods in Computer Science},
  year = 	 {2014},
  OPTkey = 	 {},
  OPTvolume = 	 {10},
  OPTnumber = 	 {2:11},
  OPTpages = 	 {1--50}
}

@incollection{carbone2013sessions,
  title={Sessions and separability in security protocols},
  author={Marco Carbone and Joshua D  Guttman},
  booktitle={Principles of Security and Trust},
  pages={267--286},
  year={2013},
  publisher={Springer}
}

@inproceedings{adao2014mignis,
  title={Mignis: A semantic based tool for firewall configuration},
  author={P Adao and Claudio Bozzato and Gian-Luca Dei Rossi, R Focardi and F Luccio},
  booktitle={{IEEE CSF}},
  year=2014
}

@article{van2012architectural,
  title={Architectural refinement and notions of intransitive noninterference},
  author={Ron {van der Meyden}},
  journal={Formal Aspects of Computing},
  volume={24},
  number={4-6},
  pages={769--792},
  year={2012},
  publisher={Springer}
}

@book{rushby1992noninterference,
  title={Noninterference, transitivity, and channel-control security policies},
  author={John Rushby},
  year={1992},
  publisher={SRI International, Computer Science Laboratory}
}

@incollection{van2007indeed,
  title={What, indeed, is intransitive noninterference?},
  author={Ron {van der Meyden}},
  booktitle={Computer Security--ESORICS 2007},
  pages={235--250},
  year={2007},
  publisher={Springer}
}

@TechReport{ChongvanderMeyden14,
  author = 	 {Stephen Chong and Ron {van der Meyden}},
  title = 	 {Using Architecture to Reason about Information Security},
  institution =  {Arxiv},
  year = 	 2014,
  number = 	 {arXiv:1409.0309},
  month = 	 {Sept.},
  note = 	 {\url{http://arxiv.org/abs/1409.0309v1}}}

@incollection{sabelfeld2004model,
  title={A model for delimited information release},
  author={Andrei Sabelfeld and Andrew C Myers},
  booktitle={Software Security-Theories and Systems},
  pages={174--191},
  year={2004},
  publisher={Springer}
}

@article{delaune2009verifying,
  title={Verifying privacy-type properties of electronic voting protocols},
  author={St{\'e}phanie Delaune and Steve Kremer and Mark Ryan},
  journal={Journal of Computer Security},
  volume={17},
  number={4},
  pages={435--487},
  year={2009},
  publisher={IOS Press}
}

@inproceedings{wittbold1990information,
  title={Information flow in nondeterministic systems},
  author={J Todd Wittbold and Dale M Johnson},
  booktitle={{IEEE} Symp. Security and Privacy},
  pages={144--144},
  year={1990}
}

@Article{HaighYoung1987,
  author = 	 {J Thomas Haigh and William D Young},
  title = 	 {Extending the non-interference version of MLS for SAT},
  journal = 	 {{IEEE} Transactions on Software Engineering},
  year = 	 1987,
  volume = 	 13,
  number = 	 2}

@inproceedings{askarov2007gradual,
  title={Gradual release: Unifying declassification, encryption and key release policies},
  author={Aslan Askarov and Andrei Sabelfeld},
  booktitle={{IEEE} Symp. Security and Privacy},
  pages={207--221},
  year={2007},
  organization={IEEE}
}

@inproceedings{mantel2011assumptions,
  title={Assumptions and guarantees for compositional noninterference},
  author={Heiko Mantel and David Sands and Henning Sudbrock},
  booktitle={{IEEE} Computer Security Foundations Symposium},
  pages={218--232},
  year={2011}
}

@incollection{roscoe1994non,
  title={Non-interference through determinism},
  author={A.W. Roscoe and J.C.P. Woodcock and L. Wulf},
  booktitle={Computer Security---ESORICS 94},
  pages={31--53},
  year={1994},
  publisher={Springer}
}

@inproceedings{mclean1994general,
  title={A general theory of composition for trace sets closed under selective interleaving functions},
  author={John McLean},
  booktitle={{IEEE} Symp.~Security and Privacy},
  pages={79--93},
  year={1994}
}

@article{McLean1996,
 author = {McLean, John},
 title = {A General Theory of Composition for a Class of ``Possibilistic'' Properties},
 journal = {IEEE Trans. Softw. Eng.},
 issue_date = {January 1996},
 volume = {22},
 number = {1},
 month = jan,
 year = {1996},
 pages = {53--67}
 }

@Misc{GuttmanRowe14:cut,
  author = 	 {Joshua D. Guttman and Paul D. Rowe},
  title = 	 {A Cut Principle for Information Flow},
  howpublished = {Arxiv},
  month = 	 {October},
  year = 	 2014,
  note = 	 {\url{http://arxiv.org/abs/1410.4617}}}

@InProceedings{GuttmanRowe15,
  author = 	 {Joshua D. Guttman and Paul D. Rowe},
  title = 	 {A Cut Principle for Information Flow},
  booktitle = {{IEEE} Computer Security Foundations},
  year = 	 2015,
  month = 	 {July},
  publisher = {{IEEE} Computer Society Press}}

@book{cormen2003introduction,
  title={Introduction to Algorithms},
  author={Thomas H. Cormen and Charles E. Leiserson and Ronald
                  L. Rivest and Clifford Stein},
  publisher={MIT Press},
  edition={second},
  address = {Cambridge, MA},
  year=2003
}

@article{bossi2004verifying,
  title={Verifying persistent security properties},
  author={Annalisa Bossi and Riccardo Focardi and Carla Piazza and Sabina Rossi},
  journal={Computer Languages, Systems \& Structures},
  volume={30},
  number={3},
  pages={231--258},
  year={2004}
}

@inproceedings{rossi2009information,
  title={Information flow security for service compositions.},
  author={Sabina Rossi and Damiano Macedonio},
  booktitle={ICUMT},
  pages={1--8},
  year={2009}
}

@incollection{focardi2001classification,
  title={Classification of security properties},
  author={Riccardo Focardi and Roberto Gorrieri},
  booktitle={Foundations of Security Analysis and Design},
  pages={331--396},
  year={2001},
  publisher={Springer}
}

@inproceedings{mantel2000possibilistic,
  title={Possibilistic definitions of security-an assembly kit},
  author={Heiko Mantel},
  booktitle={{IEEE} Computer Security Foundations},
  pages={185--199},
  year={2000},
  organization={IEEE}
}

@inproceedings{mantel2001preserving,
  title={Preserving information flow properties under refinement},
  author={Heiko Mantel},
  booktitle={{IEEE} Computer Security Foundations},
  pages={78--91},
  year={2001}
}

@inproceedings{mantel2002composition,
  title={On the composition of secure systems},
  author={Heiko Mantel},
  booktitle={{IEEE} Security and Privacy},
  pages={88--101},
  year={2002}
}

@article{zakinthinos1995composability,
  title={The composability of non-interference},
  author={Aris Zakinthinos and E Stewart Lee},
  journal={Journal of Computer Security},
  volume={3},
  number={4},
  pages={269--281},
  year={1995}
}

@inproceedings{johnson1988security,
  title={Security and the Composition of Machines.},
  author={Dale M Johnson and F Javier Thayer},
  booktitle={CSFW},
  volume={88},
  pages={72--89},
  year={1988}
}

@article{askarov2008cryptographically,
  title={Cryptographically-masked flows},
  author={Aslan Askarov and Daniel Hedin and Andrei Sabelfeld},
  journal={Theoretical Computer Science},
  volume={402},
  number={2},
  pages={82--101},
  year={2008},
  publisher={Elsevier}
}

@Misc{rivest2006threeballot,
  author = 	 {Ronald L. Rivest},
  title = 	 {The {ThreeBallot} voting system},
  howpublished = {\url{http://theory.lcs.mit.edu/\~rivest/Rivest-TheThreeBallotVotingSystem.pdf}},
  month = 	 Oct,
  year = 	 2006}

@Misc{rivest2007three,
  title =	{Three Voting Protocols: {ThreeBallot}, {VAV}, and {Twin}},
  author=	{Rivest, Ronald L and Smith, Warren D},
  howpublished = {\url{http://people.csail.mit.edu/rivest/pubs/RS07.pdf}},
  year = 	 2007}

@inproceedings{clark2007security,
  title={On the security of ballot receipts in E2E voting systems},
  author={Jeremy Clark and Aleks Essex and Carlisle Adams},
  booktitle={Workshop on Trustworthy Elections ({WOTE})},
  year={2007}
}

@incollection{chatzikokolakis2007making,
  title={Making random choices invisible to the scheduler},
  author={Konstantinos Chatzikokolakis and Catuscia Palamidessi},
  booktitle={CONCUR},
  pages={42--58},
  year={2007},
  publisher={Springer}
}

@incollection{canetti2006time,
  title={Time-bounded task-PIOAs: A framework for analyzing security protocols},
  author={Ran Canetti and Ling Cheung and Dilsun Kaynar and Moses Liskov and Nancy Lynch and Olivier Pereira and Roberto Segala},
  booktitle={Distributed Computing},
  pages={238--253},
  year={2006},
  publisher={Springer}
}

@article{CanettiCKLLPS08,
  author    = {Ran Canetti and
               Ling Cheung and
               Dilsun Kirli Kaynar and
               Moses Liskov and
               Nancy A. Lynch and
               Olivier Pereira and
               Roberto Segala},
  title     = {Analyzing Security Protocols Using Time-Bounded Task-{PIOAs}},
  journal   = {Discrete Event Dynamic Systems},
  volume    = {18},
  number    = {1},
  pages     = {111--159},
  year      = {2008}
}

@article{mccamant2008quantitative,
  title={Quantitative information flow as network flow capacity},
  author={Stephen McCamant and Michael D Ernst},
  journal={ACM SIGPLAN Notices ({PLDI})},
  volume={43},
  number={6},
  pages={193--205},
  year={2008},
  publisher={ACM}
}

@incollection{guttman2014security,
  title={Security Goals and Evolving Standards},
  author={Joshua D Guttman and Moses D Liskov and Paul D Rowe},
  booktitle={Security Standardisation Research},
  pages={93--110},
  year={2014},
  publisher={Springer}
}

@Article{MoranHeatherSchneider2015,
  author = 	 {Murat Moran and James Heather and Steve Schneider},
  title = 	 {Automated anonymity verification of the {ThreeBallot} and {VAV} voting systems},
  journal = 	 {Software and Systems Modeling},
  year = 	 2015,
  note = 	 {Forthcoming}}

@incollection{sabelfeld2010dynamic,
  title={From dynamic to static and back: Riding the roller coaster of information-flow control research},
  author={Andrei Sabelfeld and Alejandro Russo},
  booktitle={Perspectives of Systems Informatics},
  pages={352--365},
  year={2010},
  publisher={Springer}
}

@inproceedings{RamsdellDGR14,
  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},
  booktitle = {Integrated Formal Methods},
  pages     = {272--287},
  year      = {2014},
  url       = {http://dx.doi.org/10.1007/978-3-319-10181-1_17},
  doi       = {10.1007/978-3-319-10181-1_17},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/ifm/RamsdellDGR14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{denning1977certification,
  title={Certification of programs for secure information flow},
  author={Dorothy E Denning and Peter J Denning},
  journal={Communications of the ACM},
  volume={20},
  number={7},
  pages={504--513},
  year={1977},
  publisher={ACM}
}

@inproceedings{Mattern1989,
    author = "Friedemann Mattern",
    editor = "M. Cosnard",
    title = "Virtual Time and Global States of Distributed Systems",
    booktitle = "Proc. Workshop on Parallel and Distributed Algorithms",
    year = "1989",
    pages = "215--226",
    address = "North-Holland / Elsevier",
    note = {(Reprinted in: Z. Yang, T.A. Marsland (Eds.), "Global States and Time in Distributed Systems", IEEE, 1994, pp. 123-133.)}
}

@inproceedings{balliu2011epistemic,
  title={Epistemic temporal logic for information flow security},
  author={Musard Balliu and Mads Dam and Gurvan Le Guernic},
  booktitle={Programming Languages and Analysis for Security},
  year={2011},
  organization={ACM}
}

@inproceedings{landauer1993lattice,
  title={A lattice of information},
  author={Jaisook Landauer and Timothy Redmond},
  booktitle={Computer Security Foundations Workshop},
  pages={65--70},
  year={1993},
  organization={IEEE}
}

@inproceedings{cade92-pvs-old,
    AUTHOR = {{S.} Owre and {J.} {M.} Rushby and {N.} Shankar},
    TITLE = {{PVS:} {A} Prototype Verification System},
    BOOKTITLE = {Conference on Automated Deduction},
    YEAR = 1992,
    SERIES = {LNAI},
    MONTH = jun,
    note = {\url{http://pvs.csl.sri.com}}
}

@inproceedings{GuttmanNadel88,
  author    = {Joshua D. Guttman and
               Mark E. Nadel},
  title     = {What Needs Securing?},
  booktitle = {{IEEE} Computer Security Foundations Workshop},
  pages     = {34--57},
  year      = {1988}
}

@inproceedings{HuntMastroeni05,
  author    = {Sebastian Hunt and
               Isabella Mastroeni},
  title     = {The {PER} Model of Abstract Non-interference},
  booktitle = {Static Analysis Symposium {SAS}},
  pages     = {171--185},
  year      = {2005}
}

@inproceedings{KuhlmanMBET08,
  author    = {Doug Kuhlman and
               Ryan Moriarty and
               Tony Braskich and
               Steve Emeott and
               Mahesh V. Tripunitara},
  title     = {{A Correctness Proof of a Mesh Security Architecture}},
  booktitle = {CSF},
  year      = {2008},
  pages     = {315-330},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/CSF.2008.23},
  crossref  = {DBLP:conf/csfw/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{HeSDDM05,
  author    = {Changhua He and
               Mukund Sundararajan and
               Anupam Datta and
               Ante Derek and
               John C. Mitchell},
  title     = {{A modular correctness proof of IEEE 802.11i and TLS}},
  booktitle = {ACM Conference on Computer and Communications Security},
  year      = {2005},
  pages     = {2-15},
  ee        = {http://doi.acm.org/10.1145/1102120.1102124},
  crossref  = {DBLP:conf/ccs/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{BhargavanFGS08,
  author    = {Karthikeyan Bhargavan and
               C{\'e}dric Fournet and
               Andrew D. Gordon and
               Nikhil Swamy},
  title     = {{Verified implementations of the information card federated
               identity-management protocol}},
  booktitle = {ASIACCS},
  year      = {2008},
  pages     = {123-135},
  ee        = {http://doi.acm.org/10.1145/1368310.1368330},
  crossref  = {DBLP:conf/ccs/2008asia},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{BhargavanFCZ12,
  author    = {Karthikeyan Bhargavan and
               C{\'e}dric Fournet and
               Ricardo Corin and
               Eugen Zalinescu},
  title     = {{Verified Cryptographic Implementations for TLS}},
  journal   = {ACM Trans. Inf. Syst. Secur.},
  volume    = {15},
  number    = {1},
  year      = {2012},
  pages     = {3},
  ee        = {http://doi.acm.org/10.1145/2133375.2133378},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{MitchellRRS08,
  author    = {John C. Mitchell and
               Arnab Roy and
               Paul Rowe and
               Andre Scedrov},
  title     = {Analysis of {EAP-GPSK} Authentication Protocol},
  booktitle = {ACNS},
  year      = {2008},
  pages     = {309-327},
  ee        = {http://dx.doi.org/10.1007/978-3-540-68914-0_19},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@misc{rfc4120,
  author="C. Neuman and T. Yu and S. Hartman and K. Raeburn",
  title="{The Kerberos Network Authentication Service (V5)}",
  series="Request for Comments",
  number="4120",
  howpublished="RFC 4120 (Proposed Standard)",
  publisher="IETF",
  organization="Internet Engineering Task Force",
  year=2005,
  month=jul,
    note="Updated by RFCs 4537, 5021, 5896, 6111, 6112, 6113, 6649, 6806",
  url="http://www.ietf.org/rfc/rfc4120.txt",
}

@misc{rfc4556,
  author="L. Zhu and B. Tung",
  title="{Public Key Cryptography for Initial Authentication in Kerberos (PKINIT)}",
  series="Request for Comments",
  number="4556",
  howpublished="RFC 4556 (Proposed Standard)",
  publisher="IETF",
  organization="Internet Engineering Task Force",
  year=2006,
  month=jun,
    note="Updated by RFC 6112",
  url="http://www.ietf.org/rfc/rfc4556.txt",
}

@article{CervesatoJSTW08,
  author    = {Iliano Cervesato and
               Aaron D. Jaggard and
               Andre Scedrov and
               Joe-Kai Tsay and
               Christopher Walstad},
  title     = {Breaking and fixing public-key {Kerberos}},
  journal   = {Inf. Comput.},
  volume    = {206},
  number    = {2-4},
  year      = {2008},
  pages     = {402-424},
  ee        = {http://dx.doi.org/10.1016/j.ic.2007.05.005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@misc{rfc5746,
  author="E. Rescorla and M. Ray and S. Dispensa and N. Oskov",
  title="{Transport Layer Security (TLS) Renegotiation Indication Extension}",
  series="Request for Comments",
  number="5746",
  howpublished="RFC 5746 (Proposed Standard)",
  publisher="IETF",
  organization="Internet Engineering Task Force",
  year=2010,
  month=feb,
    url="http://www.ietf.org/rfc/rfc5746.txt",
}

@misc{rfc5246,
  author="T. Dierks and E. Rescorla",
  title="{The Transport Layer Security (TLS) Protocol Version 1.2}",
  series="Request for Comments",
  number="5246",
  howpublished="RFC 5246 (Proposed Standard)",
  publisher="IETF",
  organization="Internet Engineering Task Force",
  year=2008,
  month=aug,
    note="Updated by RFCs 5746, 5878, 6176",
  url="http://www.ietf.org/rfc/rfc5246.txt",
}

@article{BasinCM13,
  author    = {David A. Basin and
               Cas Cremers and
               Simon Meier},
  title     = {Provably repairing the {ISO/IEC} 9798 standard for entity
               authentication},
  journal   = {Journal of Computer Security},
  volume    = {21},
  number    = {6},
  year      = {2013},
  pages     = {817-846},
  ee        = {http://dx.doi.org/10.3233/JCS-130472},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article {Meadows03,
  author    = {Catherine Meadows},
  title     = {Formal methods for cryptographic protocol analysis: Emerging
               issues and trends},
  journal   = {IEEE Journal on Selected Areas in Communications},
  volume    = {21},
  number    = {1},
  year      = {2003},
  pages     = {44-54},
  ee        = {http://dx.doi.org/10.1109/JSAC.2002.806125},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article {PimentelM08,
  author    = {Juan Carlos L{\'o}pez Pimentel and
               Raul Monroy},
  title     = {Formal Support to Security Protocol Development: A Survey},
  journal   = {Computaci{\'o}n y Sistemas},
  volume    = {12},
  number    = {1},
  year      = {2008},
  ee        = {http://cys.cic.ipn.mx/ojs/index.php/CyS/article/view/1190},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings {BhargavanDFPS14,
  author    = {Karthikeyan Bhargavan and
               Antoine Delignat-Lavaud and
               C{\'e}dric Fournet and
               Alfredo Pironti and
               Pierre-Yves Strub},
  title     = {Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over {TLS}},
  booktitle = {IEEE Symposium on Security and Privacy},
  year      = {2014}
}

@article {DattaDMR07,
  author    = {Anupam Datta and
               Ante Derek and
               John C. Mitchell and
               Arnab Roy},
  title     = {Protocol Composition Logic ({PCL})},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {172},
  year      = {2007},
  pages     = {311-358},
}

@Unpublished{RoweEtAl2015,
  author = 	 {Paul D. Rowe and Joshua D. Guttman and Moses D. Liskov},
  title = 	 {Measuring Protocol Strength with Security Goals},
  note = 	 {Submitted to \emph{IJIS} in the SSR 2014 special issue.  Available at \url{http://web.cs.wpi.edu/~guttman/pubs/ijis_measuring-security.pdf}},
  month = 	 {April},
  year = 	 2015}

@Article{RoweEtAl2016,
  author = 	 {Paul D. Rowe and Joshua D. Guttman and Moses D. Liskov},
  title = 	 {Measuring Protocol Strength with Security Goals},
  journal = 	 {International Journal of Information Security},
  year = 	 2016,
  volume = 15,
  number = 6,
  month = nov,
  pages = {575--596},
  note = 	 {DOI 10.1007/s10207-016-0319-z, \url{http://web.cs.wpi.edu/~guttman/pubs/ijis_measuring-security.pdf}}}

@inproceedings{KremerKuennemann14,
  author    = {Steve Kremer and
               Robert K{\"{u}}nnemann},
  title     = {Automated Analysis of Security Protocols with Global State},
  booktitle = {{IEEE} Symposium on Security and Privacy},
  pages     = {163--178},
  year      = {2014},
  url       = {http://dx.doi.org/10.1109/SP.2014.18},
  doi       = {10.1109/SP.2014.18},
  timestamp = {Tue, 02 Dec 2014 18:47:29 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sp/KremerK14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{MeierSCB13,
  author    = {Simon Meier and
               Benedikt Schmidt and
               Cas Cremers and
               David A. Basin},
  title     = {The {tamarin} Prover for the Symbolic Analysis of Security Protocols},
  booktitle = {Computer Aided Verification ({CAV})},
  pages     = {696--701},
  year      = 2013,
  url       = {http://dx.doi.org/10.1007/978-3-642-39799-8_48},
  doi       = {10.1007/978-3-642-39799-8_48},
  timestamp = {Fri, 12 Jul 2013 13:57:42 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/MeierSCB13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@Misc{GLRR2015a,
  author = 	 {Joshua D. Guttman and Moses D. Liskov and John D. Ramsdell and Paul D. Rowe},
  title = 	 {Formal Support for Standardizing Protocols with State (extended version)},
  howpublished = {Arxiv},
  month = 	 sep,
  year = 	 2015,
  note = 	 {Available at \url{http://arxiv.org/abs/1509.07552}}}

@InProceedings{AlmousaEtAl2015,
  author = 	 {Omar Almousa and Sebastian A. M\"{o}dersheim and Paolo Modesti and Luca Vigan\`{o}},
  title = 	 {Typing and Compositionality for Security Protocols: A Generalization to the Geometric Fragment},
  booktitle = {ESORICS},
  year = 	 2015,
  series = 	 {LNCS},
  month = 	 sep,
  publisher = {Springer}}

@InProceedings{AndoGuttman15,
  author = 	 {Megumi Ando and Joshua D. Guttman},
  title = 	 {Composable Bounds on Information Flow from Distribution Differences},
  booktitle = {Data Privacy Management, and Security Assurance},
  year = 	 2015,
  volume = 	 9481,
  series = 	 {LNCS},
  pages = 	 {13--29},
  publisher = {Springer}}

@InProceedings{AdaoEtAl16,
  author = 	 {Pedro Ad{\~a}o and Riccardo Focardi and Flaminia L. Luccio and Joshua D. Guttman},
  title = 	 {Localizing Firewall Security Policies},
  booktitle = {{IEEE} Symp. Computer Security Foundations},
  year = 	 2016,
  month = 	 {June},
  organization = {{IEEE} Computer Society}}

@Inbook{GuttmanEtAl2016,
  author="Joshua D. Guttman
and  John D. Ramsdell
and Paul D. Rowe",
title="Cross-Tool Semantics for Protocol Security Goals",
bookTitle="Security Standardisation Research, SSR 2016",
year="2016",
publisher="Springer",
pages="32--61",
isbn="978-3-319-49100-4",
doi="10.1007/978-3-319-49100-4_2",
url="http://dx.doi.org/10.1007/978-3-319-49100-4_2"
}

@inproceedings{DeMoura08,
 author = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
 title = {Z3: An Efficient SMT Solver},
 booktitle = {Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 series = {TACAS'08/ETAPS'08},
 year = {2008},
 isbn = {3-540-78799-2, 978-3-540-78799-0},
 location = {Budapest, Hungary},
 pages = {337--340},
 numpages = {4},
 url = {https://github.com/Z3Prover/z3/wiki},
 acmid = {1792766},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg}
}

@inproceedings{Maurer05,
  author    = {Ueli M. Maurer},
  title     = {Abstract Models of Computation in Cryptography},
  booktitle = {Cryptography and Coding},
  pages     = {1--12},
  year      = {2005},
  publisher = {Springer},
  volume    = {3796},
  series = {LNCS},
  url       = {https://doi.org/10.1007/11586821_1},
  doi       = {10.1007/11586821_1},
  timestamp = {Tue, 30 May 2017 16:36:52 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/ima/Maurer05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{BartheFFMSS14,
  author    = {Gilles Barthe and
               Edvard Fagerholm and
               Dario Fiore and
               John C. Mitchell and
               Andre Scedrov and
               Benedikt Schmidt},
  title     = {Automated Analysis of Cryptographic Assumptions in Generic Group Models},
  booktitle = {{CRYPTO}},
  pages     = {95--112},
  year      = 2014,
  publisher = {Springer},
  volume    = 8616,
  series = {LNCS},
  url       = {https://doi.org/10.1007/978-3-662-44371-2_6},
  doi       = {10.1007/978-3-662-44371-2_6},
  timestamp = {Fri, 02 Jun 2017 20:50:15 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/crypto/BartheFFMSS14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{Shoup97,
  author    = {Victor Shoup},
  title     = {Lower Bounds for Discrete Logarithms and Related Problems},
  booktitle = {{EUROCRYPT}},
  pages     = {256--266},
  year      = {1997},
  series    = {Lecture Notes in Computer Science},
  volume    = {1233},
  publisher = {Springer},
  url       = {https://doi.org/10.1007/3-540-69053-0_18},
  doi       = {10.1007/3-540-69053-0_18},
  timestamp = {Mon, 22 May 2017 17:12:28 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/eurocrypt/Shoup97},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{LiskovThayer14,
  author    = {Moses Liskov and F. Javier Thayer},
  title     = {Modeling {Diffie-Hellman} Derivability for Automated
                  Analysis},
  booktitle = {{IEEE} Computer Security Foundations},
  pages     = {232--243},
  year      = 2014,
  url       = {https://doi.org/10.1109/CSF.2014.24},
  doi       = {10.1109/CSF.2014.24},
  timestamp = {Thu, 25 May 2017 00:40:51 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/csfw/LiskovT14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{MoedersheimKatsoris14,
  author    = {Sebastian M{\"{o}}dersheim and
               Georgios Katsoris},
  title     = {A Sound Abstraction of the Parsing Problem},
  booktitle = {{IEEE} {CSF}},
  pages     = {259--273},
  year      = {2014},
  url       = {https://doi.org/10.1109/CSF.2014.26},
  doi       = {10.1109/CSF.2014.26},
  timestamp = {Thu, 25 May 2017 00:40:50 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/csfw/ModersheimK14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{GuttmanLRR15,
  author    = {Joshua D. Guttman and
               Moses D. Liskov and
               John D. Ramsdell and
               Paul D. Rowe},
  title     = {Formal Support for Standardizing Protocols with State},
  booktitle = {Security Standardisation Research {SSR}},
  pages     = {246--265},
  year      = {2015},
  note      = {Extended version at \url{http://arxiv.org/abs/1509.07552}},
  url       = {https://doi.org/10.1007/978-3-319-27152-1_13},
  doi       = {10.1007/978-3-319-27152-1_13},
  timestamp = {Sun, 21 May 2017 00:17:16 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/secsr/GuttmanLRR15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@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}

@InCollection{BaaderSnyder01troublesome,
  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‎}}}

@Misc{LiskovGRRT18,
  author = 	 {Moses D. Liskov and Joshua D. Guttman and John D. Ramsdell and Paul D. Rowe and F. Javier Thayer},
  title = 	 {Enrich-by-need Protocol Analysis for
                  {Diffie-Hellman} (Extended Version)},
  howpublished = {\url{http://arxiv.org/abs/1804.05713}},
  month = 	 {April},
  year = 	 2018}

@article{vigano2006automated,
  title={Automated security protocol analysis with the {AVISPA} tool},
  author={Luca Vigan{\`o}},
  journal={Electronic Notes in Theoretical Computer Science},
  volume=155,
  pages={61--86},
  year=2006,
  publisher={Elsevier}
}

@inproceedings{turuani2006cl,
  title={The {CL-Atse} protocol analyser},
  author={Mathieu Turuani},
  booktitle={Rewriting Techniques and Applications},
  pages={277--286},
  year={2006},
  organization={Springer}
}

@inproceedings{Molina-MarkhamR17,
  author    = {Andres Molina{-}Markham and
               Paul D. Rowe},
  title     = {Continuous Verification for Cryptographic Protocol Development},
  booktitle = {Proceedings of the 1st {ACM} Workshop on the Internet of Safe Things,
               SafeThings@SenSys 2017, Delft, The Netherlands, November 5, 2017},
  pages     = {51--56},
  year      = {2017},
  url       = {https://doi.org/10.1145/3137003.3137006},
  doi       = {10.1145/3137003.3137006},
  timestamp = {Tue, 06 Nov 2018 16:57:58 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/sensys/Molina-MarkhamR17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{AvoineBGG0OR17,
  author    = {Gildas Avoine and
               Xavier Bultel and
               S{\'{e}}bastien Gambs and
               David G{\'{e}}rault and
               Pascal Lafourcade and
               Cristina Onete and
               Jean{-}Marc Robert},
  editor    = {Ramesh Karri and
               Ozgur Sinanoglu and
               Ahmad{-}Reza Sadeghi and
               Xun Yi},
  title     = {A Terrorist-fraud Resistant and Extractor-free Anonymous Distance-bounding
               Protocol},
  booktitle = {Proceedings of the 2017 {ACM} on Asia Conference on Computer and Communications
               Security, AsiaCCS 2017, Abu Dhabi, United Arab Emirates, April 2-6,
               2017},
  pages     = {800--814},
  publisher = {{ACM}},
  year      = {2017},
  url       = {https://doi.org/10.1145/3052973.3053000},
  doi       = {10.1145/3052973.3053000},
  timestamp = {Mon, 16 Sep 2019 15:24:37 +0200},
  biburl    = {https://dblp.org/rec/conf/ccs/AvoineBGG0OR17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{CremersRSC12,
  author    = {Cas J. F. Cremers and
               Kasper Bonne Rasmussen and
               Benedikt Schmidt and
               Srdjan {\v{C}}apkun},
  title     = {Distance Hijacking Attacks on Distance Bounding Protocols},
  booktitle = {{IEEE} Symposium on Security and Privacy, {SP} 2012, 21-23 May 2012,
               San Francisco, California, {USA}},
  pages     = {113--127},
  publisher = {{IEEE} Computer Society},
  year      = {2012},
  url       = {https://doi.org/10.1109/SP.2012.17},
  doi       = {10.1109/SP.2012.17},
  timestamp = {Wed, 16 Oct 2019 14:14:51 +0200},
  biburl    = {https://dblp.org/rec/conf/sp/CremersRSC12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{MauwSTT18,
  author    = {Sjouke Mauw and
               Zach Smith and
               Jorge Toro{-}Pozo and
               Rolando Trujillo{-}Rasua},
  title     = {Distance-Bounding Protocols: Verification without Time and Location},
  booktitle = {2018 {IEEE} Symposium on Security and Privacy, {SP} 2018, Proceedings,
               21-23 May 2018, San Francisco, California, {USA}},
  pages     = {549--566},
  publisher = {{IEEE} Computer Society},
  year      = {2018},
  url       = {https://doi.org/10.1109/SP.2018.00001},
  doi       = {10.1109/SP.2018.00001},
  timestamp = {Sat, 19 Oct 2019 20:19:29 +0200},
  biburl    = {https://dblp.org/rec/conf/sp/MauwSTT18.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{ChothiaRS18,
  author    = {Tom Chothia and
               Joeri de Ruiter and
               Ben Smyth},
  editor    = {William Enck and
               Adrienne Porter Felt},
  title     = {Modelling and Analysis of a Hierarchy of Distance Bounding Attacks},
  booktitle = {27th {USENIX} Security Symposium, {USENIX} Security 2018, Baltimore,
               MD, USA, August 15-17, 2018},
  pages     = {1563--1580},
  publisher = {{USENIX} Association},
  year      = {2018},
  url       = {https://www.usenix.org/conference/usenixsecurity18/presentation/chothia},
  timestamp = {Mon, 20 Aug 2018 15:16:57 +0200},
  biburl    = {https://dblp.org/rec/conf/uss/ChothiaRS18.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{MaurerS96,
  author    = {Ueli M. Maurer and
               Pierre E. Schmid},
  title     = {A Calculus for Security Bootstrapping in Distributed Systems},
  journal   = {Journal of Computer Security},
  volume    = {4},
  number    = {1},
  pages     = {55--80},
  year      = {1996},
  url       = {https://doi.org/10.3233/JCS-1996-4104},
  doi       = {10.3233/JCS-1996-4104},
  timestamp = {Fri, 26 May 2017 22:53:13 +0200},
  biburl    = {https://dblp.org/rec/journals/jcs/MaurerS96.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{ThayerSG10,
  author    = {F. Javier Thayer and
               Vipin Swarup and
               Joshua D. Guttman},
  title     = {Metric Strand Spaces for Locale Authentication Protocols},
  booktitle = {Trust Management, {IFIP} {WG} 11.11},
  series    = {{IFIP} Advances in Information and Communication Technology},
  volume    = {321},
  pages     = {79--94},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-13446-3\_6},
  doi       = {10.1007/978-3-642-13446-3\_6},
  timestamp = {Sat, 19 Oct 2019 20:14:34 +0200},
  biburl    = {https://dblp.org/rec/conf/ifiptm/ThayerSG10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{BrandsC93,
  author    = {Stefan Brands and
               David Chaum},
  editor    = {Tor Helleseth},
  title     = {Distance-Bounding Protocols (Extended Abstract)},
  booktitle = {Advances in Cryptology - {EUROCRYPT} '93, Workshop on the Theory and
               Application of of Cryptographic Techniques, Lofthus, Norway, May 23-27,
               1993, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {765},
  pages     = {344--359},
  publisher = {Springer},
  year      = {1993},
  url       = {https://doi.org/10.1007/3-540-48285-7\_30},
  doi       = {10.1007/3-540-48285-7\_30},
  timestamp = {Tue, 14 May 2019 10:00:53 +0200},
  biburl    = {https://dblp.org/rec/conf/eurocrypt/BrandsC93.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{RasmussenC10,
  author    = {Kasper Bonne Rasmussen and
               Srdjan Capkun},
  title     = {Realization of {RF} Distance Bounding},
  booktitle = {19th {USENIX} Security Symposium, Washington, DC, USA, August 11-13,
               2010, Proceedings},
  pages     = {389--402},
  publisher = {{USENIX} Association},
  year      = {2010},
  url       = {http://www.usenix.org/events/sec10/tech/full\_papers/Rasmussen.pdf},
  timestamp = {Wed, 04 Jul 2018 13:06:34 +0200},
  biburl    = {https://dblp.org/rec/conf/uss/RasmussenC10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@incollection{MeadowsPPCS07,
  author    = {Catherine A. Meadows and
               Radha Poovendran and
               Dusko Pavlovic and
               LiWu Chang and
               Paul F. Syverson},
  editor    = {Radha Poovendran and
               Sumit Roy and
               Cliff Wang},
  title     = {Distance Bounding Protocols: Authentication Logic Analysis and Collusion
               Attacks},
  booktitle = {Secure Localization and Time Synchronization for Wireless Sensor and
               Ad Hoc Networks},
  series    = {Advances in Information Security},
  volume    = {30},
  pages     = {279--298},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-0-387-46276-9\_12},
  doi       = {10.1007/978-0-387-46276-9\_12},
  timestamp = {Tue, 16 May 2017 14:24:25 +0200},
  biburl    = {https://dblp.org/rec/series/ais/MeadowsPPCS07.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{AvoineT09,
  author    = {Gildas Avoine and
               Aslan Tchamkerten},
  editor    = {Pierangela Samarati and
               Moti Yung and
               Fabio Martinelli and
               Claudio Agostino Ardagna},
  title     = {An Efficient Distance Bounding {RFID} Authentication Protocol: Balancing
               False-Acceptance Rate and Memory Requirement},
  booktitle = {Information Security, 12th International Conference, {ISC} 2009, Pisa,
               Italy, September 7-9, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5735},
  pages     = {250--261},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-04474-8\_21},
  doi       = {10.1007/978-3-642-04474-8\_21},
  timestamp = {Tue, 14 May 2019 10:00:53 +0200},
  biburl    = {https://dblp.org/rec/conf/isw/AvoineT09.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Trujillo-RasuaMA10,
  author    = {Rolando Trujillo{-}Rasua and
               Benjamin Martin and
               Gildas Avoine},
  editor    = {Siddika Berna Ors Yalcin},
  title     = {The Poulidor Distance-Bounding Protocol},
  booktitle = {Radio Frequency Identification: Security and Privacy Issues - 6th
               International Workshop, RFIDSec 2010, Istanbul, Turkey, June 8-9,
               2010, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {6370},
  pages     = {239--257},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-16822-2\_19},
  doi       = {10.1007/978-3-642-16822-2\_19},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/conf/rfidsec/Trujillo-RasuaMA10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{HanckeK05,
  author    = {Gerhard P. Hancke and
               Markus G. Kuhn},
  title     = {An {RFID} Distance Bounding Protocol},
  booktitle = {First International Conference on Security and Privacy for Emerging
               Areas in Communications Networks, SecureComm 2005, Athens, Greece,
               5-9 September, 2005},
  pages     = {67--73},
  publisher = {{IEEE}},
  year      = {2005},
  url       = {https://doi.org/10.1109/SECURECOMM.2005.56},
  doi       = {10.1109/SECURECOMM.2005.56},
  timestamp = {Wed, 16 Oct 2019 14:14:54 +0200},
  biburl    = {https://dblp.org/rec/conf/securecomm/HanckeK05.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{MauwTT16,
  author    = {Sjouke Mauw and
               Jorge Toro{-}Pozo and
               Rolando Trujillo{-}Rasua},
  title     = {A Class of Precomputation-Based Distance-Bounding Protocols},
  booktitle = {{IEEE} European Symposium on Security and Privacy, EuroS{\&}P
               2016, Saarbr{\"{u}}cken, Germany, March 21-24, 2016},
  pages     = {97--111},
  publisher = {{IEEE}},
  year      = {2016},
  url       = {https://doi.org/10.1109/EuroSP.2016.19},
  doi       = {10.1109/EuroSP.2016.19},
  timestamp = {Wed, 16 Oct 2019 14:14:55 +0200},
  biburl    = {https://dblp.org/rec/conf/eurosp/MauwTT16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{KimA09,
  author    = {Chong Hee Kim and
               Gildas Avoine},
  editor    = {Juan A. Garay and
               Atsuko Miyaji and
               Akira Otsuka},
  title     = {{RFID} Distance Bounding Protocol with Mixed Challenges to Prevent
               Relay Attacks},
  booktitle = {Cryptology and Network Security, 8th International Conference, {CANS}
               2009, Kanazawa, Japan, December 12-14, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5888},
  pages     = {119--133},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-10433-6\_9},
  doi       = {10.1007/978-3-642-10433-6\_9},
  timestamp = {Tue, 14 May 2019 10:00:50 +0200},
  biburl    = {https://dblp.org/rec/conf/cans/KimA09.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{MunillaP08,
  author    = {Jorge Munilla and
               Alberto Peinado},
  title     = {Distance bounding protocols for {RFID} enhanced by using void-challenges
               and analysis in noisy channels},
  journal   = {Wireless Communications and Mobile Computing},
  volume    = {8},
  number    = {9},
  pages     = {1227--1232},
  year      = {2008},
  url       = {https://doi.org/10.1002/wcm.590},
  doi       = {10.1002/wcm.590},
  timestamp = {Wed, 17 May 2017 14:25:29 +0200},
  biburl    = {https://dblp.org/rec/journals/wicomm/MunillaP08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{ReidNTS07,
  author    = {Jason Reid and
               Juan Manuel Gonz{\'{a}}lez Nieto and
               Tee Tang and
               Bouchra Senadji},
  editor    = {Feng Bao and
               Steven Miller},
  title     = {Detecting relay attacks with timing-based protocols},
  booktitle = {Proceedings of the 2007 {ACM} Symposium on Information, Computer and
               Communications Security, {ASIACCS} 2007, Singapore, March 20-22, 2007},
  pages     = {204--213},
  publisher = {{ACM}},
  year      = {2007},
  url       = {https://doi.org/10.1145/1229285.1229314},
  doi       = {10.1145/1229285.1229314},
  timestamp = {Tue, 06 Nov 2018 11:07:29 +0100},
  biburl    = {https://dblp.org/rec/conf/ccs/ReidNTS07.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{KimAKSP08,
  author    = {Chong Hee Kim and
               Gildas Avoine and
               Fran{\c{c}}ois Koeune and
               Fran{\c{c}}ois{-}Xavier Standaert and
               Olivier Pereira},
  editor    = {Pil Joong Lee and
               Jung Hee Cheon},
  title     = {The Swiss-Knife {RFID} Distance Bounding Protocol},
  booktitle = {Information Security and Cryptology - {ICISC} 2008, 11th International
               Conference, Seoul, Korea, December 3-5, 2008, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {5461},
  pages     = {98--115},
  publisher = {Springer},
  year      = {2008},
  url       = {https://doi.org/10.1007/978-3-642-00730-9\_7},
  doi       = {10.1007/978-3-642-00730-9\_7},
  timestamp = {Tue, 14 May 2019 10:00:36 +0200},
  biburl    = {https://dblp.org/rec/conf/icisc/KimAKSP08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{AvoineBGGLOR17,
  author    = {Gildas Avoine and
               Xavier Bultel and
               S{\'{e}}bastien Gambs and
               David G{\'{e}}rault and
               Pascal Lafourcade and
               Cristina Onete and
               Jean{-}Marc Robert},
  title     = {A Terrorist-fraud Resistant and Extractor-free Anonymous Distance-bounding
               Protocol},
  journal   = {{IACR} Cryptology ePrint Archive},
  volume    = {2017},
  pages     = {297},
  year      = {2017},
  url       = {http://eprint.iacr.org/2017/297},
  timestamp = {Tue, 14 Aug 2018 17:08:17 +0200},
  biburl    = {https://dblp.org/rec/journals/iacr/AvoineBGGLOR17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{ChothiaGRBT15,
  author    = {Tom Chothia and
               Flavio D. Garcia and
               Joeri de Ruiter and
               Jordi van den Breekel and
               Matthew Thompson},
  editor    = {Rainer B{\"{o}}hme and
               Tatsuaki Okamoto},
  title     = {Relay Cost Bounding for Contactless {EMV} Payments},
  booktitle = {Financial Cryptography and Data Security - 19th International Conference,
               {FC} 2015, San Juan, Puerto Rico, January 26-30, 2015, Revised Selected
               Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {8975},
  pages     = {189--206},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-662-47854-7\_11},
  doi       = {10.1007/978-3-662-47854-7\_11},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/conf/fc/ChothiaGRBT15.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{MauwSTT19,
  author    = {Sjouke Mauw and
               Zach Smith and
               Jorge Toro{-}Pozo and
               Rolando Trujillo{-}Rasua},
  editor    = {Lorenzo Cavallaro and
               Johannes Kinder and
               XiaoFeng Wang and
               Jonathan Katz},
  title     = {Post-Collusion Security and Distance Bounding},
  booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on Computer and
               Communications Security, {CCS} 2019, London, UK, November 11-15, 2019},
  pages     = {941--958},
  publisher = {{ACM}},
  year      = {2019},
  url       = {https://doi.org/10.1145/3319535.3345651},
  doi       = {10.1145/3319535.3345651},
  timestamp = {Fri, 08 Nov 2019 12:58:49 +0100},
  biburl    = {https://dblp.org/rec/conf/ccs/MauwSTT19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DebantD19,
  author    = {Alexandre Debant and
               St{\'{e}}phanie Delaune},
  editor    = {Flemming Nielson and
               David Sands},
  title     = {Symbolic Verification of Distance Bounding Protocols},
  booktitle = {Principles of Security and Trust - 8th International Conference, {POST}
               2019, Held as Part of the European Joint Conferences on Theory and
               Practice of Software, {ETAPS} 2019, Prague, Czech Republic, April
               6-11, 2019, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {11426},
  pages     = {149--174},
  publisher = {Springer},
  year      = {2019},
  url       = {https://doi.org/10.1007/978-3-030-17138-4\_7},
  doi       = {10.1007/978-3-030-17138-4\_7},
  timestamp = {Fri, 31 Jan 2020 21:32:30 +0100},
  biburl    = {https://dblp.org/rec/conf/post/DebantD19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Desmedt88,
  author={Yvo Desmedt},
  title={Major security problems with the `unforgeable'
                  (feige)-fiat-shamir proofs of identity and how to
                  overcome them},
  booktitle={SECURICOM'88},
  year={1988},
  pages={15--17}
}

@inproceedings{AlTurkiKKNST18,
  author    = {Musab A. AlTurki and
               Max I. Kanovich and
               Tajana Ban Kirigin and
               Vivek Nigam and
               Andre Scedrov and
               Carolyn L. Talcott},
  editor    = {David Lie and
               Mohammad Mannan},
  title     = {Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn
               Family of Protocols},
  booktitle = {Proceedings of the 2018 Workshop on Cyber-Physical Systems Security
               and PrivaCy, CPS-SPC@CCS 2018, Toronto, ON, Canada, October 19, 2018},
  pages     = {60--71},
  publisher = {{ACM}},
  year      = {2018},
  url       = {https://doi.org/10.1145/3264888.3264895},
  doi       = {10.1145/3264888.3264895},
  timestamp = {Wed, 21 Nov 2018 12:44:06 +0100},
  biburl    = {https://dblp.org/rec/conf/ccs/AlTurkiKKNST18.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{KanovichKNST17,
  author    = {Max I. Kanovich and
               Tajana Ban Kirigin and
               Vivek Nigam and
               Andre Scedrov and
               Carolyn L. Talcott},
  title     = {Time, computational complexity, and probability in the analysis of
               distance-bounding protocols},
  journal   = {Journal of Computer Security},
  volume    = {25},
  number    = {6},
  pages     = {585--630},
  year      = {2017},
  url       = {https://doi.org/10.3233/JCS-0560},
  doi       = {10.3233/JCS-0560},
  timestamp = {Wed, 30 Aug 2017 15:38:06 +0200},
  biburl    = {https://dblp.org/rec/journals/jcs/KanovichKNST17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{KanovichKNST16,
  author    = {Max I. Kanovich and
               Tajana Ban Kirigin and
               Vivek Nigam and
               Andre Scedrov and
               Carolyn L. Talcott},
  editor    = {Martin Fr{\"{a}}nzle and
               Nicolas Markey},
  title     = {Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed
               Systems},
  booktitle = {Formal Modeling and Analysis of Timed Systems - 14th International
               Conference, {FORMATS} 2016, Quebec, QC, Canada, August 24-26, 2016,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9884},
  pages     = {228--244},
  publisher = {Springer},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-44878-7\_14},
  doi       = {10.1007/978-3-319-44878-7\_14},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/conf/formats/KanovichKNST16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{AlTurkiKKNST19,
  author    = {Musab A. AlTurki and
               Tajana Ban Kirigin and
               Max I. Kanovich and
               Vivek Nigam and
               Andre Scedrov and
               Carolyn L. Talcott},
  editor    = {Joshua D. Guttman and
               Carl E. Landwehr and
               Jos{\'{e}} Meseguer and
               Dusko Pavlovic},
  title     = {A Multiset Rewriting Model for Specifying and Verifying Timing Aspects
               of Security Protocols},
  booktitle = {Foundations of Security, Protocols, and Equational Reasoning - Essays
               Dedicated to Catherine A. Meadows},
  series    = {Lecture Notes in Computer Science},
  volume    = {11565},
  pages     = {192--213},
  publisher = {Springer},
  year      = {2019},
  url       = {https://doi.org/10.1007/978-3-030-19052-1\_13},
  doi       = {10.1007/978-3-030-19052-1\_13},
  timestamp = {Fri, 24 May 2019 17:45:03 +0200},
  biburl    = {https://dblp.org/rec/conf/birthday/AlTurkiKKNST19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}