Martin Abadi

Deciding knowledge in security protocols under (many more) equational theories (2005)

In the analysis of security protocols, the knowledge of attackers is often described in terms of message deducibility and indistinguishability relations. In this paper, we pursue the study of these...

Libraries Virtual Machine (2005)

In the analysis of security protocols, the knowledge of attackers is often described in terms of message deducibility and indistinguishability relations. In this paper, we pursue the study of these...

Gilles Barthe, Martin Abadi, Amy Felty, Rustan Leino, Inria Lmu Münich, Ru Nijmegen, ...

16 members

Formal Security Analysis of Basic Network-Attached Storage (2005)

Avik Chaudhuri, Martin Abadi

We study formal security properties of network-attached storage (NAS) in an applied pi calculus. We model NAS as an implementation of a specification based on traditional centralized storage. We show...

Formal Security Analysis of Basic Network-Attached Storage (2005)

Avik Chaudhuri, Martin Abadi

We study formal security properties of network-attached storage (NAS) in an applied pi calculus. We model NAS as an implementation of a specification based on traditional centralized storage. We show...

Deciding knowledge in security protocols under equational theories (2004)

Deciding knowledge in security protocols under equational theories (2004)

The analysis of security protocols requires precise formulations of the knowledge of protocol participants and attackers. In formal approaches, this knowledge is often treated in terms of message...

A Per Model of Polymorphism and Recursive Types (2003)

The analysis of security protocols requires precise formulations of the knowledge of protocol participants and attackers. In formal approaches, this knowledge is often treated in terms of message...

A Logical View of Composition (2003)

A model of Reynolds’ polymorphic lambda calculus is provided, which also allows the recursive definition of elements and types. The technique is to use a good class of partial equivalence relations...

A Logic for Parametric Polymorphism (2003)

We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification...

Plotkin, Gordon, Abadi, Martin

In this paper we introduce a logic for parametric polymorphism. Just as LCF is a logic for the simply-typed -calculus with recursion and arithmetic, our logic is a logic for System F. The logic...

Subtyping and Parametricity (2003)

Plotkin, Gordon, Abadi, Martin, Cardelli, Luca

In this paper we study the interaction of subtyping and parametricity. We describe a logic for a programming language with parametric polymorphism and subtyping. The logic supports the formal...

A Per Model of Polymorphism and Recursive Types (2003)

A Logical View of Composition (2003)

A model of Reynolds’ polymorphic lambda cal- culus is provided, which also allows the recursive definition of elements and types. The technique is to use a good class of partial equivalence re-...

A Logic for Parametric Polymorphism (2003)

We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification...

Plotkin, Gordon, Abadi, Martin

In this paper we introduce a logic for parametric polymorphism. Just as LCF is a logic for the simply-typed -calculus with recursion and arithmetic, our logic is a logic for System F. The logic...

Subtyping and Parametricity (2003)

Plotkin, Gordon, Abadi, Martin, Cardelli, Luca

In this paper we study the interaction of subtyping and parametricity. We describe a logic for a program- ming language with parametric polymorphism and sub- typing. The logic supports the formal...

FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES (2003)

Abadi, Martin, Pierce, Benjamin, Plotkin, Gordon

We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit...

FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES (2003)

Abadi, Martin, Pierce, Benjamin, Plotkin, Gordon

We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit...

Exponential distribution for the occurrence of rare patterns in Gibbsian random fields (2003)

Abadi, Martin, Chazottes, J-R, Redig, FHJ

Moderately Hard, Memory-bound Functions (2003)

Martin Abadi, Mike Burrows, Mark Manasse, Ted Wobber

A resource may be abused if its users incur little or no cost. For example, e-mail abuse is rampant because sending an e-mail has negligible cost for the sender. It has been suggested that such abuse...

Formal eavesdropping and its computational interpretation (2001)

Abadi, Martin, Jurjens, Jan

World Wide Web Conference. (2000)

Martin Abadi, Luca Cardelli, A Theory, Primitive Objects Untyped, David Atkins, Thomas Ball, ...

domain-specific language for form-based services. In: IEEE Transactions

A calculus for cryptographic protocols: The spi calculus (1999)

Martin Abadi, Andrew D. Gordon

We introduce the spi calculus, an extension of the pi calculus designed for the description and analysis of cryptographic protocols. We show how to use the spi calculus, particularly for studying...

