We illustrate AL SP (Action Language for Security Protocol), a declarative executable specification language for planning attacks to security protocols. AL SP is based on logic programming with negation as failure, and with stable model semantics. In AL SP we can give a declarative specification of a protocol with the natural semantics of send and receive actions which can be performed in parallel. By viewing a protocol trace as a plan to achieve a goal, attacks are (possibly parallel) plans achieving goals that correspond to security violations. Building on results from logic programming and planning, we map the existence of an attack into the existence of a model for the protocol that satisfies the specification of an attack. We show that our liberal model of parallel actions can adequately represent the traditional Dolev-Yao trace-based model used in the formal analysis of security protocols. Specifications in AL SP are executable, as we can automatically search for attacks via an efficient model generator (smodels), implementing the stable model semantics of normal logic programs.

We propose AL/sub SP/ a Declarative Executable Specification Language for Planning Attacks to Security Protocols based on logic programming. In AL/sub SP/ we can give a declarative specification of a protocol with the natural semantics of send and receive actions. We view a protocol trace as a plan to reach a goal, so that attacks are just plans reaching goals that correspond to security violations, which can be also declaratively specified. Building on results from logic programming and planning, we map the existence of an attack to a protocol into the existence of a model for the protocol specification that satisfies the specification of an attack. AL/sub SP/ specifications are executable, as we can automatically search for attacks via any efficient model generator (such as smodels), that implements the stable model semantics of normal logic programs. Thus, we come to a specification language which is easy to use (protocol specifications are expressed at a high level of abstraction, and with an intuitive notation close to their traditional description) still keeping the rigor of a formal specification that, in addition, is executable.

We present a general proof theoretical methodology for default systems. Given a default theory W, D, the default rules D are simply understood as restrictions on the tableaux construction of the logic. Different default approaches approch (such as Reiter, Brewka or Lukaszewicz), the allowable default extensions can be obtained from the default tableau construction. The advantage of our approach, besides being simple and neat, is in its generality: it allows for the development of a default theory for any logic with a tableau formulation, such as intuitionistic logic, linear logic or modal logic.

The need for expressing and using metalevel knowledge is emerging in the design of several kinds of AI systems. The careful distinction between object-level and metalevel notions and the formalization of the latter has first been carried out by logicians for foundational reasons; subsequently, the distinction has been exploited in Artificial Intelligence and Computation Theory, revealing itself to be of great relevance to Automated Deduction and Problem Solving. This paper concentrates on the use of metaknowledge in building knowledge-based systems. In order to introduce the issue, some motivating examples are presented. We then review various paradigms for combining knowledge and metaknowledge, with the aim of abstracting general criteria that should underly the construction of viable AI systems, as far as metaknowledge is concerned. Furthermore, a general overview of the uses of metaknowledge in AI is provided and, among them, we concentrate on inference control, which can be conveniently exercised by formalizing control strategies at the metalevel and by letting the inference engine depend on metalevel descriptions. The technique is presented with the aid of some examples, chosen from practical AI applications, that are expressed in the formalism of Horn clause logic. The issue of self-descriptive systems is then addressed. A system that embodies and can use an adequate description of itself allows for self-evaluation (e.g., the estimate of the resources needed to perform a given task) and for self-modification (e.g., the automatic improvement of deduction performance by profiting from experience gained in previous deductions).