Andre Scedrov

I&C Journal 2022 Journal Article

Language models for some extensions of the Lambek calculus

• Max Kanovich
• Stepan Kuznetsov
• Andre Scedrov

We investigate language interpretations of two extensions of the Lambek calculus: with additive conjunction and disjunction and with additive conjunction and the unit constant. For extensions with additive connectives, we show that conjunction and disjunction behave differently. Adding both of them leads to incompleteness due to the distributivity law. We show that with conjunction only no issues with distributivity arise. In contrast, there exists a corollary of the distributivity law in the language with disjunction only which is not derivable in the non-distributive system. Moreover, this difference keeps valid for systems with permutation and/or weakening structural rules, that is, intuitionistic linear and affine logics and affine multiplicative-additive Lambek calculus. For the extension of the Lambek calculus with the unit constant, we present a calculus which reflects natural algebraic properties of the empty word. We do not claim completeness for this calculus, but we prove undecidability for the whole range of systems extending this minimal calculus and sound w. r. t. language models. As a corollary, we show that in the language with the unit there exists a sequent that is true if all variables are interpreted by regular language, but not true in language models in general.

I&C Journal 2014 Journal Article

Bounded memory Dolev–Yao adversaries in collaborative systems

• Max Kanovich
• Tajana Ban Kirigin
• Vivek Nigam
• Andre Scedrov

In a collaborative system, the agents collaborate to achieve a common goal, but they are not willing to share some sensitive private information. The question is how much damage can be done by a malicious participant sitting inside the system. We assume that all the participants (including internal adversaries) have bounded memory – at any moment, they can store only a fixed number of messages of a fixed size. The Dolev–Yao adversaries can compose, decompose, eavesdrop, and intercept messages, and create fresh values (nonces), but within their bounded memory. We prove that the secrecy problem is PSPACE-complete in the bounded memory model where all actions are balanced and a potentially infinite number of the nonce updates is allowed. We also show that the well-known security protocol anomalies (starting from the Lowe attack to the Needham–Schroeder protocol) can be rephrased within the bounded memory paradigm with the explicit memory bounds.

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.

TCS Journal 2006 Journal Article

A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols

• John C. Mitchell
• Ajith Ramanathan
• Andre Scedrov
• Vanessa Teague

We prove properties of a process calculus that is designed for analysing security protocols. Our long-term goal is to develop a form of protocol analysis, consistent with standard cryptographic assumptions, that provides a language for expressing probabilistic polynomial-time protocol steps, a specification method based on a compositional form of equivalence, and a logical basis for reasoning about equivalence. The process calculus is a variant of CCS, with bounded replication and probabilistic polynomial-time expressions allowed in messages and boolean tests. To avoid inconsistency between security and nondeterminism, messages are scheduled probabilistically instead of nondeterministically. We prove that evaluation of any process expression halts in probabilistic polynomial time and define a form of asymptotic protocol equivalence that allows security properties to be expressed using observational equivalence, a standard relation from programming language theory that involves quantifying over all possible environments that might interact with the protocol. We develop a form of probabilistic bisimulation and use it to establish the soundness of an equational proof system based on observational equivalences. The proof system is illustrated by a formation derivation of the assertion, well-known in cryptography, that El Gamal encryption's semantic security is equivalent to the (computational) Decision Diffie–Hellman assumption. This example demonstrates the power of probabilistic bisimulation and equational reasoning for protocol security.

TCS Journal 2006 Journal Article

Formal analysis of Kerberos 5

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

TCS Journal 2003 Journal Article

Phase semantics for light linear logic

• Max I Kanovich
• Mitsuhiro Okada
• Andre Scedrov

Light linear logic (Girard, Inform. Comput. 14 (1998) 175–204) is a refinement of the propositions-as-types paradigm to polynomial-time computation. A semantic setting for the underlying logical system is introduced here in terms of fibred phase spaces. Strong completeness is established, with a purely semantic proof of cut elimination as a consequence. A number of mathematical examples of fibred phase spaces are presented that illustrate subtleties of light linear logic.

TCS Journal 2003 Journal Article

Preface

• Jean-Yves Girard
• Mitsuhiro Okada
• Andre Scedrov

TCS Journal 1999 Journal Article

Optimization complexity of linear logic proof games

• Patrick D. Lincoln
• John C. Mitchell
• Andre Scedrov

