Iliano Cervesato

LPAR Conference 2015 Conference Paper

Modular Multiset Rewriting

• Iliano Cervesato
• Edmund S. L. Lam

Abstract Rule-based languages are being used for ever more ambitious applications. As program size grows however, so does the overhead of team-based development, reusing components, and just keeping a large flat collection of rules from interfering. In this paper, we propose a module system for a small logically-motivated rule-based language. The resulting modules are nothing more than rewrite rules of a specific form, which are themselves just logic formulas. Yet, they provide some of the same features found in advanced module systems such as that of Standard ML, in particular name space separation, support for abstract data types, and parametrization (functors in ML). Our modules also offer essential features for concurrent programming such as facilities for sharing private names. This approach is directly applicable to other rule-based languages, including most forward-chaining logic programming languages and many process algebras.

LFMTP Workshop 2014 Conference Paper

Proof-Theoretic Foundations of Indexing in Logic Programming

• Iliano Cervesato

Indexing is generally viewed as an implementation artifact, indispensable to speed up the execution of logic programs and theorem provers, but with little intrinsically logical about it. We show that indexing can be given a justification in proof theory on the basis of focusing and linearity. We demonstrate this approach on predicate indexing for Horn clauses and several formulations of hereditary Harrop formulas. We also show how to refine this approach to discriminate on function symbols as well.

I&C Journal 2009 Journal Article

Relating state-based and process-based concurrency through linear logic (full-version)

• Iliano Cervesato
• Andre Scedrov

This paper has the purpose of reviewing some of the established relationships between logic and concurrency, and of exploring new ones. Concurrent and distributed systems are notoriously hard to get right. Therefore, following an approach that has proved highly beneficial for sequential programs, much effort has been invested in tracing the foundations of concurrency in logic. The starting points of such investigations have been various idealized languages of concurrent and distributed programming, in particular the well established state-transformation model inspired by Petri nets and multiset rewriting, and the prolific process-based models such as the π -calculus and other process algebras. In nearly all cases, the target of these investigations has been linear logic, a formal language that supports a view of formulas as consumable resources. In the first part of this paper, we review some of these interpretations of concurrent languages into linear logic and observe that, possibly modulo duality, they invariably target a small semantic fragment of linear logic that we call LVobs. In the second part of the paper, we propose a new approach to understanding concurrent and distributed programming as a manifestation of logic, which yields a language that merges those two main paradigms of concurrency. Specifically, we present a new semantics for multiset rewriting founded on an alternative view of linear logic and specifically LVobs. The resulting interpretation is extended with a majority of linear connectives into the language of ω -multisets. This interpretation drops the distinction between multiset elements and rewrite rules, and considerably enriches the expressive power of standard multiset rewriting with embedded rules, choice, replication, and more. Derivations are now primarily viewed as open objects, and are closed only to examine intermediate rewriting states. The resulting language can also be interpreted as a process algebra. For example, a simple translation maps process constructors of the asynchronous π -calculus to rewrite operators. The language of ω -multisets forms the basis for the security protocol specification language MSR 3. With relations to both multiset rewriting and process algebra, it supports specifications that are process-based, state-based, or of a mixed nature, with the potential of combining verification techniques from both worlds. Additionally, its logical underpinning makes it an ideal common ground for systematically comparing protocol specification languages.

I&C Journal 2008 Journal Article

Breaking and fixing public-key Kerberos

• Iliano Cervesato
• Aaron D. Jaggard
• Andre Scedrov
• Joe-Kai Tsay
• Christopher Walstad

We report on a man-in-the-middle attack on PKINIT, the public key extension of the widely deployed Kerberos 5 authentication protocol. This flaw allows an attacker to impersonate Kerberos administrative principals (KDC) and end-servers to a client, hence breaching the authentication guarantees of Kerberos. It also gives the attacker the keys that the KDC would normally generate to encrypt the service requests of this client, hence defeating confidentiality as well. The discovery of this attack caused the IETF to change the specification of PKINIT and Microsoft to release a security update for some Windows operating systems. We discovered this attack as part of an ongoing formal analysis of the Kerberos protocol suite, and we have formally verified several possible fixes to PKINIT—including the one adopted by the IETF—that prevent our attack as well as other authentication and secrecy properties of Kerberos with PKINIT.

KER Journal 2007 Journal Article

NEXCEL, a deductive spreadsheet

• Iliano Cervesato

