Catherine Meadows

chapter

Deriving Secrecy in Key Establishment Protocols

Dusko Pavlovic, Catherine Meadows

Lecture Notes in Computer Science > Computer Security – ESORICS 2006 > 384-403

Secrecy and authenticity properties of protocols are mutually dependent: every authentication is based on some secrets, and every secret must be authenticated. This interdependency is a significant source of complexity in reasoning about security. We describe a method to simplify it, by encapsulating the authenticity assumptions needed in the proofs of secrecy. This complements the method for encapsulating...

chapter

What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis

Catherine Meadows

Lecture Notes in Computer Science > Programming Languages and Systems > Invited Talks > 10-21

Much attention has been paid to the design of languages for the specification of cryptographic protocols. However, the ability to specify their desired behavior correctly is also important; indeed many perceived protocol flaws arise out of a misunderstanding of the protocol’s requirements. In this talk we give a brief survey of the history of requirements specification in formal analysis of cryptographic...

chapter

Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis

Catherine Meadows

Lecture Notes in Computer Science > Computer Aided Verification > Invited Talks and Tutorials > 2-2

Protocols using encryption to communicate securely and privately are essential to the protection of our infrastructure. However, since they must be designed to work even under the most hostile conditions, it is not easy to design them correctly. As a matter of fact, it is possible for such protocols to be incorrect even if the cryptographic algorithms they use work perfectly. Thus, over the last few...

chapter

A formal specification of requirements for payment transactions in the SET protocol

Catherine Meadows, Paul Syverson

Lecture Notes in Computer Science > Financial Cryptography > 122-140

Payment transactions in the SET (Secure Electronic Transaction) protocol are described. Requirements for SET are discussed and formally represented in a version of NPATRL (the NRL Protocol Analyzer Temporal Requirements Language). NPATRL is language for expressing generic requirements, heretofore applied to key distribution or key agreement protocols. Transaction vectors and other new constructs added...

chapter

Covert channels—A context-based view

Catherine Meadows, Ira S. Moskowitz

Lecture Notes in Computer Science > Information Hiding > 73-93

In this paper we introduce a taxonomy of covert channels that is based on the context in which the covert channel occurs. This differs from the usual taxonomies, which are based upon the mechanisms employed by the covert channel. Our goal is to use a context-based taxonomy to aid in the understanding of the tradeoffs that are involved in building a secure system.

chapter

Sound Approximations to Diffie-Hellman Using Rewrite Rules

Christopher Lynch, Catherine Meadows

Lecture Notes in Computer Science > Information and Communications Security > 262-277

The commutative property of exponentiation that is necessary to model the Diffie-Hellman key exchange can lead to inefficiency when reasoning about protocols that make use of that cryptographic construct. In this paper we discuss the feasibility of approximating the commutative rule for exponentiation with a pair of rewrite rules, for which in unification-based systems, the complexity of the unification...

chapter

Protocol Analysis Modulo Combination of Theories: A Case Study in Maude-NPA

Ralf Sasse, Santiago Escobar, Catherine Meadows, José Meseguer

Lecture Notes in Computer Science > Security and Trust Management > 163-178

There is a growing interest in formal methods and tools to analyze cryptographic protocols modulo algebraic properties of their underlying cryptographic functions. It is well-known that an intruder who uses algebraic equivalences of such functions can mount attacks that would be impossible if the cryptographic functions did not satisfy such equivalences. In practice, however, protocols use a collection...

chapter

Environmental Requirements for Authentication Protocols

Ran Canetti, Catherine Meadows, Paul Syverson

Lecture Notes in Computer Science > Software Security — Theories and Systems > Authentication Protocols > 339-355

Most work on requirements in the area of authentication protocols has concentrated on identifying requirements for the protocol without much consideration of context. Little work has concentrated on assumptions about the environment, for example, the applications that make use of authenticated keys. We will show in this paper how the interaction between a protocol and its environment can have a major...

chapter

Open Issues in Formal Methods for Cryptographic Protocol Analysis

Catherine Meadows

Lecture Notes in Computer Science > Information Assurance in Computer Networks > Invited Talks > 21-21

The history of the application of formal methods to cryptographic protocol analysis spans nearly twenty years, and recently has been showing signs of new maturity and consolidation. A number of specialized tools have been developed, and others have effectively demonstrated that existing general-purpose tools can also be applied to these problems with good results. However, with this better understanding...

chapter

State Space Reduction in the Maude-NRL Protocol Analyzer

Santiago Escobar, Catherine Meadows, José Meseguer

Lecture Notes in Computer Science > Computer Security - ESORICS 2008 > Session 11: Formal Models and Cryptographic Protocols > 548-562

The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and provides a formal framework for the original NRL Protocol Analyzer, which supported equational reasoning in a more limited way. Maude-NPA supports a wide variety of algebraic properties...

chapter

Reasoning about Probabilistic Security Using Task-PIOAs

Aaron D. Jaggard, Catherine Meadows, Michael Mislove, Roberto Segala

Lecture Notes in Computer Science > Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security > 2-22

Task-structured probabilistic input/output automata (Task-PIOAs) are concurrent probabilistic automata that, among other things, have been used to provide a formal framework for the universal composability paradigms of protocol security. One of their advantages is that that they allow one to distinguish high-level nondeterminism that can affect the outcome of the protocol, from low-level choices,...

chapter