A Type System for Java Bytecode Subroutines (1998)

Raymie Stata, Martin Abadi, Raymie Stata, Martn Abadi, Martn Abadi

ing with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permission from Publications...

A Logic of Object-Oriented Programs (1998)

Martin Abadi, Martn Abadi, Martn Abadi, K. Rustan, K. Rustan, ...

We develop a logic for reasoning about object-oriented programs. The logic is for a language with an imperative semantics and aliasing, and accounts for self-reference in objects. It is much like a...

Modal Theorem Proving, (1997)

Abadi, Martin, Manna, Zohar

We describe resolution proof systems for several modal logics. First we present the propositional versions of the systems and prove their completeness. The first-order resolution rule for classical...

References (1997)

Michael Burrows, Martin Abadi, Roger Needham, A Acm

Explicit Communication Revisited: Two New Attacks on Authentication Protocols (1997)

Martin Abadi

SSH and AKA are recent, practical protocols for secure connections over an otherwise unprotected network. This paper shows that, despite the use of public-key cryptography, SSH and AKA do not provide...

A calculus for cryptographic protocols: The spi calculus (1997)

Martin Abadi, Andrew D. Gordon

We introduce the spi calculus, an extension of the pi calculus designed for the description and analysis of cryptographic protocols. We show how to use the spi calculus, particularly for studying...

A Logic of Object-Oriented Programs (1997)

Martin Abadi, K. Rustan, M. Leino

We develop a logic for reasoning about object-oriented programs.

A TLA solution to the RPC-Memory specification problem (1996)

Martin Abadi, Leslie Lamport, Stephan Merz

We present a complete solution to the Broy-Lamport specification problem. Our specifications are written in TLA, a formal language based on TLA. We give the high levels of structured proofs and

A TLA Solution to the RPC-Memory Specification Problem (1996)

Martin Abadi, Leslie Lamport, Stephan Merz

. We present a complete solution to the Broy-Lamport specification problem. Our specifications are written in TLA + , a formal language based on TLA. We give the high levels of structured proofs and...

Analysis and Caching of Dependencies (1996)

Martin Abadi, Butler Lampson, Jean-Jacques Lévy, Inria Rocquencourt

We address the problem of dependency analysis and caching in the context of the -calculus. The dependencies of a - term are (roughly) the parts of the -term that contribute to the result of...

On TLA as a Logic (1996)

Martin Abadi, Stephan Merz

this paper we describe TLA from a logical perspective; our description of TLA has three aspects: 1. As a logic, TLA has a precise syntax and semantics. We define these in the next section. Our intent...

On TLA as a Logic (1996)

Martin Abadi, Stephan Merz

this paper we describe TLA from a logical perspective# our description of TLA has three aspects: 1' As a logic, TLA has a precise syntax and semantics. We define these in the next section. Our...

A TLA Solution to the RPC-Memory Specification Problem (1996)

Martin Abadi, Leslie Lamport, Stephan Merz

We present a complete solution to the Broy-Lamport specification problem. Our specifications are written in TLA , a formal language based on TLA. Wegive the high levels of structured proofs and...

A Model for Formal Parametric Polymorphism: a Per Interpretation for System R (1995)

Uperieure S Ormale, N Ecole, Pierre-Louis Curien, Martin Abadi, Martin Abadi, Roberto Bellucci, ...

System R is an extension of system F that formalizes Reynolds' notion of relational parametricity. In this paper we describe a semantics for system R. As a first step, we give a careful and...

A Model for Formal Parametric Polymorphism: A PER Interpretation for System R (1995)

Roberto Bellucci, Martin Abadi, Pierre-Louis Curien

System R is an extension of system F that formalizes Reynolds' notion of relational parametricity. In system R, considerably more lambda-terms can be proved equal than in system F: for example,...

A Theory of Primitive Objects (1994)

Martin Abadi, Martn Abadi, Luca Cardelli

We investigate calculi that support method override in presence of object subsumption. Subsumption is the ability to emulate an object by means of another object that has more refined methods....

Object Types with SELF (1994)

Martin Abadi, Luca Cardelli

Extensible Syntax with Lexical Scoping (1994)

Luca Cardelli, Florian Matthes, Martin Abadi, Robert W. Taylor

