@article(r:gordon99,
 author       = {M. Abadi and A. D. Gordon},
 year         = {1999},
 title        = {A Calculus for Cryptographic Protocols: The Spi Calculus},
 journal      = {Information and Computation},
 volume       = {148},
 number       = {1},
 pages        = {1--70},
 doi          = {10.1006/inco.1998.2740},
)
@article(r:abadi02a,
 author       = {M. Abadi and P. Rogaway},
 year         = {2002},
 title        = {Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)},
 journal      = {Journal of Cryptology},
 volume       = {15},
 number       = {2},
 pages        = {103--127},
 doi          = {10.1007/s00145-007-0203-0},
)
@inproceedings(AT91,
 author       = {M. Abadi and M. R. Tuttle},
 year         = {1991},
 title        = {A Semantics for a Logic of Authentication},
 booktitle    = {Proc.~10th ACM Symposium on Principles of Distributed Computing},
 pages        = {201--216},
 doi          = {10.1145/112600.112618},
)
@inproceedings(r:accorsi01,
 author       = {R. Accorsi and D. Basin and L. Vigan\`{o}},
 year         = {2001},
 title        = {Towards an awareness-based semantics for security protocol analysis},
 editor       = {Goubault-Larrecq, Jean},
 booktitle    = {Proc.~Workshop on Logical Aspects of Cryptographic Protocol Verification},
 series       = {Electronic Notes in Theoretical Computer Science},
 volume       = {55.1},
 publisher    = {Elsevier Science Publishers},
 pages        = {5--24},
 doi          = {10.1016/S1571-0661(04)00242-7},
)
@inproceedings(r:backes03,
 author       = {M. Backes and B. Pfitzmann and M. Waidner},
 year         = {2003},
 title        = {A Composable Cryptographic Library with Nested Operations},
 booktitle    = {Proc.~10th ACM Conference on Computer and Communications Security (CCS'03)},
 publisher    = {ACM Press},
 pages        = {220--230},
 doi          = {10.1145/948109.948140},
)
@inproceedings(r:bellare93,
 author       = {M. Bellare and P. Rogaway},
 year         = {1993},
 title        = {Entity Authentication and Key Distribution},
 booktitle    = {Proc.~13th Annual International Cryptology Conference (CRYPTO'93)},
 series       = {Lecture Notes in Computer Science},
 volume       = {773},
 publisher    = {Springer-Verlag},
 pages        = {232--249},
 doi          = {10.1007/3-540-48329-2_21},
)
@inproceedings(r:bieber90,
 author       = {P. Bieber},
 year         = {1990},
 title        = {A Logic of Communication in Hostile Environment},
 booktitle    = {Proc.~3rd IEEE Computer Security Foundations Workshop (CSFW'90)},
 publisher    = {IEEE Computer Society Press},
 pages        = {14--22},
 doi          = {10.1109/CSFW.1990.128181},
)
@article(r:blanchet08,
 author       = {B. Blanchet},
 year         = {2008},
 title        = {A Computationally Sound Mechanized Prover for Security Protocols},
 journal      = {IEEE Transactions on Dependable and Secure Computing},
 volume       = {5},
 number       = {4},
 pages        = {193--207},
 doi          = {10.1109/TDSC.2007.1005},
)
@article(BoureanuCL09,
 author       = {I. Boureanu and M. Cohen and A. Lomuscio},
 year         = {2009},
 title        = {Automatic verification of temporal-epistemic properties of cryptographic protocols},
 journal      = {Journal of Applied Non-Classical Logics},
 volume       = {19},
 number       = {4},
 pages        = {463--487},
 doi          = {10.3166/jancl.19.463-487},
)
@article(r:burrows90,
 author       = {M. Burrows and M. Abadi and R. Needham},
 year         = {1990},
 title        = {A Logic of Authentication},
 journal      = {ACM Transactions on Computer Systems},
 volume       = {8},
 number       = {1},
 pages        = {18--36},
 doi          = {10.1145/77648.77649},
)
@article(r:burrows90a,
 author       = {M. Burrows and M. Abadi and R. M. Needham},
 year         = {1990},
 title        = {Rejoinder to {Nessett}},
 journal      = {ACM Operating Systems Review},
 volume       = {24},
 number       = {2},
 pages        = {39--40},
 doi          = {10.1145/382258.382790},
)
@article(CanettiGH04,
 author       = {R. Canetti and O. Goldreich and S. Halevi},
 year         = {2004},
 title        = {The random oracle methodology, revisited},
 journal      = {J. {ACM}},
 volume       = {51},
 number       = {4},
 pages        = {557--594},
 doi          = {10.1145/1008731.1008734},
)
@inproceedings(r:cervesato99,
 author       = {I. Cervesato and N. Durgin and P. Lincoln and J. Mitchell and A. Scedrov},
 year         = {1999},
 title        = {A Meta-Notation for Protocol Analysis},
 booktitle    = {Proc.~12th IEEE Computer Security Foundations Workshop (CSFW'99)},
 publisher    = {IEEE Computer Society Press},
 pages        = {55--69},
 doi          = {10.1109/CSFW.1999.779762},
)
@phdthesis(cohenthesis,
 author       = {M. Cohen},
 year         = {2007},
 title        = {Logics of Knowledge and Cryptography: Completeness and Expressiveness},
 school       = {KTH},
)
@inproceedings(r:cohen05,
 author       = {M. Cohen and M. Dam},
 year         = {2005},
 title        = {Logical Omniscience in the Semantics of {BAN} Logic},
 booktitle    = {Proc.~Workshop on Foundations of Computer Security (FCS'05)},
)
@inproceedings(r:cohen07,
 author       = {M. Cohen and M. Dam},
 year         = {2007},
 title        = {A complete axiomatization of knowledge and cryptography},
 booktitle    = {Proc.~22nd Annual IEEE Symposium on Logic in Computer Science (LICS'07)},
 doi          = {10.1109/LICS.2007.4},
)
@inproceedings(r:datta05,
 author       = {A. Datta and A. Derek and J. C. Mitchell and V. Shmatikov and M. Turuani},
 year         = {2005},
 title        = {Probabilistic Polynomial-Time Semantics for a Protocol Security Logic},
 booktitle    = {Proc.~32nd Colloquium on Automata, Languages, and Programming (ICALP'05)},
 pages        = {16--29},
 doi          = {10.1007/11523468_2},
)
@article(DechesneWang2010,
 author       = {F. Dechesne and Y. Wang},
 year         = {2010},
 title        = {To know or not to know: epistemic approaches to security protocol verification},
 journal      = {Synthese},
 volume       = {177},
 number       = {1},
 pages        = {51--76},
 doi          = {10.1007/s11229-010-9765-8},
)
@book(r:fagin95,
 author       = {R. Fagin and J. Y. Halpern and Y. Moses and M. Y. Vardi},
 year         = {1995},
 title        = {Reasoning about Knowledge},
 publisher    = {MIT Press},
)
@inproceedings(r:gammie04,
 author       = {P. Gammie and R. van der Meyden},
 year         = {2004},
 title        = {{MCK}: Model Checking the Logic of Knowledge},
 booktitle    = {Proc.~16th International Conference on Computer Aided Verification (CAV'04)},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer-Verlag},
 pages        = {479--483},
 doi          = {10.1007/978-3-540-27813-9_41},
)
@book(r:goldreich01,
 author       = {O. Goldreich},
 year         = {2001},
 title        = {Foundations of Cryptography: Volume 1, Basic Techniques},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511546891},
)
@article(GoldreichGM86,
 author       = {O. Goldreich and S. Goldwasser and Silvio Micali},
 year         = {1986},
 title        = {How to construct random functions},
 journal      = {J. {ACM}},
 volume       = {33},
 number       = {4},
 pages        = {792--807},
 doi          = {10.1145/6490.6503},
)
@inproceedings(r:gong90,
 author       = {L. Gong and R. Needham and R. Yahalom},
 year         = {1990},
 title        = {Reasoning about Belief in Cryptographic Protocols},
 booktitle    = {Proc.~1990 IEEE Symposium on Security and Privacy},
 publisher    = {IEEE Computer Society Press},
 pages        = {234--248},
 doi          = {10.1109/RISP.1990.63854},
)
@inproceedings(r:guttman02a,
 author       = {J. D. Guttman},
 year         = {2002},
 title        = {Security protocol design via authentication tests},
 booktitle    = {Proc.~15th IEEE Computer Security Foundations Workshop (CSFW'02)},
 publisher    = {IEEE Computer Society Press},
 pages        = {92--103},
 doi          = {10.1109/RISP.1990.63854},
)
@article(HM90,
 author       = {J. Y. Halpern and Y. Moses},
 year         = {1990},
 title        = {Knowledge and common knowledge in a distributed environment},
 journal      = {Journal of the ACM},
 volume       = {37},
 number       = {3},
 pages        = {549--587},
 doi          = {10.1145/79147.79161},
)
@inproceedings(r:halpern02e,
 author       = {J. Y. Halpern and R. Pucella},
 year         = {2002},
 title        = {Modeling adversaries in a logic for reasoning about security protocols},
 booktitle    = {Proc.~Workshop on Formal Aspects of Security (FASec'02)},
 series       = {Lecture Notes in Computer Science},
 volume       = {2629},
 pages        = {115--132},
 doi          = {10.1145/79147.79161},
)
@article(HT,
 author       = {J. Y. Halpern and M. R. Tuttle},
 year         = {1993},
 title        = {Knowledge, probability, and adversaries},
 journal      = {Journal of the ACM},
 volume       = {40},
 number       = {4},
 pages        = {917--962},
 doi          = {10.1145/153724.153770},
)
@book(r:hintikka62,
 author       = {J. Hintikka},
 year         = {1962},
 title        = {Knowledge and Belief},
 publisher    = {Cornell University Press},
)
@inproceedings(HuangLM11,
 author       = {X. Huang and C. Luo and R. van der Meyden},
 year         = {2011},
 title        = {Symbolic model checking of probabilistic knowledge},
 booktitle    = {Proc. Conf. on Theoretical Aspects of Rationality and Knowledge (TARK-2011)},
 pages        = {177--186},
 doi          = {10.1145/2000378.2000399},
)
@inproceedings(r:kindred97,
 author       = {D. Kindred and J. M. Wing},
 year         = {1997},
 title        = {Closing the idealization gap with theory generation},
 booktitle    = {DIMACS Workshop on Design and Formal Verification of Security Protocols},
)
@article(LomuscioQR17,
 author       = {A. Lomuscio and H. Qu and F. Raimondi},
 year         = {2017},
 title        = {{MCMAS:} an open-source model checker for the verification of multi-agent systems},
 journal      = {{STTT}},
 volume       = {19},
 number       = {1},
 pages        = {9--30},
 doi          = {10.1007/s10009-015-0378-x},
)
@article(r:lowe98,
 author       = {G. Lowe},
 year         = {1998},
 title        = {Casper: A Compiler for the Analysis of Security Protocols},
 journal      = {Journal of Computer Security},
 volume       = {6},
 pages        = {53--84},
 doi          = {10.3233/JCS-1998-61-204},
)
@article(r:lowe02,
 author       = {G. Lowe},
 year         = {2004},
 title        = {Analysing protocols subject to guessing attacks},
 journal      = {Journal of Computer Security},
 volume       = {12},
 number       = {1},
 pages        = {83--97},
 doi          = {10.3233/JCS-2004-12104},
)
@inproceedings(r:mao95,
 author       = {W. Mao},
 year         = {1995},
 title        = {An augmentation of {BAN}-like logics},
 booktitle    = {Proc.~8th IEEE Computer Security Foundations Workshop (CSFW'95)},
 publisher    = {IEEE Computer Society Press},
 pages        = {44--56},
 doi          = {10.1109/CSFW.1995.518552},
)
@inproceedings(r:meyden04,
 author       = {R. van der Meyden and K. Su},
 year         = {2004},
 title        = {Symbolic Model Checking the Knowledge of the Dining Cryptographers},
 booktitle    = {Proc.~17th IEEE Computer Security Foundations Workshop (CSFW'04)},
 publisher    = {IEEE Computer Society Press},
 pages        = {280--291},
 doi          = {10.1109/CSFW.2004.1310747},
)
@inproceedings(r:micciancio04,
 author       = {D. Micciancio and B. Warinschi},
 year         = {2004},
 title        = {Soundness of Formal Encryption in the Presence of Active Adversaries},
 booktitle    = {Proc.~Theory of Cryptography Conference (TCC'04)},
 series       = {Lecture Notes in Computer Science},
 volume       = {2951},
 publisher    = {Springer-Verlag},
 pages        = {133--151},
 doi          = {10.1007/978-3-540-24638-1_8},
)
@inproceedings(r:mitchell97,
 author       = {J. Mitchell and M. Mitchell and U. Stern},
 year         = {1997},
 title        = {Automated analysis of cryptographic protocols using {Mur$\varphi$}},
 booktitle    = {Proc.~1997 IEEE Symposium on Security and Privacy},
 publisher    = {IEEE Computer Society Press},
 pages        = {141--151},
 doi          = {10.1109/SECPRI.1997.601329},
)
@article(MosesShoham,
 author       = {Y. Moses and Y. Shoham},
 year         = {1993},
 title        = {Belief as defeasible knowledge},
 journal      = {Artificial Intelligence},
 volume       = {64},
 number       = {2},
 pages        = {299--322},
 doi          = {10.1016/0004-3702(93)90107-M},
)
@article(r:nessett90,
 author       = {D. M. Nessett},
 year         = {1990},
 title        = {A Critique of the {Burrows}, {Abadi} and {Needham} Logic},
 journal      = {ACM Operating Systems Review},
 volume       = {24},
 number       = {2},
 pages        = {35--38},
 doi          = {10.1145/382258.382789},
)
@article(r:neuman93,
 author       = {B. C. Neuman and S. Stubblebine},
 year         = {1993},
 title        = {A Note on the Use of Timestamps as Nonces},
 journal      = {ACM Operating Systems Review},
 volume       = {27},
 number       = {2},
 pages        = {10--14},
 doi          = {10.1145/155848.155852},
)
@article(r:paulson98,
 author       = {L. C. Paulson},
 year         = {1998},
 title        = {The Inductive Approach to Verifying Cryptographic Protocols},
 journal      = {Journal of Computer Security},
 volume       = {6},
 number       = {1/2},
 pages        = {85--128},
 doi          = {10.3233/JCS-1998-61-205},
)
@incollection(Pucella2015,
 author       = {R. Pucella},
 year         = {2015},
 title        = {Knowledge and Security},
 editor       = {H. van Ditmarsch and J. Y. Halpern and W. van der Hoek and B. Kooi},
 booktitle    = {Handbook of Epistemic Logic},
 publisher    = {College Publications},
 pages        = {591--655},
)
@inproceedings(r:stubblebine96,
 author       = {S. Stubblebine and R. Wright},
 year         = {1996},
 title        = {An authentication logic supporting synchronization, revocation, and recency},
 booktitle    = {Proc.~3rd ACM Conference on Computer and Communications Security (CCS'96)},
 publisher    = {ACM Press},
 pages        = {95--105},
 doi          = {10.1145/238168.238195},
)
@inproceedings(r:syverson94,
 author       = {P. F. Syverson and P. C. van Oorschot},
 year         = {1994},
 title        = {On Unifying Some Cryptographic Protocol Logics},
 booktitle    = {Proc.~1994 IEEE Symposium on Security and Privacy},
 publisher    = {IEEE Computer Society Press},
 pages        = {14--28},
 doi          = {10.1109/RISP.1994.296595},
)
@article(r:thayer99,
 author       = {F. J. Thayer and J. C. Herzog and J. D. Guttman},
 year         = {1999},
 title        = {Strand Spaces: Proving Security Protocols Correct},
 journal      = {Journal of Computer Security},
 volume       = {7},
 number       = {2/3},
 pages        = {191--230},
 doi          = {10.3233/JCS-1999-72-304},
)
@inproceedings(r:toninho10,
 author       = {B. Toninho and L. Caires},
 year         = {2010},
 title        = {A Spatial-Epistemic Logic for Reasoning about Security Protocols},
 booktitle    = {Proc.~8th International Workshop on Security Issues in Concurrency},
 pages        = {1--15},
 doi          = {10.4204/EPTCS.51.1},
)
@incollection(Ditmarsch12,
 author       = {Van Ditmarsch, H. and Van Eijck, J. and Hernández-Antón, I. and F. Sietsma and S. Simon and Soler-Toscano, F.},
 year         = {2012},
 title        = {Modelling cryptographic keys in dynamic epistemic logic with demo},
 editor       = {J. Bajo P{\'{e}}rez and M. A. S{\'{a}}nchez and P. Mathieu and Rodr{\'{\i}}guez, J. M. Corchado and E. Adam and A. Ortega and Garc{\'{\i}}a, M. N. Moreno and E. Navarro and B. Hirsch and H. L. Cardoso and V. Juli{\'{a}}n},
 booktitle    = {Highlights on Practical Applications of Agents and Multi-Agent Systems},
 publisher    = {Springer},
 pages        = {155--162},
 doi          = {10.1007/978-3-642-28762-6_19},
)
@inproceedings(r:wedel96,
 author       = {G. Wedel and V. Kessler},
 year         = {1996},
 title        = {Formal Semantics for Authentication Logics},
 booktitle    = {Proc.~4th European Symposium on Research in Computer Security (ESORICS'96)},
 series       = {Lecture Notes in Computer Science},
 volume       = {1146},
 publisher    = {Springer-Verlag},
 pages        = {219--241},
 doi          = {10.1007/3-540-61770-1_39},
)