逻辑程序及其在安全协议验证中的应用
|
摘要
非单调推理是人工智能领域中一类重要的常识推理,其中包含缺省逻辑、自认知逻辑等内容。
自认知逻辑的稳定集和扩充可用于刻划主体(agent)的推理能力以及认知状态,是自认知逻辑重要的研究内容。本文给出了稳定集的一种等价表示方法,该方法可以比较简洁、统一地描述多自认知逻辑中的相关概念。
在多自认知逻辑中,本文基于对主体之间认知能力的不同假设,提出了四种稳定集,讨论了它们之间的关系,并以一种稳定集为例,给出了其语义表示,并引入了相应的扩充概念。另外,文中也讨论了一种可以描述环境的扩充。
自认知逻辑程序可以看成是自认知逻辑的一种简化,可以比较方便地用于推理。本文分别讨论了单主体和多主体的自认知逻辑程序。对于单主体的情形,给出了一种不动点语义,证明了它和完全Bonatti稳定集等价,并可以转化为扩展逻辑程序的回答集语义。对于多主体的情形,根据对主体认知情况的不同处理,提出了两类稳定集:P稳定集和广义稳定集。在给出了多自认知逻辑程序的三值语义模型后,证明了该语义是和广义稳定集相互对应的。而当三值语义简化为二值时,对应的是P稳定集。P稳定集可看成是自认知逻辑程序中稳定集的自然推广,而广义稳定集可看成是Bonatti稳定集的推广。
对于有序逻辑程序,本文基于不动点原理,提出了处理优先序的新方法,统一了多种已有的回答集语义,得到了一类新的回答集语义。通过证明和举例详细比较了各种回答集语义之间的强弱关系,给出了它们在集合包含关系意义下的哈斯图,证明了各种回答集语义在包含关系下形成格的结构。
安全协议是保证网络通信安全的重要内容。形式化方法是验证安全协议的一种重要方法。本文提出了一种复合型安全协议,在同一协议中结合了在线可信第三方和离线可信第三方两种通信方式。对SVO逻辑和Kailar逻辑进行扩充,增强其表达能力,特别是非单调推理能力,给出了协议验证的新方法。另外,作为逻辑程序的一种应用,本文也提出了基于多自认知逻辑程序的验证方法,并以KM等协议为例,验证了协议的非否认性和公平性等性质。
Nonmonotonic reasoning systems including default logic and autoepistemic logic are important in the commonsense reasoning of artificial intelligence.
The stable sets and expansions of autoepistemic logic are important to denote the reasoning ability and the epistemic status of the agent. A new characterization of the stable sets of the autoepistemic logic is given and it can be extended to multi-autoepistemic logic easily.
There are different cases of the epistemic ability between the agents in the multi-autoepistemic logic. Based on the different assumptions of the epistemic ability four kinds of the stable sets are introduced and their relationship are discussed. The corresponding expansions and semantics of multi-autoepistemic logic are also given. Moreover, a kind of expansion in which the environment can be described is presented too.
Autoepistemic logic program is a simplification of the autoepistemic logic. The single agent and multi-agent autoepistemic logic program are introduced. For the single agent case, a fixed-point semantics which can be translated to the answer set semantics of the general logic program is given and is proved equivalent to the complete Bonatti stable set. For the multi-agent case, two kinds of stable sets are discussed, that is the P stable set and the general stable set. The three-value semantics for the multi-agent autoepistemic logic program corresponds to general stable semantics and the simplified two-value semantics corresponds to the P stable set. P stable set can be viewed as the generalization of the stable set in autoepistemic logic and general stable set can be viewed as the generalization of the Bonatti stable set in autoepistemic logic.
Based on the fixpoint principle, some new methods are introduced to treat the prior orders among the rules in ordered logic program. That results in a new class of answer set semantics for ordered logic program including several kinds of already existed semantics. The diverse answer set semantics are compared in detail and a Hasse diagram with respect to set inclusive relations for the semantics is given. It is proved that the answer set semantics form a lattice structure.
Security protocols are important for the security of the network communications and formal methods are important for verifying the security protocols. Combined with the online trusted third part(TTP) protocol and the off-line TTP protocol, a new compound security protocol is introduced. Based on the extended systems of SVO logic and Kailar logic which can process nonmonotonic reasoning, the new methods for the security protocol verification are given. Moreover, the verification methods using general logic program and multi-agent autoepistemic logic program are also discussed. With these new methods, some non-repudiation protocols are proved to have the property of non-repudiation and fairness.
自认知逻辑的稳定集和扩充可用于刻划主体(agent)的推理能力以及认知状态,是自认知逻辑重要的研究内容。本文给出了稳定集的一种等价表示方法,该方法可以比较简洁、统一地描述多自认知逻辑中的相关概念。
在多自认知逻辑中,本文基于对主体之间认知能力的不同假设,提出了四种稳定集,讨论了它们之间的关系,并以一种稳定集为例,给出了其语义表示,并引入了相应的扩充概念。另外,文中也讨论了一种可以描述环境的扩充。
自认知逻辑程序可以看成是自认知逻辑的一种简化,可以比较方便地用于推理。本文分别讨论了单主体和多主体的自认知逻辑程序。对于单主体的情形,给出了一种不动点语义,证明了它和完全Bonatti稳定集等价,并可以转化为扩展逻辑程序的回答集语义。对于多主体的情形,根据对主体认知情况的不同处理,提出了两类稳定集:P稳定集和广义稳定集。在给出了多自认知逻辑程序的三值语义模型后,证明了该语义是和广义稳定集相互对应的。而当三值语义简化为二值时,对应的是P稳定集。P稳定集可看成是自认知逻辑程序中稳定集的自然推广,而广义稳定集可看成是Bonatti稳定集的推广。
对于有序逻辑程序,本文基于不动点原理,提出了处理优先序的新方法,统一了多种已有的回答集语义,得到了一类新的回答集语义。通过证明和举例详细比较了各种回答集语义之间的强弱关系,给出了它们在集合包含关系意义下的哈斯图,证明了各种回答集语义在包含关系下形成格的结构。
安全协议是保证网络通信安全的重要内容。形式化方法是验证安全协议的一种重要方法。本文提出了一种复合型安全协议,在同一协议中结合了在线可信第三方和离线可信第三方两种通信方式。对SVO逻辑和Kailar逻辑进行扩充,增强其表达能力,特别是非单调推理能力,给出了协议验证的新方法。另外,作为逻辑程序的一种应用,本文也提出了基于多自认知逻辑程序的验证方法,并以KM等协议为例,验证了协议的非否认性和公平性等性质。
Nonmonotonic reasoning systems including default logic and autoepistemic logic are important in the commonsense reasoning of artificial intelligence.
The stable sets and expansions of autoepistemic logic are important to denote the reasoning ability and the epistemic status of the agent. A new characterization of the stable sets of the autoepistemic logic is given and it can be extended to multi-autoepistemic logic easily.
There are different cases of the epistemic ability between the agents in the multi-autoepistemic logic. Based on the different assumptions of the epistemic ability four kinds of the stable sets are introduced and their relationship are discussed. The corresponding expansions and semantics of multi-autoepistemic logic are also given. Moreover, a kind of expansion in which the environment can be described is presented too.
Autoepistemic logic program is a simplification of the autoepistemic logic. The single agent and multi-agent autoepistemic logic program are introduced. For the single agent case, a fixed-point semantics which can be translated to the answer set semantics of the general logic program is given and is proved equivalent to the complete Bonatti stable set. For the multi-agent case, two kinds of stable sets are discussed, that is the P stable set and the general stable set. The three-value semantics for the multi-agent autoepistemic logic program corresponds to general stable semantics and the simplified two-value semantics corresponds to the P stable set. P stable set can be viewed as the generalization of the stable set in autoepistemic logic and general stable set can be viewed as the generalization of the Bonatti stable set in autoepistemic logic.
Based on the fixpoint principle, some new methods are introduced to treat the prior orders among the rules in ordered logic program. That results in a new class of answer set semantics for ordered logic program including several kinds of already existed semantics. The diverse answer set semantics are compared in detail and a Hasse diagram with respect to set inclusive relations for the semantics is given. It is proved that the answer set semantics form a lattice structure.
Security protocols are important for the security of the network communications and formal methods are important for verifying the security protocols. Combined with the online trusted third part(TTP) protocol and the off-line TTP protocol, a new compound security protocol is introduced. Based on the extended systems of SVO logic and Kailar logic which can process nonmonotonic reasoning, the new methods for the security protocol verification are given. Moreover, the verification methods using general logic program and multi-agent autoepistemic logic program are also discussed. With these new methods, some non-repudiation protocols are proved to have the property of non-repudiation and fairness.
引文
[1] Abadi M.,Glew N.,Horne B,Certified Email with a Light On-Line Trusted Third Party: Design and Implementation.In:Proceedings of the Eleventh International World Wide Web Conference.2002: 387-395
[2] Abadi M.,Blanchet B.Analyzing security protocols with secrecy types and logic programs. Journal of the ACM.2005.52(1): 102-146
[3] Abadi M.,Blanchet B.Computer-Assisted Verification of a Protocol for Certified Email. Science of Computer Programming,2005, 58(1-2): 3-27
[4] Aiello L., Massacci F. Verifying security protocols as planning in logic programming.ACM Transactions on Computational Logic. 2001.2(4): 542-580
[5] Amati G.,Aiello L.,Pirri F. Intuitionistic Autoepistemic Logic. Studia Logica 1997.59(1):103-120
[6] Amgoud.L.,Cayrol.C.A Reasoning Model Based on the production of acceptable Arguments. Annals of Mathematics and Artificial Intelligence. 2002.34:197-215
[7] Antoniou G., Sperschneider V. Operational Concepts of Nonmonotonic Logics Part 2: Autoepistemic Logic. Artificial Intelligence Review. 1998.12(6): 431-443
[8] Balduccini.M. and Gelfond. M. Diagnostic reasoning with a-prolog.Theory and Practive of Logic Programming.2003.3(4):425-461
[9] Baral,C.Knowledge representation,reasoning and declarative problem solving.Cambridge University Press.2003
[10] Blanchet B. Automatic verification of cryptographic protocols: a logic programming approach.In:Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. Uppsala, Sweden. 2003:1-3
[11] Blanchet B. and Podelski A.Verification of Cryptographic Protocols: Tagging Enforces Termination. Theoretical Computer Science. 2005.333(1-2):67-90
[12] Bonatti P.Autoepistemic Logic Programming.Journal of Automated Reasoning. 1994,13(1): 35-67
[13] Bonatti P.Autoepistemic Logics as a Unifying Framework for the Semantics of Logic Programs. Journal of Logic Programming.1995.22(2): 91-149
[14] Bondarenko.A.,Dung.P.M., Kowalski.R.A.,Toni.F., An abstract,argumentation-theoretic approach to default reasoning.Artificial Intelligence.1997.97:63-101
[15] Brewka G. Preferred subtheories: an extended logical framework for default reasoning. in: Proceedings 11th International Joint Conference on Artificial Intelligence (IJCAI-89), Detroit, MI, Morgan Kaufmann,San Mateo, CA, 1989.1043-1048
[16] Brewka G.and Eiter T.Preferred Answer Sets for Extended Logic Programs Artificial Intelligence,Artificial Intelligence 1999.109: 297-356
[17] Brewka G. and Eiter T. Preferred answer sets for extended logic programs. In Cohn, A. Schubert, L. and Shapiro, S., eds., Proceedings of the Sixth International Conference on the Principles of Knowledge Representation and Reasoning,1998:86-97
[18] Brewka, G., and Eiter, T.. Prioritizing default logic. In H¨olldobler, S., ed., Intellectics and Computational Logic — Papers in Honour of Wolfgang Bibel. Kluwer Academic Publishers. 2000:27-45
[19] Brewka, G. Adding priorities and specificity to default logic. In Pereira, L., and Pearce, D., eds., European Workshop on Logics in Artificial Intelligence (JELIA’94), Lecture Notes in Artificial Intelligence,. Springer Verlag.1994:247-260
[20] Brewka, G. Well-founded semantics for extended logic programs with dynamic preferences. Journal of Artificial Intelligence Research.1996.4:19-36
[21] Brignoli,G. Costantini,S.Antona,O.Characterizing and computing stable models of logic programs:the non-stratified case.Proceedings of the conference on information technology.Bhubaneswar AAAI Press.1999:197-201
[22] Burrows M.,Abadi M.,Needham R. A logic of authentication. ACM Transacion on Computer System. 1990. 8(1):18-36.
[23] Chen, J. Embedding prioritized circumscription into logic programs. In Proc. of the 10th International symposium on Foundations of Intelligent Systems (ISMIS’97), LNAI 1325,Springer-Verlag.1997:50-59
[24] Clark,K.L.,Negation as failure.Logics and Data Bases.Plenum,New York,1978
[25] Cui, B., and Swift, T.. Preference logic grammars:Fixed-point semantics and application to data standardization. Artificial Intelligence.2001
[26] Delgrande, J., Schaub, T., and Tompits, H. A framework for compiling preferences in logic programs. Theory and Practice of Logic Programming.2003.3:129-187
[27] Delgrande, J., and Schaub, T. Expressing preferences in default logic. Artificial Intelligence 2000.123(1-2):41-87
[28] Delgrande, J. Schaub, T. and Tompits,A framework for compiling preferences in logic programs. Theory and Practice of Logic Programming.2002
[29] Denecker M.,Marek W.,Truszczynski W.Uniform semantic treatment of default and autoepistemic logics. Artificial Intelligence.2003.143(1): 79-122
[30] Dung.P.M.On the acceptability of arguments and its fundamental role in nonmonotonic reasoning,logic programming and n-person games,Artificial Intelligence,1995.77: 321-357
[31] Eiter, T. and Lukasiewicz T. Complexity results for explanations in the structural-model approach. Artificial Intelligence 2004. 154:145-198
[32] Eiter, T. and Faber T. A logic programming approach to knowledge-state planning, II:The DLVK System.Artificial Intelligence 2002. 144:157-211
[33] Eiter, T. Faber, W. Leone, N. Computing preferred and weakly preferred answer sets by meta-interpretation in answer set programming. In Provetti, A., and Cao, S., eds., Proceedings AAAI 2001 Spring Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning,AAAI Press. 2001.45-52
[34] Fábrega F., Herzog JC, Guttman JD. Strand spaces: Proving security protocols correct. Journal of Computer Security. 1999.7(10):191-230.
[35] Fages,F.Consistency of clark's completion and the existence of stable models.Journal of Methods of Logic in Computer Science.1994.1:51-60
[36] 范红,冯登国. 安全协议理论与方法. 科学出版社. 2003
[37] Gelder V.,A. Ross,K.,and Schlipf,J. The well-founded semantics for general logic programs.Journal of ACM.1991.38(3):620-650
[38] Gelfond M,Lifschitz V.The stable model semantics for logic programming. In: Proc. of the Fifth Logic Programming Symposium,Cambridge ,Mass.1988:1070-1080
[39] Gelfond,M.,and Leone,N. Logic programming and knowledge representation—The A-Prolog perspective.Artificial Intelligence 2002.138:3-38
[40] Gelfond M., Lifschitz V. Representing actions and change by logic programs, J. Logic Programming 2000.17:301-323
[41] Gelfond M., Lifschitz V. The stable model semantics for logic programming, in: R. Kowalski, K. Bowen (Eds.), Logic Programming: Proc. Fifth Internat.Conference and Symposium, 1988.1070-1080.
[42] Gelfond M., Lifschitz V. Classical negation in logic programs and disjunctive databases.New Generation Computing.1991.9:365-387
[43] Gelfond, M., and Son, T. Reasoning with prioritized defaults. In Dix, J.Pereira, L. and Przymusinski, T., eds., Third International Workshop on Logic Programming and Knowledge Representation,volume 1471 of Lecture Notes in Computer Science, Springer-Verlag.1997:164-223
[44] Gong L., Needham R., Yahalom R. Reasoning about Belief in Cryptographic Protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. 1990. 234-248
[45] Gottlob G.Translating Default Logic into Standard Autoepistemic Logic. Journal of the ACM.1995.42(4):711-740
[46] Grosof, B. Prioritized conflict handling for logic programs.In Maluszynsk, J., ed., Logic Programming: Proceedings of the 1997 International Symposium,The MIT Press. 1997:197-211
[47] Gurgens,S.,Rudolph G. Security analysis of efficient (Un-)fair non-repudiation protocols. Formal Aspects of Computing. 2005. 17(3):260-276
[48] Gurgens S.On the security of fair non-repudiation protocols. International Journal of Information Security. 2005. 4(4): 253-262
[49] Halpern J., Moses Y. Towards a Theory of Knowledge and Ignorance. In. Proceedings of the Non-Monotonic Reasoning Workshop, Mohonk Mountain House, New Paltz.1984:125-143
[50] Inoue, K., and Sakama, C.. Abducing priorities to derive intended conclusions. In Proceedings of the International Joint Conference on Artificial Intelligence,Morgan Kaufmann Publishers. 1999:44-49
[51] Kailar R.Accountability in Electronic Commerce Protocols. IEEE Trans. Software Eng.1996,22(5): 313-328
[52] Kaminski M., Rey G. Revisiting quantification in autoepistemic logic. ACM Transactions on Computational Logic. 2002. 3(4): 542-561
[53] Koch,C. and Leone,N.Stable model checking made easy, in: Proc. IJCAI-99, Stockholm, Sweden, Morgan Kaufmann, San Mateo, CA,1999:70-75
[54] Konolige, K., On the Relation between Default and Autoepistemic Logic, Artificial Intelligence.1988.35:343-382
[55] Konczak K.Graphs and colorings for answer set programming with preferences.Fundamenta Informaticae.2003:1-30
[56] Kremer S.,Markowitch O.Optimistic non-repudiable information exchange. In J. Biemond, editor, 21st Symp.on Information Theory in the Benelux.Wassenaar.The Netherlands.2000:139-146
[57] Kremer S.,Markowitch O. A Multi-Party Non-Repudiation Protocol.In:Sihan Qing, Jan H. P. Eloff Eds.: Information Security for Global Information Infrastructures, Fifteenth Annual Working Conference on Information Security, August 22-24, 2000, Beijing, China.Kluwer.2000: 271-280
[58] Kremer S.,Markowitch O. and Zhou J. An intensive survey of non-repudiation protocols. Computer Communications, 2002.25(17):1606-1621
[59] Kremer S, Markowitch O. Fair multi-party nonrepudiation protocols. International Journal of Information Security. 2003.1(4):223-235
[60] Li L.,Zhang H.,Wang L. An Improved Non- Repudiation Protocol and Its Securty Analysis. Wuhan University Journal of Natural Sciences. 2004.9(3):288-292
[61] Lifschitz,V. Answer set programming and plan generation, Artificial Intelligence. 2002.138:39-54
[62] Linke,T.Graph theoretical characterization and computation of answer sets.In B.Nebel,editor,Proceedings of International Joint Conference on Artificial Intelligence.Morgan Kaufmann Publishers.2001:641-645
[63] Lloyd,J. Foundations of logic programming. Springer-Verlag. 1987
[64] Marek W.,Truszczynski M.Autoepistemic Logic. Journal of the ACM.1991.38(3): 588-619
[65] Marek, V., and Truszczynski, M. Nonmonotonic logic: context-dependent reasoning. Artifical Intelligence.Springer-Verlag.1993
[66] Marek,W. and Subrahmanian,V.S. The relationship between logic program semantics and nonmonotonic reasoning, in: G. Levi, M. Martelli (Eds.), Proc. Sixth Internat. Conference on Logic Programming, Lisbon, Portugal, 1989. 600-617
[67] McCarthy, J. Applications of circumscription to formalizing common-sense knowledge. Artificial Intelligence.1986.28:89-116
[68] McDermott,D. and Doyle,J. Nonmonotonic logic I, Artificial Intelligence 1980.13(1-2):41-72
[69] McDermott,D. Nonmonotonic logic II: Nonmonotonic modal theories, J. ACM 1982.29(1): 33-57
[70] Meadows C.Formal methods for cryptographic protocol analysis: Emerging issues and trends. IEEE Journal on Selected Areas in Communication,2003. 21(1):44-54
[71] Milnikel R. A sequent calculus for skeptical reasoning in autopeistemic logic. In: 10th International Workshop on Non-Monotonic Reasoning (NMR 2004). Whistler. Canada. 2004: 292-296
[72] Milnikel R. Sequent calculi for skeptical reasoning in predicate default logic and other nonmonotonic logics. Annals of Mathematics and Artificial Intelligence. 1995. 44(1-2): 1-34
[73] Moore R.Semantical considerations on nonmonotonic logic. Artificial Intelligence.1985.25:75-94
[74] Moore R.Autoepistemic Logic Revisited. Artificial Intelligence. 1993. 59(1-2): 27-30
[75] Niemel? I. Autoepistemic logic as a unified basis for nonmonotonic reasoning. Doctoral dissertation. Research Report A24. Helsinki University of Technology. Digital Systems Laboratory. Espoo. Finland.1993
[76] Niemel? I., and P. Simons, Smodels—An implementation of the stable model and well-founded semantics for normal logic programs, in: Proc. 4th International Conference on Logic Programming and Non-Monotonic Reasoning, Dagstuhl, Germany, 1997. 421-430
[77] Onieva J.A.,Zhou J.,and Lopez J.Non-repudiation protocols for multiple entities. Computer Communications.2004(27):1608-1616
[78] Paulson L. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security. 1998. 6(1-2): 85-128
[79] Prakken, H. Argument-based logic programming with defeasible priorities. Journal of Applied Non-classical Logics 1997. 7:25-75
[80] Prakken, H. Logical Tools for Modelling Legal Argument.Kluwer Academic Publishers.1997
[81] Przymusinski T. Autoepistemic Logic of Knowledge and Beliefs.Artificial Intelligence.1997.95(1):115-154
[82] Przymusinski T. Three-Valued Nonmonotonic Formalisms and Semantics of Logic Programs. Artificial Intelligence. 1991.49(1-3): 309-343
[83] Przymusinski T. The Well-Founded Semantics Coincides with the Three-Valued Stable Semantics. Fundamenta Informaticae. 1990.13(4):445-463
[84] 卿斯汉,冯登国.信息系统的安全.科学出版社.2003
[85] 卿斯汉.安全协议.清华大学出版社.2005.
[86] 卿斯汉.李改成.公平交换协议的一个形式化模型.中国科学 E 辑.2005,35(2): 161-172
[87] Reiter, R. A logic for default reasoning, Artificial Intelligence 1980.13 (1-2): 81-132
[88] Rintanen Jussi.Lexicographic priorities in default logic.Artificial Intelligence 1998 106:221-265
[89] Sakama C.,Inoue K.Prioritized logic programming and its application to commonsense reasoning.Artificial Intelligence.2000 123:185-222
[90] Schaub, T. and Wang, K.A semantic framework for preference handling in answer set programming Theory and Practice of Logic Programming.2003
[91] Schneider S. Verifying authentication protocols with CSP. In:10th Computer Security Foundations Workshop (CSFW '97). Rockport. Massachusetts. USA. 1997: 3-17
[92] Schwarz G. On Embedding Default Logic into Moore's Autoepistemic Logic. Artificial Intelligence. 1996.80(1-2):349-359
[93] Simons,P. and I. Niemel?, T. Soininen, Extending and implementing the stable model semantics, Artificial Intelligence 2002.138:181-234
[94] St?rk R. Multi-Valued Autoepistemic Logic. Annals of Mathematics and Artificial Intelligence. 1996.18(2-4): 159-174
[95] Syverson. P. and van Oorschot PC.On unifying some cryptographic protocol logics. In:IEEE Computer Society Symposium on Research in Security and Privacy.Oakland:IEEE Computer Society Press.1994:14-28
[96] Toyama K., Kojima T.,Inagaki Y.: Translating Multi-Agent Autoepistemic Logic into Logic Program.Electronic Notes in Theoretical Computer Science.2002. 70(5):1-18
[97] Wang G.,Bao F.,Zhou J.On the Security of a Certified E-Mail Scheme.5th International Conference on Cryptology in India, Chennai, India, December 20-22. Springer,2004:48-60
[98] Wang, K. Zhou, L.And Lin, F. Alternating fixpoint theory for logic programs with priority. In Proc.Int’l Conference on Computational Logic. Springer-Verlag, 2000.164-178
[99] You, J.Wang, X.,and Yuan, L. Nonmonotonic reasoning as prioritizedargumentation. IEEE Transactions on Knowledge and Data Engineering 2001.13(6):968-979
[100] Yuan L. Autoepistemic Logic of First Order and Its Expressive Power.Journal of Automated Reasoning.1994.13(1): 69-82
[101] Yuan L., You J. Goebel R. Disjunctive Logic Programming and Autoepistemic Logic.In: Dix J. (Eds.): Logic Programming and Knowledge Representation, Third International Workshop, LPKR '97. New York, USA. 1997. Lecture Notes in Computer Science 1471.Springer.1998: 85-101
[102] Zhang Yan.Two results for proiritized logic programming. Theory and Practice of Logic Programming. 2003.3:223-242
[103] 周典萃,卿斯汉,周展飞.Kailar 逻辑的缺陷.软件学报. 1999.10(12):1238-1245
[104] 周典萃,卿斯汉,周展飞.一种分析电子商务协议的新工具. 软件学报. 2001. 12(9): 1318-1328
[105] Zhou J.On the Security of a Multi-Party Certified Email Protocol.ICICS. 2004:40-52
[106] Zhou J, Gollmann D. Towards verification of non-repudiation protocols. In: International Refinement Workshop and Formal Methods Pacific. Berlin: Springer-Verlag, 1998. 370-380
[107] Zhou J. On the Security of a Multi-party Certified Email Protocol. In: Information and Communications Security, 6th International Conference.Berlin: Springer-Verlag.2004: 40-52
[108] 朱梧槚,肖奚安. 数理逻辑引论. 南京大学出版社 .1995
[109] 朱梧槚,肖奚安. 数学基础概论. 南京大学出版社 .1996
[2] Abadi M.,Blanchet B.Analyzing security protocols with secrecy types and logic programs. Journal of the ACM.2005.52(1): 102-146
[3] Abadi M.,Blanchet B.Computer-Assisted Verification of a Protocol for Certified Email. Science of Computer Programming,2005, 58(1-2): 3-27
[4] Aiello L., Massacci F. Verifying security protocols as planning in logic programming.ACM Transactions on Computational Logic. 2001.2(4): 542-580
[5] Amati G.,Aiello L.,Pirri F. Intuitionistic Autoepistemic Logic. Studia Logica 1997.59(1):103-120
[6] Amgoud.L.,Cayrol.C.A Reasoning Model Based on the production of acceptable Arguments. Annals of Mathematics and Artificial Intelligence. 2002.34:197-215
[7] Antoniou G., Sperschneider V. Operational Concepts of Nonmonotonic Logics Part 2: Autoepistemic Logic. Artificial Intelligence Review. 1998.12(6): 431-443
[8] Balduccini.M. and Gelfond. M. Diagnostic reasoning with a-prolog.Theory and Practive of Logic Programming.2003.3(4):425-461
[9] Baral,C.Knowledge representation,reasoning and declarative problem solving.Cambridge University Press.2003
[10] Blanchet B. Automatic verification of cryptographic protocols: a logic programming approach.In:Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. Uppsala, Sweden. 2003:1-3
[11] Blanchet B. and Podelski A.Verification of Cryptographic Protocols: Tagging Enforces Termination. Theoretical Computer Science. 2005.333(1-2):67-90
[12] Bonatti P.Autoepistemic Logic Programming.Journal of Automated Reasoning. 1994,13(1): 35-67
[13] Bonatti P.Autoepistemic Logics as a Unifying Framework for the Semantics of Logic Programs. Journal of Logic Programming.1995.22(2): 91-149
[14] Bondarenko.A.,Dung.P.M., Kowalski.R.A.,Toni.F., An abstract,argumentation-theoretic approach to default reasoning.Artificial Intelligence.1997.97:63-101
[15] Brewka G. Preferred subtheories: an extended logical framework for default reasoning. in: Proceedings 11th International Joint Conference on Artificial Intelligence (IJCAI-89), Detroit, MI, Morgan Kaufmann,San Mateo, CA, 1989.1043-1048
[16] Brewka G.and Eiter T.Preferred Answer Sets for Extended Logic Programs Artificial Intelligence,Artificial Intelligence 1999.109: 297-356
[17] Brewka G. and Eiter T. Preferred answer sets for extended logic programs. In Cohn, A. Schubert, L. and Shapiro, S., eds., Proceedings of the Sixth International Conference on the Principles of Knowledge Representation and Reasoning,1998:86-97
[18] Brewka, G., and Eiter, T.. Prioritizing default logic. In H¨olldobler, S., ed., Intellectics and Computational Logic — Papers in Honour of Wolfgang Bibel. Kluwer Academic Publishers. 2000:27-45
[19] Brewka, G. Adding priorities and specificity to default logic. In Pereira, L., and Pearce, D., eds., European Workshop on Logics in Artificial Intelligence (JELIA’94), Lecture Notes in Artificial Intelligence,. Springer Verlag.1994:247-260
[20] Brewka, G. Well-founded semantics for extended logic programs with dynamic preferences. Journal of Artificial Intelligence Research.1996.4:19-36
[21] Brignoli,G. Costantini,S.Antona,O.Characterizing and computing stable models of logic programs:the non-stratified case.Proceedings of the conference on information technology.Bhubaneswar AAAI Press.1999:197-201
[22] Burrows M.,Abadi M.,Needham R. A logic of authentication. ACM Transacion on Computer System. 1990. 8(1):18-36.
[23] Chen, J. Embedding prioritized circumscription into logic programs. In Proc. of the 10th International symposium on Foundations of Intelligent Systems (ISMIS’97), LNAI 1325,Springer-Verlag.1997:50-59
[24] Clark,K.L.,Negation as failure.Logics and Data Bases.Plenum,New York,1978
[25] Cui, B., and Swift, T.. Preference logic grammars:Fixed-point semantics and application to data standardization. Artificial Intelligence.2001
[26] Delgrande, J., Schaub, T., and Tompits, H. A framework for compiling preferences in logic programs. Theory and Practice of Logic Programming.2003.3:129-187
[27] Delgrande, J., and Schaub, T. Expressing preferences in default logic. Artificial Intelligence 2000.123(1-2):41-87
[28] Delgrande, J. Schaub, T. and Tompits,A framework for compiling preferences in logic programs. Theory and Practice of Logic Programming.2002
[29] Denecker M.,Marek W.,Truszczynski W.Uniform semantic treatment of default and autoepistemic logics. Artificial Intelligence.2003.143(1): 79-122
[30] Dung.P.M.On the acceptability of arguments and its fundamental role in nonmonotonic reasoning,logic programming and n-person games,Artificial Intelligence,1995.77: 321-357
[31] Eiter, T. and Lukasiewicz T. Complexity results for explanations in the structural-model approach. Artificial Intelligence 2004. 154:145-198
[32] Eiter, T. and Faber T. A logic programming approach to knowledge-state planning, II:The DLVK System.Artificial Intelligence 2002. 144:157-211
[33] Eiter, T. Faber, W. Leone, N. Computing preferred and weakly preferred answer sets by meta-interpretation in answer set programming. In Provetti, A., and Cao, S., eds., Proceedings AAAI 2001 Spring Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning,AAAI Press. 2001.45-52
[34] Fábrega F., Herzog JC, Guttman JD. Strand spaces: Proving security protocols correct. Journal of Computer Security. 1999.7(10):191-230.
[35] Fages,F.Consistency of clark's completion and the existence of stable models.Journal of Methods of Logic in Computer Science.1994.1:51-60
[36] 范红,冯登国. 安全协议理论与方法. 科学出版社. 2003
[37] Gelder V.,A. Ross,K.,and Schlipf,J. The well-founded semantics for general logic programs.Journal of ACM.1991.38(3):620-650
[38] Gelfond M,Lifschitz V.The stable model semantics for logic programming. In: Proc. of the Fifth Logic Programming Symposium,Cambridge ,Mass.1988:1070-1080
[39] Gelfond,M.,and Leone,N. Logic programming and knowledge representation—The A-Prolog perspective.Artificial Intelligence 2002.138:3-38
[40] Gelfond M., Lifschitz V. Representing actions and change by logic programs, J. Logic Programming 2000.17:301-323
[41] Gelfond M., Lifschitz V. The stable model semantics for logic programming, in: R. Kowalski, K. Bowen (Eds.), Logic Programming: Proc. Fifth Internat.Conference and Symposium, 1988.1070-1080.
[42] Gelfond M., Lifschitz V. Classical negation in logic programs and disjunctive databases.New Generation Computing.1991.9:365-387
[43] Gelfond, M., and Son, T. Reasoning with prioritized defaults. In Dix, J.Pereira, L. and Przymusinski, T., eds., Third International Workshop on Logic Programming and Knowledge Representation,volume 1471 of Lecture Notes in Computer Science, Springer-Verlag.1997:164-223
[44] Gong L., Needham R., Yahalom R. Reasoning about Belief in Cryptographic Protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. 1990. 234-248
[45] Gottlob G.Translating Default Logic into Standard Autoepistemic Logic. Journal of the ACM.1995.42(4):711-740
[46] Grosof, B. Prioritized conflict handling for logic programs.In Maluszynsk, J., ed., Logic Programming: Proceedings of the 1997 International Symposium,The MIT Press. 1997:197-211
[47] Gurgens,S.,Rudolph G. Security analysis of efficient (Un-)fair non-repudiation protocols. Formal Aspects of Computing. 2005. 17(3):260-276
[48] Gurgens S.On the security of fair non-repudiation protocols. International Journal of Information Security. 2005. 4(4): 253-262
[49] Halpern J., Moses Y. Towards a Theory of Knowledge and Ignorance. In. Proceedings of the Non-Monotonic Reasoning Workshop, Mohonk Mountain House, New Paltz.1984:125-143
[50] Inoue, K., and Sakama, C.. Abducing priorities to derive intended conclusions. In Proceedings of the International Joint Conference on Artificial Intelligence,Morgan Kaufmann Publishers. 1999:44-49
[51] Kailar R.Accountability in Electronic Commerce Protocols. IEEE Trans. Software Eng.1996,22(5): 313-328
[52] Kaminski M., Rey G. Revisiting quantification in autoepistemic logic. ACM Transactions on Computational Logic. 2002. 3(4): 542-561
[53] Koch,C. and Leone,N.Stable model checking made easy, in: Proc. IJCAI-99, Stockholm, Sweden, Morgan Kaufmann, San Mateo, CA,1999:70-75
[54] Konolige, K., On the Relation between Default and Autoepistemic Logic, Artificial Intelligence.1988.35:343-382
[55] Konczak K.Graphs and colorings for answer set programming with preferences.Fundamenta Informaticae.2003:1-30
[56] Kremer S.,Markowitch O.Optimistic non-repudiable information exchange. In J. Biemond, editor, 21st Symp.on Information Theory in the Benelux.Wassenaar.The Netherlands.2000:139-146
[57] Kremer S.,Markowitch O. A Multi-Party Non-Repudiation Protocol.In:Sihan Qing, Jan H. P. Eloff Eds.: Information Security for Global Information Infrastructures, Fifteenth Annual Working Conference on Information Security, August 22-24, 2000, Beijing, China.Kluwer.2000: 271-280
[58] Kremer S.,Markowitch O. and Zhou J. An intensive survey of non-repudiation protocols. Computer Communications, 2002.25(17):1606-1621
[59] Kremer S, Markowitch O. Fair multi-party nonrepudiation protocols. International Journal of Information Security. 2003.1(4):223-235
[60] Li L.,Zhang H.,Wang L. An Improved Non- Repudiation Protocol and Its Securty Analysis. Wuhan University Journal of Natural Sciences. 2004.9(3):288-292
[61] Lifschitz,V. Answer set programming and plan generation, Artificial Intelligence. 2002.138:39-54
[62] Linke,T.Graph theoretical characterization and computation of answer sets.In B.Nebel,editor,Proceedings of International Joint Conference on Artificial Intelligence.Morgan Kaufmann Publishers.2001:641-645
[63] Lloyd,J. Foundations of logic programming. Springer-Verlag. 1987
[64] Marek W.,Truszczynski M.Autoepistemic Logic. Journal of the ACM.1991.38(3): 588-619
[65] Marek, V., and Truszczynski, M. Nonmonotonic logic: context-dependent reasoning. Artifical Intelligence.Springer-Verlag.1993
[66] Marek,W. and Subrahmanian,V.S. The relationship between logic program semantics and nonmonotonic reasoning, in: G. Levi, M. Martelli (Eds.), Proc. Sixth Internat. Conference on Logic Programming, Lisbon, Portugal, 1989. 600-617
[67] McCarthy, J. Applications of circumscription to formalizing common-sense knowledge. Artificial Intelligence.1986.28:89-116
[68] McDermott,D. and Doyle,J. Nonmonotonic logic I, Artificial Intelligence 1980.13(1-2):41-72
[69] McDermott,D. Nonmonotonic logic II: Nonmonotonic modal theories, J. ACM 1982.29(1): 33-57
[70] Meadows C.Formal methods for cryptographic protocol analysis: Emerging issues and trends. IEEE Journal on Selected Areas in Communication,2003. 21(1):44-54
[71] Milnikel R. A sequent calculus for skeptical reasoning in autopeistemic logic. In: 10th International Workshop on Non-Monotonic Reasoning (NMR 2004). Whistler. Canada. 2004: 292-296
[72] Milnikel R. Sequent calculi for skeptical reasoning in predicate default logic and other nonmonotonic logics. Annals of Mathematics and Artificial Intelligence. 1995. 44(1-2): 1-34
[73] Moore R.Semantical considerations on nonmonotonic logic. Artificial Intelligence.1985.25:75-94
[74] Moore R.Autoepistemic Logic Revisited. Artificial Intelligence. 1993. 59(1-2): 27-30
[75] Niemel? I. Autoepistemic logic as a unified basis for nonmonotonic reasoning. Doctoral dissertation. Research Report A24. Helsinki University of Technology. Digital Systems Laboratory. Espoo. Finland.1993
[76] Niemel? I., and P. Simons, Smodels—An implementation of the stable model and well-founded semantics for normal logic programs, in: Proc. 4th International Conference on Logic Programming and Non-Monotonic Reasoning, Dagstuhl, Germany, 1997. 421-430
[77] Onieva J.A.,Zhou J.,and Lopez J.Non-repudiation protocols for multiple entities. Computer Communications.2004(27):1608-1616
[78] Paulson L. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security. 1998. 6(1-2): 85-128
[79] Prakken, H. Argument-based logic programming with defeasible priorities. Journal of Applied Non-classical Logics 1997. 7:25-75
[80] Prakken, H. Logical Tools for Modelling Legal Argument.Kluwer Academic Publishers.1997
[81] Przymusinski T. Autoepistemic Logic of Knowledge and Beliefs.Artificial Intelligence.1997.95(1):115-154
[82] Przymusinski T. Three-Valued Nonmonotonic Formalisms and Semantics of Logic Programs. Artificial Intelligence. 1991.49(1-3): 309-343
[83] Przymusinski T. The Well-Founded Semantics Coincides with the Three-Valued Stable Semantics. Fundamenta Informaticae. 1990.13(4):445-463
[84] 卿斯汉,冯登国.信息系统的安全.科学出版社.2003
[85] 卿斯汉.安全协议.清华大学出版社.2005.
[86] 卿斯汉.李改成.公平交换协议的一个形式化模型.中国科学 E 辑.2005,35(2): 161-172
[87] Reiter, R. A logic for default reasoning, Artificial Intelligence 1980.13 (1-2): 81-132
[88] Rintanen Jussi.Lexicographic priorities in default logic.Artificial Intelligence 1998 106:221-265
[89] Sakama C.,Inoue K.Prioritized logic programming and its application to commonsense reasoning.Artificial Intelligence.2000 123:185-222
[90] Schaub, T. and Wang, K.A semantic framework for preference handling in answer set programming Theory and Practice of Logic Programming.2003
[91] Schneider S. Verifying authentication protocols with CSP. In:10th Computer Security Foundations Workshop (CSFW '97). Rockport. Massachusetts. USA. 1997: 3-17
[92] Schwarz G. On Embedding Default Logic into Moore's Autoepistemic Logic. Artificial Intelligence. 1996.80(1-2):349-359
[93] Simons,P. and I. Niemel?, T. Soininen, Extending and implementing the stable model semantics, Artificial Intelligence 2002.138:181-234
[94] St?rk R. Multi-Valued Autoepistemic Logic. Annals of Mathematics and Artificial Intelligence. 1996.18(2-4): 159-174
[95] Syverson. P. and van Oorschot PC.On unifying some cryptographic protocol logics. In:IEEE Computer Society Symposium on Research in Security and Privacy.Oakland:IEEE Computer Society Press.1994:14-28
[96] Toyama K., Kojima T.,Inagaki Y.: Translating Multi-Agent Autoepistemic Logic into Logic Program.Electronic Notes in Theoretical Computer Science.2002. 70(5):1-18
[97] Wang G.,Bao F.,Zhou J.On the Security of a Certified E-Mail Scheme.5th International Conference on Cryptology in India, Chennai, India, December 20-22. Springer,2004:48-60
[98] Wang, K. Zhou, L.And Lin, F. Alternating fixpoint theory for logic programs with priority. In Proc.Int’l Conference on Computational Logic. Springer-Verlag, 2000.164-178
[99] You, J.Wang, X.,and Yuan, L. Nonmonotonic reasoning as prioritizedargumentation. IEEE Transactions on Knowledge and Data Engineering 2001.13(6):968-979
[100] Yuan L. Autoepistemic Logic of First Order and Its Expressive Power.Journal of Automated Reasoning.1994.13(1): 69-82
[101] Yuan L., You J. Goebel R. Disjunctive Logic Programming and Autoepistemic Logic.In: Dix J. (Eds.): Logic Programming and Knowledge Representation, Third International Workshop, LPKR '97. New York, USA. 1997. Lecture Notes in Computer Science 1471.Springer.1998: 85-101
[102] Zhang Yan.Two results for proiritized logic programming. Theory and Practice of Logic Programming. 2003.3:223-242
[103] 周典萃,卿斯汉,周展飞.Kailar 逻辑的缺陷.软件学报. 1999.10(12):1238-1245
[104] 周典萃,卿斯汉,周展飞.一种分析电子商务协议的新工具. 软件学报. 2001. 12(9): 1318-1328
[105] Zhou J.On the Security of a Multi-Party Certified Email Protocol.ICICS. 2004:40-52
[106] Zhou J, Gollmann D. Towards verification of non-repudiation protocols. In: International Refinement Workshop and Formal Methods Pacific. Berlin: Springer-Verlag, 1998. 370-380
[107] Zhou J. On the Security of a Multi-party Certified Email Protocol. In: Information and Communications Security, 6th International Conference.Berlin: Springer-Verlag.2004: 40-52
[108] 朱梧槚,肖奚安. 数理逻辑引论. 南京大学出版社 .1995
[109] 朱梧槚,肖奚安. 数学基础概论. 南京大学出版社 .1996