A frequent dilemma in programming language design is the choice between a language with a rich set of notations and a small, simple core language. We address this dilemma by proposing extensible...

Authentication in the Taos Operating System (1994)

Edward Wobber, Martin Abadi, Mike Burrows

This version was reconstructed from the printed version by OCR and hand

Authentication in the Taos Operating System (1994)

Edward Wobber, Martin Abadi, Mike Burrows

This version was reconstructed from the printed version by OCR and hand

A Calculus for Access Control in Distributed Systems (1993)

Abadi, Martin, Burrows, Michael, Lampson, Butler, Plotkin, Gordon

We study some of the concepts, protocols, and algorithms for access control in distributed systems, from a logical perspective. We account for how a principal may come to believe that another...

A Calculus for Access Control in Distributed Systems (1993)

Abadi, Martin, Burrows, Michael, Lampson, Butler, Plotkin, Gordon

We study some of the concepts, protocols, and algorithms for access control in distributed systems, from a logical perspective. We account for how a principal may come to believe that another...

Formal Parametric Polymorphism (1993)

Martin Abadi, Martn Abadi, Luca Cardelli, Pierre-Louis Curien

A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds's work, the study of parametricity is typically semantic. In...

Formal Parametric Polymorphism (1993)

Martin Abadi, Martn Abadi, Luca Cardelli, Pierre-Louis Curien

A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds's work, the study of parametricity is typically semantic. In...

An Old-Fashioned Recipe for Real Time (1993)

Martin Abadi, Leslie Lamport

Traditional methods for specifying and reasoning about concurrent systems work for realtime systems. Using TLA (the temporal logic of actions), we illustrate how they work with the examples of a...

Subtyping and Parametricity (1993)

Gordon Plotkin, Martin Abadi, Luca Cardelli

and parametricity. We describe a logic for a programming language with parametric polymorphism and subtyping. The logic supports the formal definition and use of relational parametricity. We give two...

Authentication in distributed systems: Theory and practice (1992)

Butler Lampson, Martin Abadi, Michael Burrows, Edward Wobber

Digital Equipment Corporation We describe a theory of authentication and a system that implements it. Our theory is based on the notion of principal and a ‘speaks for ’ relation between...

A Logical View of Composition (1992)

Martin Abadi, Gordon D. Plotkin

We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification...

Authentication in Distributed Systems: Theory and Practice (1992)

Butler Lampson, Martin Abadi, Martn Abadi, Michael Burrows, Edward Wobber

this paper appeared in the Proceedings of the Thirteenth ACM Sympos - ium on Operating Systems Principles.

A Logical View of Composition (1992)

Martin Abadi, Gordon D. Plotkin

We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification...

Preserving Liveness: Comments on "Safety and Liveness from a Methodological Point of View" (1991)

Martin Abadi, Bowen Alpern, Krzysztof R. Apt, Nissim Francez, Shmuel Katz, Leslie Lamport, ...

17> I.B.M., T. J. Watson Research Center z C.W.I. x Department of Computer Science, The Technion -- Computer Science Department, Cornell University (Supported by Office of Naval Research contract...

A Semantics for a Logic of Authentication (1991)

Martin Abadi, Mark Tuttle

Burrows, Abadi, and Needham have proposed a logic for the analysis of authentication protocols. It is a logic of belief, with special constructs for expressing some of the central concepts used in...

Authentication protocols are the basis of security in many distributed systems, and it is therefore essential to ensure that these protocols function correctly. Unfortunately, their design has been...

Authentication protocols are the basis of security in many distributed systems, and it is therefore essential to ensure that these protocols function correctly. Unfortunately, their design has been...

Authentication protocols are the basis of security in many distributed systems, and it is therefore essential to ensure that these protocols function correctly. Unfortunately, their design has been...

The Scope of a Logic of Authentication (1990)

Questions of belief are essential in analyzing protocols for the authentication of principals in distributed computing systems. In this paper we motivate, set out, and exemplify a logic specifically...

this report has helped us in analyzing certain aspects of authentication protocols. Our logic consists of a simple set of inference rules, in a notation designed specifically for the study of...

Authentication: A practical study in belief and action (1988)

Authentication protocols are the basis of security in many distributed systems, and it is therefore essential to ensure that these protocols function correctly. Unfortunately, their design has been...