A class of linear logic proof games is developed, each with a numeric score that depends on the number of preferred axioms used in a complete or partial proof tree. The complexity of these games is analyzed for the NP-complete multiplicative fragment (MLL) extended with additive constants and the PSPACE-complete multiplicative, additive fragment (MALL) of propositional linear logic. In each case, it is shown that it is as hard to compute an approximation of the best possible score as it is to determine the optimal strategy. Furthermore, it is shown that no efficient heuristics exist unless there is an unexpected collapse in the complexity hierarchy.

FOCS Conference 1998 Conference Paper

A Linguistic Characterization of Bounded Oracle Computation and Probabilistic Polynomial Time

• John C. Mitchell
• Mark Mitchell
• Andre Scedrov

We present a higher-order functional notation for polynomial-time computation with an arbitrary 0, 1-valued oracle. This formulation provides a linguistic characterization for classes such as NP and BPP, as well as a notation for probabilistic polynomial-time functions. The language is derived from Hofmann's adaptation of Bellantoni-Cook safe recursion, extended to oracle computation via work derived from that of Kapron and Cook. Like Hofmann's language, ours is an applied typed lambda calculus with complexity bounds enforced by a type system. The type system uses a modal operator to distinguish between two sorts of numerical expressions. Recursion can take place on only one of these sorts. The proof that the language captures precisely oracle polynomial time is model-theoretic, using adaptations of various techniques from category theory.

I&C Journal 1996 Journal Article

The Undecidability of Second Order Multiplicative Linear Logic

• Yves Lafont
• Andre Scedrov

The multiplicative fragment of second order propositional linear logic is shown to be undecidable.

TCS Journal 1995 Journal Article

Moez Alimohamed, 1967–1994

• Andre Scedrov
• Dennis DeTurk
• Wolfgang Ziller

CSL Conference 1993 Conference Paper

Notes on Sconing and Relators

• John C. Mitchell
• Andre Scedrov

Abstract This paper describes a semantics of typed lambda calculi based on relations. The main mathematical tool is a category-theoretic method of sconing, also called glueing or Freyd covers. Its correspondence to logical relations is also examined.

TCS Journal 1992 Journal Article

Bounded linear logic: a modular approach to polynomial-time computability

• Jean-Yves Girard
• Andre Scedrov
• Philip J. Scott

Usual typed lambda-calculi yield input/output specifications; in this paper the authors show how to extend this paradigm to complexity specifications. This is achieved by means of a restricted version of linear logic in which the use of exponential connectives is bounded in advance. This bounded linear logic naturally involves polynomials in its syntax and dynamics. It is then proved that any functional term of appropriate type actually encodes a polynomial-time algorithm and that conversely any polynomial-time function can be obtained in this way.

I&C Journal 1991 Journal Article

Inheritance as implicit coercion

• Val Breazu-Tannen
• Thierry Coquand
• Carl A. Gunter
• Andre Scedrov

We present a method for providing semantic interpretations for languages with a type system featuring inheritance polymorphism. Our approach is illustrated on an extension of the language Fun of Cardelli and Wegner, which we interpret via a translation into an extended polymorphic lambda calculus. Our goal is to interpret inheritances in Fun via coercion functions which are definable in the target of the translation. Existing techniques in the theory of semantic domains can be then used to interpret the extended polymorphic lambda calculus, thus providing many models for the original language. This technique makes it possible to model a rich type discipline which includes parametric polymorphism and recursive types as well as inheritance. A central difficulty in providing interpretations for explicit type disciplines featuring inheritance in the sense discussed in this paper arises from the fact that programs can type-check in more than one way. Since interpretations follow the type-checking derivations, coherence theorems are required: that is, one must prove that the meaning of a program does not depend on the way it was type-checked. Proofs of such theorems for our proposed interpretation are the basic technical results of this paper. Interestingly, proving coherence in the presence of recursive types, variants, and abstract types forced us to reexamine fundamental equational properties that arise in proof theory (in the form of commutative reductions) and domain theory (in the form of strict vs. non-strict functions).

FOCS Conference 1990 Conference Paper

Decision Problems for Propositional Linear Logic

• Patrick Lincoln
• John C. Mitchell
• Andre Scedrov
• Natarajan Shankar

It is shown that, unlike most other propositional (quantifier-free) logics, full propositional linear logic is undecidable. Further, it is provided that without the model storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. Also established are membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for certain fragments of noncommutative propositional linear logic. >