{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T07:30:27Z","timestamp":1773300627293,"version":"3.50.1"},"reference-count":107,"publisher":"Springer Science and Business Media LLC","issue":"S1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Synthese"],"published-print":{"date-parts":[[2010,12]]},"DOI":"10.1007\/s11229-010-9765-8","type":"journal-article","created":{"date-parts":[[2010,8,23]],"date-time":"2010-08-23T07:56:18Z","timestamp":1282550178000},"page":"51-76","source":"Crossref","is-referenced-by-count":11,"title":["To know or not to know: epistemic approaches to security protocol verification"],"prefix":"10.1007","volume":"177","author":[{"given":"Francien","family":"Dechesne","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yanjing","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,8,24]]},"reference":[{"key":"9765_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., & Cortier, V. (2004). Deciding knowledge in security protocols under equational theories. In ICALP04, LNCS (Vol. 3142, pp. 46\u201358).","DOI":"10.1007\/978-3-540-27836-8_7"},{"key":"9765_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., & Fournet, C. (2001). Mobile values, new names, and secure communication. In POPL \u201901 (pp. 104\u2013115).","DOI":"10.1145\/360204.360213"},{"issue":"2","key":"9765_CR3","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s00145-001-0014-7","volume":"15","author":"M. Abadi","year":"2002","unstructured":"Abadi M., Rogaway P. (2002) Reconciling two views of cryptography (The computational soundness of formal encryption). Journal of Cryptology 15(2): 103\u2013127","journal-title":"Journal of Cryptology"},{"key":"9765_CR4","doi-asserted-by":"crossref","unstructured":"Abadi, M., & Tuttle, M. R. (1991). A semantics for a logic of authentication (extended abstract). In PODC \u201991 (pp. 201\u2013216). New York, NY, USA.","DOI":"10.1145\/112600.112618"},{"key":"9765_CR5","unstructured":"Accorsi, R., Basin, D., & Vigano, L. (2001). Towards an awareness-based semantics for security protocol analysis. In Logical aspects of cryptographic protocol verification, ENTCS (Vol. 55, pp. 5\u201324)."},{"key":"9765_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T. A., Mang, F. Y. C., Qadeer, S., Rajamani, S. K., & Tasiran, S. (1998). Mocha: Modularity in model checking. In CAV\u201998, LNCS (Vol. 1427, pp. 521\u2013525).","DOI":"10.1007\/BFb0028774"},{"key":"9765_CR7","doi-asserted-by":"crossref","unstructured":"Alur, R., \u010cern\u00fd, P., & Chaudhuri, S. (2007). Model checking on trees with path equivalences. In TACAS\u201907, LNCS (Vol. 4424, pp. 664\u2013678).","DOI":"10.1007\/978-3-540-71209-1_51"},{"key":"9765_CR8","doi-asserted-by":"crossref","unstructured":"Alur, R., \u010cern\u00fd, P., & Zdancewic, S. (2006). Preserving secrecy under refinement. In ICALP\u201906, LNCS (Vol. 4052, pp. 107\u2013118).","DOI":"10.1007\/11787006_10"},{"key":"9765_CR9","doi-asserted-by":"crossref","unstructured":"Anderson, R., & Needham, R. (1995). Programming Satan\u2019s computer. In J. Leeuwen (Ed.), Computer science today, LNCS (Vol. 1000, Chap. 26, pp. 426\u2013440). Berlin\/Heidelberg: Springer.","DOI":"10.1007\/BFb0015258"},{"key":"9765_CR10","unstructured":"Baltag, A., Moss, L. S., & Solecki, S. (1999). The logic of public announcements, common knowledge, and private suspicions. Technical Report SEN-R9922, CWI, Amsterdam."},{"issue":"2","key":"9765_CR11","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/s11229-008-9369-8","volume":"165","author":"A. Baltag","year":"2008","unstructured":"Baltag A., Smets S. (2008) Probabilistic dynamic belief revision. Synthese 165(2): 179\u2013202","journal-title":"Synthese"},{"key":"9765_CR12","doi-asserted-by":"crossref","unstructured":"Baskar, A., Ramanujam, R., & Suresh, S. P. (2007). Knowledge-based modelling of voting protocols. In TARK \u201907 (pp. 62\u201371).","DOI":"10.1145\/1324249.1324261"},{"key":"9765_CR13","doi-asserted-by":"crossref","unstructured":"Bhargava, M., & Palamidessi, C. (2005). Probabilistic anonymity. In CONCUR\u201905, LNCS (Vol. 3653, pp. 171\u2013185).","DOI":"10.1007\/11539452_16"},{"key":"9765_CR14","doi-asserted-by":"crossref","unstructured":"Bieber, P. (1990). A logic of communication in hostile environment. In Computer security foundations workshop III (pp. 14\u201322).","DOI":"10.1109\/CSFW.1990.128181"},{"issue":"4","key":"9765_CR15","doi-asserted-by":"crossref","first-page":"463","DOI":"10.3166\/jancl.19.463-487","volume":"19","author":"I. Boureanu","year":"2009","unstructured":"Boureanu I., Cohen M., Lomuscio A. (2009) Automatic verification of temporal-epistemic properties of cryptographic protocols. Journal of Applied Non-Classical Logics 19(4): 463\u2013487","journal-title":"Journal of Applied Non-Classical Logics"},{"issue":"3","key":"9765_CR16","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"D. Brookes","year":"1984","unstructured":"Brookes D., Hoare C. A. R., Roscoe A. W. (1984) A theory of communicating sequential processes. Journal of the ACM 31(3): 560\u2013599","journal-title":"Journal of the ACM"},{"key":"9765_CR17","doi-asserted-by":"crossref","unstructured":"Burrows, M., Abadi, M., & Needham, R. (1989). A logic of authentication. In Proceedings of the royal society of london, Series A, Mathematical and Physical Sciences (Vol. 426(1871), pp. 233\u2013271).","DOI":"10.1145\/74850.74852"},{"key":"9765_CR18","doi-asserted-by":"crossref","unstructured":"Chadha, R., Delaune, S., & Kremer, S. (2009). Epistemic logic for the applied pi calculus. In FMOODS \u201909\/FORTE \u201909, LNCS (Vol. 5522, pp. 182\u2013197).","DOI":"10.1007\/978-3-642-02138-1_12"},{"key":"9765_CR19","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/BF00206326","volume":"1","author":"D. Chaum","year":"1988","unstructured":"Chaum D. (1988) The dining cryptographers problem: Unconditional sender and receiver untraceability. Journal of Cryptology 1: 65\u201375","journal-title":"Journal of Cryptology"},{"key":"9765_CR20","doi-asserted-by":"crossref","unstructured":"Chaum, D., Cr\u00e9peau, C., & Damgard, I. (1988). Multiparty unconditionally secure protocols. In STOC \u201988 (pp. 11\u201319).","DOI":"10.1145\/62212.62214"},{"key":"9765_CR21","doi-asserted-by":"crossref","unstructured":"Ciob\u00e2c\u0103, S., Delaune, S., & Kremer, S. (2009). Computing knowledge in security protocols under convergent equational theories. In CADE-22, LNCS (Vol. 5663, pp. 355\u2013370).","DOI":"10.1007\/978-3-642-02959-2_27"},{"key":"9765_CR22","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke E.M., Grumberg O., Peled D.A. (1999) Model checking. The MIT Press, Cambridge"},{"key":"9765_CR23","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Jha, S., & Marrero, W. R. (1998). Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In PROCOMET \u201998 (pp. 87\u2013106).","DOI":"10.1007\/978-0-387-35358-6_10"},{"key":"9765_CR24","unstructured":"Cohen, M., & Dam, M. (2005a). A completeness result for BAN logic. In Methods for modalities (pp. 202\u2013219)."},{"key":"9765_CR25","unstructured":"Cohen, M., & Dam, M. (2005b). Logical omniscience in the semantics of BAN logic. In FCS\u201905 (pp. 121\u2013132)."},{"key":"9765_CR26","doi-asserted-by":"crossref","unstructured":"Cohen, M., & Dam, M. (2007). A complete axiomatization of knowledge and cryptography. In LICS (pp. 77\u201388).","DOI":"10.1109\/LICS.2007.4"},{"key":"9765_CR27","unstructured":"Cohen, M., Dam, M., Lomuscio, A., & Russo, F. (2009a). Abstraction in model checking multi-agent systems. In AAMAS \u201909 (pp. 945\u2013952)."},{"key":"9765_CR28","doi-asserted-by":"crossref","unstructured":"Cohen, M., Lomuscio, A., Dam, M., & Qu, H. (2009b). A symmetry reduction technique for model checking temporal epistemic logic. In IJCAI\u201909 (pp. 721\u2013726).","DOI":"10.1007\/978-3-642-00431-5_7"},{"key":"9765_CR29","unstructured":"Cremers, C. J. F. (2006). Scyther\u2014Semantics and verification of security protocols. Ph.D. dissertation, Eindhoven University of Technology."},{"key":"9765_CR30","doi-asserted-by":"crossref","unstructured":"Dechesne, F., Mousavi, M. R., & Orzan, S. (2007). Operational and epistemic approaches to protocol analysis: Bridging the gap. In LPAR (pp. 226\u2013241).","DOI":"10.1007\/978-3-540-75560-9_18"},{"key":"9765_CR31","doi-asserted-by":"crossref","unstructured":"Dechesne, F., Orzan, S., & Wang, Y. (2008). Refinement of Kripke models for dynamics. In ICTAC\u201908, LNCS (Vol. 5160, pp. 111\u2013125).","DOI":"10.1007\/978-3-540-85762-4_8"},{"key":"9765_CR32","unstructured":"Dechesne, F., & Wang, Y. (2007). Dynamic epistemic verification of security protocols: Framework and case study. In A meeting of the minds (LORI 2008), Texts in Computer Science (Vol. 8, pp. 129\u2013144)."},{"key":"9765_CR33","doi-asserted-by":"crossref","unstructured":"Delaune, S., Kremer, S., & Ryan, M. (2006). Coercion-resistance and receipt-freeness in electronic voting. In CSFW\u201906 (pp. 28\u201342).","DOI":"10.1109\/CSFW.2006.8"},{"issue":"4","key":"9765_CR34","doi-asserted-by":"crossref","first-page":"435","DOI":"10.3233\/JCS-2009-0340","volume":"17","author":"S. Delaune","year":"2009","unstructured":"Delaune S., Kremer S., Ryan M. (2009) Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17(4): 435\u2013487","journal-title":"Journal of Computer Security"},{"key":"9765_CR35","unstructured":"Dixon, C., Carmen, Fisher, M., & van der Hoek, W. (2003). Using temporal logics of knowledge in the formal verification of security protocols. Technical Report ULCS-03-022, University of Liverpool, Department of Computer Science."},{"issue":"2","key":"9765_CR36","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev D., Yao A. (1983) On the security of public key protocols. IEEE Transactions on Information Theory 29(2): 198\u2013208","journal-title":"IEEE Transactions on Information Theory"},{"key":"9765_CR37","unstructured":"Durgin, N. A., Lincoln, P. D., Mitchell, J. C., & Scedrov, A. (1999). Undecidability of bounded security protocols. In Proceedings of the workshop on formal methods and security protocols."},{"issue":"2","key":"9765_CR38","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0020-0190(87)90097-4","volume":"24","author":"E. A. Emerson","year":"1987","unstructured":"Emerson E. A. (1987) Uniform inevitability is tree automaton ineffable. Information Processing Letters 24(2): 77\u201379","journal-title":"Information Processing Letters"},{"key":"9765_CR39","doi-asserted-by":"crossref","unstructured":"Engelhardt, K., Gammie, P., & van der Meyden, R. (2007). Model checking knowledge and linear time: PSPACE cases. In LFCS (pp. 195\u2013211)","DOI":"10.1007\/978-3-540-72734-7_14"},{"key":"9765_CR40","unstructured":"Engelhardt, K., Van Der Meyden, R., & Su, K. (2002). Modal logics with a linear hierarchy of local propositional quantifiers. In Advances in modal logic (Vol. 9, pp. 9\u201330)."},{"key":"9765_CR41","doi-asserted-by":"crossref","unstructured":"Fagin, R., Halpern, J. Y., Moses, Y., & Vardi, M. Y. (1995a). Knowledge-based programs. In Symposium on principles of distributed computing (pp. 153\u2013163).","DOI":"10.1145\/224964.224982"},{"key":"9765_CR42","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin R., Halpern J.Y., Vardi M.Y., Moses Y. (1995b) Reasoning about knowledge. MIT Press, Cambridge, MA, USA"},{"key":"9765_CR43","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/s001459900004","volume":"9","author":"M.J. Fischer","year":"1996","unstructured":"Fischer M.J., Wright R.N. (1996) Bounds on secret key exchange using a random deal of cards. Journal of Cryptology 9: 71\u201399","journal-title":"Journal of Cryptology"},{"key":"9765_CR44","unstructured":"Focardi, R., Gorrieri, R., & Martinelli, F. (2004). Classification of security properties (Part II: Network Security), In LNCS (Vol. 2946, pp. 139\u2013185). Springer."},{"key":"9765_CR45","doi-asserted-by":"crossref","unstructured":"Gammie, P., & van der Meyden, R. (2004). MCK: Model checking the logic of knowledge. In CAV\u201904, LNCS (Vol. 3114\u00a0pp. 256\u2013259). Springer.","DOI":"10.1007\/978-3-540-27813-9_41"},{"key":"9765_CR46","doi-asserted-by":"crossref","unstructured":"Garcia, F. D., Hasuo, I., van Rossum, P., & Pieters, W. (2005). Provable anonymity. In Formal Methods in Security Engineering \u201905 (pp. 63\u201372).","DOI":"10.1145\/1103576.1103585"},{"issue":"2","key":"9765_CR47","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1023\/A:1008222603071","volume":"6","author":"J. Gerbrandy","year":"1997","unstructured":"Gerbrandy J., Groeneveld W. (1997) Reasoning about information change. Journal of Logic, Language and Information 6(2): 147\u2013169","journal-title":"Journal of Logic, Language and Information"},{"key":"9765_CR48","doi-asserted-by":"crossref","unstructured":"Gong, L., Needham, R., & Yahalom, R. (1990). Reasoning about belief in cryptographic protocols. In Research in security and privacy. pp. 234\u2013248.","DOI":"10.1109\/RISP.1990.63854"},{"key":"9765_CR49","doi-asserted-by":"crossref","unstructured":"Halpern, J., & O\u2019Neill, K. (2002). Secrecy in multiagent systems. In Proc. 15th IEEE Computer Security Foundations Workshop (pp. 32\u201346).","DOI":"10.1109\/CSFW.2002.1021805"},{"issue":"3","key":"9765_CR50","doi-asserted-by":"crossref","first-page":"483","DOI":"10.3233\/JCS-2005-13305","volume":"13","author":"J. Halpern","year":"2005","unstructured":"Halpern J., O\u2019Neill K. (2005) Anonymity and information hiding in multiagent systems. Journal of Computer Security 13(3): 483\u2013514","journal-title":"Journal of Computer Security"},{"issue":"4","key":"9765_CR51","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/BF01784885","volume":"3","author":"J. Y. Halpern","year":"1989","unstructured":"Halpern J. Y., Fagin R. (1989) Modelling knowledge and action in distributed systems. Distributed Computing 3(4): 159\u2013177","journal-title":"Distributed Computing"},{"issue":"3","key":"9765_CR52","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1145\/79147.79161","volume":"37","author":"J. Y. Halpern","year":"1990","unstructured":"Halpern J. Y., Moses Y. (1990) Knowledge and common knowledge in a distributed environment. Journal of the ACM 37(3): 549\u2013587","journal-title":"Journal of the ACM"},{"key":"9765_CR53","doi-asserted-by":"crossref","unstructured":"Halpern, J. Y., Moses, Y., & Vardi, M. Y. (1994). Algorithmic knowledge. In TARK \u201994 (pp. 255\u2013266).","DOI":"10.1016\/B978-1-4832-1453-5.50022-2"},{"key":"9765_CR54","doi-asserted-by":"crossref","unstructured":"Halpern, J. Y., & Pucella, R. (2003a). Modeling adversaries in a logic for security protocol analysis. In Formal aspects of security, LNCS (Vol. 2629, pp. 87\u2013100). Springer.","DOI":"10.1007\/978-3-540-40981-6_11"},{"issue":"1","key":"9765_CR55","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/605434.605436","volume":"6","author":"J. Y. Halpern","year":"2003","unstructured":"Halpern J. Y., Pucella R. (2003) On the relationship between strand spaces and multi-agent systems. ACM Transactions on Information and System Security 6(1): 43\u201370","journal-title":"ACM Transactions on Information and System Security"},{"key":"9765_CR56","doi-asserted-by":"crossref","unstructured":"Halpern, J. Y., & Pucella, R. (2010). Dealing with logical omniscience: Expressiveness and pragmatics. Artificial Intelligence. doi: 10.1016\/j.artint.2010.04.009 .","DOI":"10.1016\/j.artint.2010.04.009"},{"key":"9765_CR57","doi-asserted-by":"crossref","unstructured":"Halpern, J. Y., & Vardi, M. Y. (1986). The complexity of reasoning about knowledge and time. In STOC \u201986 (pp. 304\u2013315).","DOI":"10.1145\/12130.12161"},{"key":"9765_CR58","doi-asserted-by":"crossref","unstructured":"Halpern, J. Y., & Vardi, M. Y. (1991). Model checking vs. theorem proving: A manifesto. In Artificial intelligence and mathematical theory of computation: Papers in honor of John McCarthy (pp. 151\u2013176). Academic Press Professional, Inc.","DOI":"10.1016\/B978-0-12-450010-5.50015-3"},{"issue":"2\u20133","key":"9765_CR59","first-page":"191","volume":"7","author":"J. C. Herzog","year":"1999","unstructured":"Herzog J. C., Guttman J. D. (1999) Strand spaces: Proving security protocols correct. Journal of Computer Security 7(2\u20133): 191\u2013230","journal-title":"Journal of Computer Security"},{"key":"9765_CR60","volume-title":"Knowledge and belief: An introduction to the logic of the two notions","author":"J. Hintikka","year":"1962","unstructured":"Hintikka J. (1962) Knowledge and belief: An introduction to the logic of the two notions. Cornell University Press, Ithaca, NY"},{"key":"9765_CR61","first-page":"289","volume-title":"Information, interaction and agency","author":"A. Hommersom","year":"2005","unstructured":"Hommersom A., Meyer J.-J., Vink E. (2005) Update semantics of security protocols. In: Hoek W. (ed.) Information, interaction and agency. Springer, Berlin, pp 289\u2013327"},{"issue":"2","key":"9765_CR62","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1007\/s11229-009-9552-6","volume":"169","author":"T. Hoshi","year":"2009","unstructured":"Hoshi T., Yap A. (2009) Dynamic epistemic logic with branching temporal structures. Synthese 169(2): 259\u2013281","journal-title":"Synthese"},{"key":"9765_CR63","unstructured":"Hunter, A., & Delgrande, J. P. (2007). Belief change and cryptographic protocol verification. In AAAI (pp. 427\u2013433)."},{"key":"9765_CR64","doi-asserted-by":"crossref","unstructured":"Jonker, H. L., & de Vink, E. P. (2006). Formalising receipt-freeness. In Information security, LNCS (Vol. 4176, pp. 476\u2013488).","DOI":"10.1007\/11836810_34"},{"key":"9765_CR65","unstructured":"Jonker, H. L., & Pieters, W. (2006). Receipt-freeness as a special case of anonymity in epistemic logic. In Workshop On trustworthy elections 2006."},{"issue":"1","key":"9765_CR66","doi-asserted-by":"crossref","first-page":"313","DOI":"10.3233\/FUN-2008-851-422","volume":"85","author":"M. Kacprzak","year":"2008","unstructured":"Kacprzak M., Nabia\u0142ek W., Niewiadomski A., Penczek W., P\u00f3\u0142rola A., Szreter M., Wo\u017ana B., Zbrzezny A. (2008) VerICS 2007\u2014A model checker for knowledge and real-time. Fundamenta Informaticae 85(1): 313\u2013328","journal-title":"Fundamenta Informaticae"},{"key":"9765_CR67","doi-asserted-by":"crossref","unstructured":"Kramer, S. (2007). Logical concepts in cryptography. Ph.D. thesis, EPFL.","DOI":"10.1145\/1345189.1345205"},{"issue":"1","key":"9765_CR68","doi-asserted-by":"crossref","first-page":"219","DOI":"10.2307\/2273878","volume":"52","author":"H. L\u00e4uchli","year":"1987","unstructured":"L\u00e4uchli H., Savioz C. (1987) Monadic second order definable relations on the binary tree. The Journal of Symbolic Logic 52(1): 219\u2013226","journal-title":"The Journal of Symbolic Logic"},{"issue":"3","key":"9765_CR69","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1145\/1324215.1324231","volume":"38","author":"A. Lomuscio","year":"2007","unstructured":"Lomuscio A., Penczek W. (2007) Symbolic model checking for temporal-epistemic logics. SIGACT News 38(3): 77\u201399","journal-title":"SIGACT News"},{"key":"9765_CR70","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Qu, H., & Raimondi, F. (2009). MCMAS: A model checker for the verification of multi-agent systems. In CAV\u201909, LNCS (Vol. 5643, pp. 682\u2013688).","DOI":"10.1007\/978-3-642-02658-4_55"},{"key":"9765_CR71","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., & Raimondi, F. (2006a). The complexity of model checking concurrent programs against CTLK specifications. In AAMAS \u201906 (pp. 548\u2013550).","DOI":"10.1145\/1160633.1160733"},{"key":"9765_CR72","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., & Raimondi, F. (2006b). MCMAS: A model checker for multi-agent systems. In TACAS \u201906, LNCS (Vol. 3920, pp. 450\u2013454).","DOI":"10.1007\/11691372_31"},{"key":"9765_CR73","doi-asserted-by":"crossref","unstructured":"Lowe, G. (1996). Breaking and fixing the needham-schroeder public-key protocol using FDR. In TACAS \u201996, LNCS (Vol. 1055, pp. 147\u2013166).","DOI":"10.1007\/3-540-61042-1_43"},{"issue":"12","key":"9765_CR74","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. M. Needham","year":"1978","unstructured":"Needham R. M., Schroeder M. D. (1978) Using encryption for authentication in large networks of computers. Communications of the ACM 21(12): 993\u2013999","journal-title":"Communications of the ACM"},{"key":"9765_CR75","unstructured":"Orzan, S. (2005). LYS. Available from http:\/\/www.mobanet.nl\/simona\/lys\/ ."},{"key":"9765_CR76","doi-asserted-by":"crossref","unstructured":"Parikh, R., & Ramanujam, R. (1985). Distributed processes and the logic of knowledge. In Logic of programs, LNCS (Vol. 193, pp. 256\u2013268).","DOI":"10.1007\/3-540-15648-8_21"},{"issue":"4","key":"9765_CR77","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1023\/A:1025007018583","volume":"12","author":"R. Parikh","year":"2003","unstructured":"Parikh R., Ramanujam R. (2003) A knowledge based semantics of messages. Journal of Logic, Language and Information 12(4): 453\u2013467","journal-title":"Journal of Logic, Language and Information"},{"key":"9765_CR78","doi-asserted-by":"crossref","unstructured":"Paulson, L. C. (1997). Proving properties of security protocols by induction. In 10th Computer Security Foundations Workshop (pp. 70\u201383).","DOI":"10.1109\/CSFW.1997.596788"},{"key":"9765_CR79","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L. C. Paulson","year":"1998","unstructured":"Paulson L. C. (1998) The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6: 85\u2013128","journal-title":"Journal of Computer Security"},{"key":"9765_CR80","doi-asserted-by":"crossref","unstructured":"Petride, S., & Pucella, R. (2007). Perfect cryptography, S5 knowledge, and algorithmic knowledge. In TARK \u201907 (pp. 239\u2013247).","DOI":"10.1145\/1324249.1324281"},{"key":"9765_CR81","unstructured":"Plaza, J. A. (1989). Logics of public communications. In Proceedings of the 4th international symposium on methodologies for intelligent systems (pp. 201\u2013216)."},{"issue":"2","key":"9765_CR82","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1093\/logcom\/exi078","volume":"16","author":"R. Pucella","year":"2006","unstructured":"Pucella R. (2006) Deductive algorithmic knowledge. Journal of Logic and Computation 16(2): 287\u2013309","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"9765_CR83","doi-asserted-by":"crossref","first-page":"135","DOI":"10.3233\/JCS-2005-13106","volume":"13","author":"R. Ramanujam","year":"2005","unstructured":"Ramanujam R., Suresh S. P. (2005a) Decidability of context-explicit security protocols. Journal of Computer Security 13(1): 135\u2013165","journal-title":"Journal of Computer Security"},{"key":"9765_CR84","unstructured":"Ramanujam, R., & Suresh, S. P. (2005b). Deciding knowledge properties of security protocols. In TARK \u201905 (pp. 219\u2013235)."},{"key":"9765_CR85","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"M. K. Reiter","year":"1998","unstructured":"Reiter M. K., Rubin A. D. (1998) Crowds: Anonymity for web transactions. ACM Transactions on Information and System Security 1: 66\u201392","journal-title":"ACM Transactions on Information and System Security"},{"key":"9765_CR86","volume-title":"Modelling and analysis of security protocols","author":"P. Ryan","year":"2001","unstructured":"Ryan P., Schneider S. (2001) Modelling and analysis of security protocols. Reading, MA, USA, Addison Wesley"},{"key":"9765_CR87","unstructured":"Shilov, N. V., & Garanina, N. O. (2002). Model checking knowledge and fixpoints. In FICS, BRICS notes series (Vol. NS-02-2, pp. 25\u201339)."},{"issue":"3\/4","key":"9765_CR88","doi-asserted-by":"crossref","first-page":"355","DOI":"10.3233\/JCS-2004-123-403","volume":"12","author":"V. Shmatikov","year":"2004","unstructured":"Shmatikov V. (2004) Probabilistic model checking of an anonymity system. Journal of Computer Security 12(3\/4): 355\u2013377","journal-title":"Journal of Computer Security"},{"key":"9765_CR89","unstructured":"Su, K. (2004). Model checking temporal logics of knowledge in distributed systems. In AAAI (pp. 98\u2013103)."},{"issue":"3\u20134","key":"9765_CR90","doi-asserted-by":"crossref","first-page":"317","DOI":"10.3233\/JCS-1992-13-407","volume":"1","author":"P. F. Syverson","year":"1992","unstructured":"Syverson P. F. (1992) Knowledge, belief, and semantics in the analysis of cryptographic protocols. Journal of Computer Security 1(3\u20134): 317\u2013334","journal-title":"Journal of Computer Security"},{"key":"9765_CR91","doi-asserted-by":"crossref","unstructured":"Syverson, P. F., & Stubblebine, S. G. (1999). Group principals and the formalization of anonymity. In World congress on formal methods, LNCS (Vol. 1708, pp. 814\u2013833).","DOI":"10.1007\/3-540-48119-2_45"},{"key":"9765_CR92","unstructured":"Teepe, W. (2006). BAN logic is not \u2018sound\u2019, constructing epistemic logics for security is difficult. In Proceedings of FAMAS\u201906 (pp. 79\u201391)."},{"issue":"5","key":"9765_CR93","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/s10992-008-9099-x","volume":"38","author":"J. Benthem van","year":"2009","unstructured":"van Benthem J., Gerbrandy J., Hoshi T., Pacuit E. (2009) Merging frameworks for interaction. Journal of Philosophical Logic 38(5): 491\u2013526","journal-title":"Journal of Philosophical Logic"},{"key":"9765_CR94","doi-asserted-by":"crossref","unstructured":"van Benthem, J., Gerbrandy, J., & Pacuit, E. (2007). Merging frameworks for interaction: DEL and ETL. In TARK \u201907 (pp. 72\u201381).","DOI":"10.1145\/1324249.1324262"},{"issue":"11","key":"9765_CR95","doi-asserted-by":"crossref","first-page":"1620","DOI":"10.1016\/j.ic.2006.04.006","volume":"204","author":"J. van Benthem","year":"2006","unstructured":"van Benthem J., van Eijck J., Kooi B. (2006) Logics of communication and change. Information and Computation 204(11): 1620\u20131662","journal-title":"Information and Computation"},{"key":"9765_CR96","doi-asserted-by":"crossref","unstructured":"van der Hoek, W., & Wooldridge, M. (2002). Tractable multiagent planning for epistemic goals. In AAMAS \u201902 (pp. 1167\u20131174).","DOI":"10.1145\/545056.545095"},{"key":"9765_CR97","doi-asserted-by":"crossref","unstructured":"van der Meyden, R., & Shilov, N. (1999). Model checking knowledge and time in systems with perfect recall. In FSTTCS \u201999, LNCS (Vol. 1738, pp. 432\u2013445).","DOI":"10.1007\/3-540-46691-6_35"},{"key":"9765_CR98","doi-asserted-by":"crossref","unstructured":"van der Meyden, R., & Su, K. (2004). Symbolic model checking the knowledge of the dining cryptographers. In CSFW \u201904 (pp. 280\u2013291).","DOI":"10.1109\/CSFW.2004.1310747"},{"key":"9765_CR99","doi-asserted-by":"crossref","unstructured":"van der Meyden, R., & Wilke, T. (2007). Preservation of epistemic properties in security protocol implementations. In TARK \u201907 (pp. 212\u2013221).","DOI":"10.1145\/1324249.1324278"},{"issue":"1","key":"9765_CR100","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1023\/A:1026168632319","volume":"75","author":"H. van Ditmarsch","year":"2003","unstructured":"van Ditmarsch H. (2003) The Russian cards problem. Studia Logica 75(1): 31\u201362","journal-title":"Studia Logica"},{"key":"9765_CR101","unstructured":"van Ditmarsch, H. (2008). Unconditionally secure protocols with card deals. Presentation, available at http:\/\/www.cs.otago.ac.nz\/staffpriv\/hans\/lorentz\/niaslorentz.pdf ."},{"key":"9765_CR102","doi-asserted-by":"crossref","unstructured":"van Ditmarsch, H., van der Hoek, W., van der Meyden, R., & Ruan, J. (2006). Model checking Russian cards. In MoChArt 05, ENTCS (Vol. 149(2), pp. 105\u2013123).","DOI":"10.1016\/j.entcs.2005.07.029"},{"key":"9765_CR103","unstructured":"van Eijck, J. (2005). DEMO program and documentation. Available from http:\/\/www.cwi.nl\/~jve\/demo\/ ."},{"key":"9765_CR104","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/j.entcs.2006.08.026","volume":"168","author":"J. van Eijck","year":"2007","unstructured":"van Eijck J., Orzan S. (2007) Epistemic verification of anonymity. Electronic Notes in Theoretical Computer Science 168: 159\u2013174","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9765_CR105","volume-title":"An essay in modal logic","author":"G. H. Von Wright","year":"1951","unstructured":"Von Wright G. H. (1951) An essay in modal logic. North Holland, Amsterdam"},{"key":"9765_CR106","doi-asserted-by":"crossref","unstructured":"Wang, Y., Kuppusamy, L., & van Eijck, J. (2009). Verifying epistemic protocols under common knowledge. In TARK \u201909 (pp. 257\u2013266).","DOI":"10.1145\/1562814.1562848"},{"key":"9765_CR107","unstructured":"Wang, Y., Sietsma, F., & van Eijck, J. (2010). Logic of information flow on communication channels (extended abstract). In AAMAS \u201910 (to appear)."}],"container-title":["Synthese"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/s11229-010-9765-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T23:14:19Z","timestamp":1740438859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11229-010-9765-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,8,24]]},"references-count":107,"journal-issue":{"issue":"S1","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["9765"],"URL":"https:\/\/doi.org\/10.1007\/s11229-010-9765-8","relation":{},"ISSN":["0039-7857","1573-0964"],"issn-type":[{"value":"0039-7857","type":"print"},{"value":"1573-0964","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,8,24]]}}}