Abstract Usability and usefulness have made the spreadsheet one of the most successful computing applications of all times: millions rely on it every day for anything from typing grocery lists to developing multimillion-dollar budgets. One thing spreadsheets are not very good at is manipulating the symbolic data and helping users make decisions based on them. By tapping into recent research in Logic Programming, Databases and Cognitive Psychology, we propose a deductive extension to the spreadsheet paradigm that precisely addresses this issue. The accompanying tool, which we call NEXCEL, is intended as an automated assistant for the daily reasoning and decision-making needs of computer users, in the same way as a spreadsheet application such as Microsoft Excel assists them every day with simple and complex calculations. Users without formal training in Logic or even Computer Science can interactively define logical rules in the same simple way as they define formulas in Excel. NEXCEL immediately evaluates these rules, thereby returning lists of values that satisfy them, again just like with numerical formulas. The deductive component is seamlessly integrated into the traditional spreadsheet so that a user not only still has access to the usual functionalities but is also able to use them as part of the logical inference and, dually, to embed deductive steps in a numerical calculation.

TCS Journal 2006 Journal Article

Formal analysis of Kerberos 5

• Frederick Butler
• Iliano Cervesato
• Aaron D. Jaggard
• Andre Scedrov
• Christopher Walstad

I&C Journal 2002 Journal Article

A Linear Logical Framework

• Iliano Cervesato
• Frank Pfenning

We present the linear type theory λΠ⊸&⊤ as the formal basis for LLF, a conservative extension of the logical framework LF. LLF combines the expressive power of dependent types with linear logic to permit the natural and concise representation of a whole new class of deductive systems, namely those dealing with state. As an example we encode a version of Mini-ML with mutable references including its type system and its operational semantics and describe how to take practical advantage of the representation of its computations.

TIME Conference 2000 Conference Paper

A Calculus of Macro-Events: Progress Report

• Iliano Cervesato
• Angelo Montanari

The need for constraining the temporal relationships among sets of related events arises in several temporal reasoning tasks, including monitoring, plan validation, planning and diagnosis. Process constructors provide an effective way of packaging related events into individual conceptual chunks, called macro-events. In this paper, we present a first attempt at defining a calculus of macro-events that extends Kowalski and Sergot's (1985) event calculus with process constructors to express effects triggered by complex combinations of event occurrences. We apply this language to model the operations of a simple gas heater and present a Prolog implementation.

TCS Journal 2000 Journal Article

Efficient resource management for linear logic proof search

• Iliano Cervesato
• Joshua S. Hodas
• Frank Pfenning

The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and hereditary Harrop formulas (λ Prolog and Elf). Among these, the problem of efficiently managing the linear context when solving a goal is of crucial importance for the use of these systems in non-trivial applications. This paper studies this problem in the case of Lolli [10], though its results have application to other systems including those based on linear type theory. We first give a proof-theoretic presentation of the operational semantics of this language as a resolution calculus. We then present a series of resource management systems designed to eliminate the non-determinism in the distribution of linear formulas that undermines the efficiency of a direct implementation of this system.

TIME Conference 1998 Conference Paper

Event Calculus with Explicit Quantifiers

• Iliano Cervesato
• Massimo Franceschet
• Angelo Montanari

Kowalski and Sergot's (1986) Event Calculus (EC) is a simple temporal formalism that, given a set of event occurrences, derives the maximal validity intervals (MVIs) over which properties initiated or terminated by these events hold. We extend this calculus to give a semantic foundation to our Quantifiers and Connectives Event Calculus (QCEC). In particular, we extend the range of queries accepted by EC, which has so far been limited to Boolean combinations of MVI verification or computation requests, to admit arbitrary quantification over events and properties. We demonstrate the added expressive power by encoding a medical diagnosis problem as a case study. Moreover, we give a /spl lambda/Prolog implementation of this formalism and analyze the computational complexity of the extended calculus.

TIME Conference 1997 Conference Paper

Modal Event Calculi with Preconditions

• Iliano Cervesato
• Massimo Franceschet
• Angelo Montanari

Kowalski and Sergot's (1986) event calculus (EC) is a simple temporal formalism that, given a set of event occurrences, allows the derivation of the maximal validity intervals (MVIs) over which properties initiated or terminated by those events hold. The limited expressive power of EC is notably augmented by permitting events to initiate or terminate a property only if a given set of preconditions hold at their occurrence time. We define a semantic formalization of the event calculus with preconditions. We gain further expressiveness by considering modal variants of this formalism, and show how to adapt our semantic characterization to encompass the additional operators. We discuss the complexity of MVI validation and describe examples showing that modal event calculi with preconditions can be successfully exploited to deal with real-world applications.

ECAI Conference 1996 Conference Paper

A General Modal Framework for the Event Calculus and its Skeptical and Credulous Variants

• Angelo Montanari
• Luca Chittaro
• Iliano Cervesato