Logic Program And Its Application To The Verification Of Security Protocols

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.