Using a Declarative Language to Build an Experimental Analysis Tool

Catherine Meadows

Lecture Notes in Computer Science > Practical Aspects of Declarative Languages > Invited Talks > 1-2

In this paper we give a brief summary of our experience in using a declarative language, Prolog, to develop an experimental formal analysis tool, the NRL Protocol Analyzer, which was updated and modified over the years to incorporate new theories and techniques. We discuss the benefits of using such an approach, and also some of the downsides.. . .

chapter

Sequential Protocol Composition in Maude-NPA

Santiago Escobar, Catherine Meadows, José Meseguer, Sonia Santiago

Lecture Notes in Computer Science > Computer Security – ESORICS 2010 > Formal Analysis > 303-318

Protocols do not work alone, but together, one protocol relying on another to provide needed services. Many of the problems in cryptographic protocols arise when such composition is done incorrectly or is not well understood. In this paper we discuss an extension to the Maude-NPA syntax and operational semantics to support dynamic sequential composition of protocols, so that protocols can be specified...

chapter

Deriving, Attacking and Defending the GDOI Protocol

Catherine Meadows, Dusko Pavlovic

Lecture Notes in Computer Science > Computer Security – ESORICS 2004 > 53-72

As a part of a continued effort towards a logical framework for incremental reasoning about security, we attempted a derivational reconstruction of GDOI, the protocol proposed in IETF RFC 3547 for authenticated key agreement in group communication over IPsec. The difficulties encountered in deriving one of its authentication properties led us to derive an attack that had not surfaced in the previous...

chapter

Security of Ramp Schemes

G. R. Blakley, Catherine Meadows

Lecture Notes in Computer Science > Advances in Cryptology > Randomness and Its Concomitants > 242-268

A k out of n p/s/r process [AS81] is a very efficient way to convey information (k words suffice to reclaim k words). But it provides virtually no cryptographic security for the information it deals with.

chapter

Formal requirements for key distribution protocols

Paul Syverson, Catherine Meadows

Lecture Notes in Computer Science > Advances in Cryptology — EUROCRYPT'94 > 320-331

We discuss generic formal requirements for reasoning about two party key distribution protocols, using a language developed for specifying security requirements for security protocols. Typically earlier work has considered formal analysis of already developed protocols. Our goal is to present sets of formal requirements for various contexts which can be applied at the design stage as well as to existing...

book

Computer Security — ESORICS 98

Jean-Jacques Quisquater, Yves Deswarte, Catherine Meadows, Dieter Gollmann

Lecture Notes in Computer Science

This book constitutes the refereed proceedings of the 5th European Symposium on Research in Computer Security, ESORICS 98, held in Louvain-la-Neuve, Belgium, in September 1998.The 24 revised full papers presented were carefully reviewed and selected from a total of 57 submissions. The papers provide current results from research and development in design and specification of security policies, access...

book

Security and Privacy in Ad-hoc and Sensor Networks

Frank Stajano, Catherine Meadows, Srdjan Capkun, Tyler Moore

Lecture Notes in Computer Science

You hold in your hands the proceedings of ESAS 2007, the Fourth European Workshop on Security and Privacy in Ad hoc and Sensor Networks. The wo- nd rd shop took place in Cambridge, UK, on the 2 and 3 of July 2007. The workshop was European in name and location but it was de?nitely transatlantic in scope. We had a program chair from Europe and one from the USA, and membership of our program committee...

article

State space reduction in the Maude-NRL Protocol Analyzer

Santiago Escobar, Catherine Meadows, José Meseguer, Sonia Santiago

Information and Computation > 2014 > 238 > Complete > 157-186

The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and provides a formal framework for the original NRL Protocol Analyzer, which supported equational reasoning in a more limited way. Maude-NPA supports a wide variety of algebraic properties...

article

Dedication

Stephen Brookes, Achim Jung, Catherine Meadows, Michael Mislove, more

Electronic Notes in Theoretical Computer Science > 2012 > 286 > Complete > 3

INFONA - science communication portal

Search results for: Catherine Meadows

Deriving Secrecy in Key Establishment Protocols

What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis

Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis

A formal specification of requirements for payment transactions in the SET protocol

Covert channels—A context-based view

Sound Approximations to Diffie-Hellman Using Rewrite Rules

Protocol Analysis Modulo Combination of Theories: A Case Study in Maude-NPA

Environmental Requirements for Authentication Protocols

Open Issues in Formal Methods for Cryptographic Protocol Analysis

State Space Reduction in the Maude-NRL Protocol Analyzer

Reasoning about Probabilistic Security Using Task-PIOAs

Using a Declarative Language to Build an Experimental Analysis Tool

Sequential Protocol Composition in Maude-NPA

Deriving, Attacking and Defending the GDOI Protocol

Security of Ramp Schemes

Formal requirements for key distribution protocols

Computer Security — ESORICS 98

Security and Privacy in Ad-hoc and Sensor Networks

State space reduction in the Maude-NRL Protocol Analyzer

Dedication

Filter options

Publication date

Content availability

Publication type

Keywords

Data set

Journal

INFONA - science communication portal

Search results for: Catherine Meadows

Add recipient

Sending message cancelled

Are you sure you want to cancel sending this message?

Send message

Filter options

Publication date

Date range setting

Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.

Content availability

Publication type

Keywords

Data set

Journal

Reporting an error / abuse

Sending the report failed

Accessibility options