{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T18:40:03Z","timestamp":1736707203667,"version":"3.32.0"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2006,11,1]],"date-time":"2006-11-01T00:00:00Z","timestamp":1162339200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comput Sci Technol"],"published-print":{"date-parts":[[2006,11]]},"DOI":"10.1007\/s11390-006-0932-9","type":"journal-article","created":{"date-parts":[[2006,12,22]],"date-time":"2006-12-22T06:26:24Z","timestamp":1166768784000},"page":"932-943","source":"Crossref","is-referenced-by-count":4,"title":["Verification of Authentication Protocols for Epistemic Goals via SAT Compilation"],"prefix":"10.1007","volume":"21","author":[{"given":"Kai-Le","family":"Su","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qing-Liang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abdul","family":"Sattar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wei-Ya","family":"Yue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guan-Feng","family":"Lv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xi-Zhong","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"932_CR1","volume-title":"Knowledge and Belief","author":"J Hintikka","year":"1962","unstructured":"Hintikka J. Knowledge and Belief. Ithaca, NY: Cornell University Press, 1962."},{"key":"932_CR2","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, Moses Y, Vardi M. Reasoning about Knowledge. Cambridge, MA: MIT Press, 1995."},{"issue":"3","key":"932_CR3","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1145\/146637.146638","volume":"39","author":"J Halpern","year":"1992","unstructured":"Halpern J, Zuck L. A little knowledge goes a long way: Simple knowledge based derivations and correctness proofs for a family of protocols. Journal of the ACM, 1992, 39(3): 449\u2013478.","journal-title":"Journal of the ACM"},{"issue":"1","key":"932_CR4","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1111\/1467-8586.00140","volume":"54","author":"F Stulp","year":"2002","unstructured":"Stulp F, Verbrugge R. A knowledge-based algorithm for the Internet protocol TCP. Bulletin of Economic Research, 2002, 54(1): 69\u201394.","journal-title":"Bulletin of Economic Research"},{"issue":"1","key":"932_CR5","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M Burrows","year":"1990","unstructured":"Burrows M, Abadi M, Needham R M. A logic of authentication. ACM Trans. Computer Systems, 1990, 8(1): 18\u201336.","journal-title":"ACM Trans. Computer Systems"},{"doi-asserted-by":"crossref","unstructured":"Li Gong, Roger Needham, Raphael Yahalom. Reasoning about beliefs in cryptographic protocols. In Proc. IEEE Computer Society Symposium on Research in Security and Privacy, Los Alamitos, California, 1990, IEEE Computer Society Press, pp.234\u2013248.","key":"932_CR6","DOI":"10.1109\/RISP.1990.63854"},{"doi-asserted-by":"crossref","unstructured":"Abadi M, Tuttle M R. A semantics for a logic of authentication. In Proc. the 10th Annual ACM Symp. Principles of Distributed Computing, Montreal, Canada, 1991, pp.201\u2013216.","key":"932_CR7","DOI":"10.1145\/112600.112618"},{"doi-asserted-by":"crossref","unstructured":"Boyd C, Mao M. On a limitation of BAN logic. In Proc. EUROCRYPT\u201993, Lofthus, Norway: Springer-Verlag, LNCS 765, 1993, pp.240\u2013247.","key":"932_CR8","DOI":"10.1007\/3-540-48285-7_20"},{"doi-asserted-by":"crossref","unstructured":"P van Oorschot. Extending cryptographic logics of belief to key agreement. In Proc. 1st ACM Conf. Computer and Communications Security, Fairfax, USA, Nov. 1993, pp.232\u2013243.","key":"932_CR9","DOI":"10.1145\/168588.168617"},{"doi-asserted-by":"crossref","unstructured":"P F Syverson, P C van Oorschot. A unified cryptographic protocol logic. Technical Report 5540-227, CHACS, Naval Research Lab, 1996.","key":"932_CR10","DOI":"10.21236\/ADA464967"},{"unstructured":"Kaile Su, Guanfeng Lv, Yan Zhang. Reasoning about knowledge by variable forgetting. In Proc. the 9th Int. Conf. Principles of Knowledge Representation and Reasoning KR-2004, Whistler, Canada, June 2004, pp.576\u2013586.","key":"932_CR11"},{"doi-asserted-by":"crossref","unstructured":"Lowe G. A hierarchy of authentication specifications. In Proc. 10th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Rockport, USA, 1997, pp.31\u201343.","key":"932_CR12","DOI":"10.1109\/CSFW.1997.596782"},{"issue":"4","key":"932_CR13","first-page":"337","volume":"35","author":"Su Kaile","year":"April 2005","unstructured":"Kaile Su, Guanfeng Lv, Qingliang Chen. Knowledge structure approach to verification of authentication protocols. Science in China, Series E: Information Sciences, April 2005, 35(4): 337\u2013351.","journal-title":"Science in China, Series E: Information Sciences"},{"issue":"12","key":"932_CR14","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. Using encryption for authentication in large networks of computers. Communication of the ACM, 1978, 21(12): 993\u2013999.","journal-title":"Communication of the ACM"},{"doi-asserted-by":"crossref","unstructured":"Gavin Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. Tools and Algorithms for the Construction and Analysis of Systems, Margaria and Steffen (eds.), LNCS 1055, Passau, Germany: Springer Verlag, 1996, pp.147\u2013166.","key":"932_CR15","DOI":"10.1007\/3-540-61042-1_43"},{"key":"932_CR16","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S Kripke","year":"1963","unstructured":"Kripke S. A semantical analysis of modal logic. I: Normal modal propositional calculi. Z. Math. Logik Grundl. Math., 1963, 9: 67\u201396.","journal-title":"Z. Math. Logik Grundl. Math."},{"unstructured":"Fangzhen Lin. On strongest necessary and weakest sufficient conditions. In Proc. Seventh Int. Conf. Principles of Knowledge Representation and Reasoning, Breckenridge, Colorado, USA, April 11\u201315, 2000, pp.167\u2013175.","key":"932_CR17"},{"issue":"8","key":"932_CR18","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"Aug. 1983","unstructured":"Dolev D, Yao A C. On the security of public-key protocols. IEEE Trans. Information Theory, Aug. 1983, 29(8): 198\u2013208.","journal-title":"IEEE Trans. Information Theory"},{"unstructured":"Durgin N, Lincoln P, Mitchell J, Scedrov A. Undecidability of bounded security protocols. In Proc. Workshop on Formal Methods and Security Protocols (FMSP\u201999), Trento, Italy, 1999, http:\/\/citeseer.nj.nec.com\/durgin99undecidability.html .","key":"932_CR19"},{"doi-asserted-by":"crossref","unstructured":"Iliano Cervesato, Catherine Meadows, Dusko Pavlovic. An encapsulated authentication logic for reasoning about key distribution protocol. In Eighteenth Computer Security Foundations Workshop \u2014 CSFW-18, IEEE Computer Society Press, Aix-en-Provence, France, 20\u201322 June, 2005, pp.48\u201361.","key":"932_CR20","DOI":"10.1109\/CSFW.2005.7"},{"issue":"4","key":"932_CR21","doi-asserted-by":"crossref","first-page":"677","DOI":"10.3233\/JCS-2003-11407","volume":"11","author":"Nancy A Durgin","year":"2003","unstructured":"Nancy A Durgin, John C Mitchell, Dusko Pavlovic. A compositional logic for proving security properties of protocols. Journal of Computer Security, 2003, 11(4): 677\u2013722.","journal-title":"Journal of Computer Security"},{"unstructured":"F Javier Thayer, Jonathan C Herzog, Joshua D Guttman. Strand spaces. Technical Report, The MITRE Corporation, Nov. 1997.","key":"932_CR22"},{"doi-asserted-by":"crossref","unstructured":"John V Franco, Michal Kouril, John S Schlipf et al. SBSAT: A state-based, BDD-based satisfiability solver. In Proc. the Theory and Applications of Satisfiability Testing, 6th Int. Conf., SAT 2003., Santa Margherita Ligure, Italy, Springer, LNCS 2919, 2003, pp.398\u2013410.","key":"932_CR23","DOI":"10.1007\/978-3-540-24605-3_30"},{"doi-asserted-by":"crossref","unstructured":"Pierre Bieber. A logic of communication in hostile environment. In Proc. the 3rd IEEE Computer Security Foundations Workshop, Franconia, USA, IEEE Computer Society Press, June 1990, pp.14\u201322.","key":"932_CR24","DOI":"10.1109\/CSFW.1990.128181"},{"unstructured":"Clarke E, Jha S Marrero. A machine checkable logic of knowledge for specifying security properties of electronic commerce protocols. In Proc. 13th IEEE Annual Symposium on Logic in Computer Science LICS98 Workshop on Formal Methods and Security Protocols, Indianapolis, Indiana, June 21\u201324, 1998, http:\/\/citeseer.ist.psu.edu\/clarke98machine.html .","key":"932_CR25"},{"doi-asserted-by":"crossref","unstructured":"Paul Syverson. Towards a strand semantics for authentication logic. Electronic Notes in Theoretical Computer Science, 1999, http:\/\/www.elsevier.nl\/locate\/entcs\/volume20.html .","key":"932_CR26","DOI":"10.1016\/S1571-0661(04)80072-0"},{"issue":"1","key":"932_CR27","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/605434.605436","volume":"6","author":"Joseph Y Halpern","year":"2003","unstructured":"Joseph Y Halpern, Riccardo Pucella. On the relationship between strand spaces and multi-agent systems. ACM Trans. Inf. Syst. Secur., 2003, 6(1): 43\u201370.","journal-title":"ACM Trans. Inf. Syst. Secur."},{"doi-asserted-by":"crossref","unstructured":"Anupam Datta, Ante Derek, John C Mitchell, Dusko Pavlovic. A derivation system for security protocols and its logical formalization. In 16th IEEE Computer Security Foundations Workshop CSFW-16 2003, Pacific Grove, CA, USA, IEEE Computer Society, June 30\u2013July 2, 2003, pp.109\u2013125.","key":"932_CR28","DOI":"10.1109\/CSFW.2003.1212708"},{"issue":"7","key":"932_CR29","first-page":"1097","volume":"41","author":"Li Mengjun","year":"July 2004","unstructured":"Li Mengjun, Li Zhoujun, Chen Huowang. A survey of security protocol verification based on process algebra. Chinese J. Computer Research and Development, July 2004, 41(7): 1097\u20131103.","journal-title":"Chinese J. Computer Research and Development"},{"doi-asserted-by":"crossref","unstructured":"Abadi M, Gordon A. A calculus for cryptographic protocols: The spi calculus. In Proc. 4th ACM Conf. Computer and Communication Security, Zurich, Switzerland, April 1997, pp.36\u201347.","key":"932_CR30","DOI":"10.1145\/266420.266432"},{"issue":"2","key":"932_CR31","first-page":"199","volume":"47","author":"Huai Jinpeng","year":"Feb. 2004","unstructured":"Huai Jinpeng, Li Xianxian. Algebra model and security analysis for cryptographic protocols. Science in China, Series F: Information Sciences, Feb. 2004, 47(2): 199\u2013220.","journal-title":"Science in China, Series F: Information Sciences"},{"issue":"4","key":"932_CR32","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1007\/BF02944758","volume":"19","author":"Rui Xue","year":"2004","unstructured":"Xue Rui, Feng Deng-Guo. New semantic model for authentication protocols in ASMs. J. Comput. Sci. & Tech., 2004, 19(4): 555\u2013563.","journal-title":"J. Comput. Sci. & Tech."},{"issue":"4","key":"932_CR33","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1145\/363516.363528","volume":"9","author":"E M Clarke","year":"October 2000","unstructured":"Clarke E M, Jha S, Marrero W. Verifying security protocols with Brutus. ACM Trans. Software Engineering and Methodology, October 2000, 9(4): 443\u2013487.","journal-title":"ACM Trans. Software Engineering and Methodology"},{"issue":"1, 2","key":"932_CR34","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","volume":"9","author":"D Song","year":"2001","unstructured":"Song D, Berezin S, Perrig A. Athena: A novel approach to efficient automatic security protocol analysis. Journal of Computer Security, 2001, 9(1, 2): 47\u201374.","journal-title":"Journal of Computer Security"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-006-0932-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-006-0932-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-006-0932-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T18:02:27Z","timestamp":1736704947000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-006-0932-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11]]},"references-count":34,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2006,11]]}},"alternative-id":["932"],"URL":"https:\/\/doi.org\/10.1007\/s11390-006-0932-9","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"type":"print","value":"1000-9000"},{"type":"electronic","value":"1860-4749"}],"subject":[],"published":{"date-parts":[[2006,11]]}}}