Secure protocol composition

30 October 2003

proceedings article
Published by Association for Computing Machinery (ACM)

p. 11-23
https://doi.org/10.1145/1035429.1035431

Abstract

Modular composition of security mechanisms is complicated by the way that one mechanism may reveal information that interferes with the security of another. We develop methods for modular reasoning about security protocols, using before-after assertions and protocol invariants. The before-after assertions allow us to prove properties of a sequential composition of protocol steps and therefore enable construction of complex protocols from smaller sub-protocols. Invariants provide a mechanism for ensuring that sub-protocols which are individually secure do not interact insecurely when they are composed to construct a bigger protocol. The application of the method is demonstrated by giving modular formal proofs involving two standard protocols.

Keywords

This publication has 16 references indexed in Scilit:

A Calculus for Cryptographic Protocols: The Spi Calculus
Information and Computation, 1999
The NRL Protocol Analyzer: An Overview
The Journal of Logic Programming, 1996
A general theory of composition for a class of "possibilistic" properties
IEEE Transactions on Software Engineering, 1996
A formal language for cryptographic protocol requirements
Designs, Codes and Cryptography, 1996
A model for secure protocols and their compositions
IEEE Transactions on Software Engineering, 1996
Authentication and authenticated key exchanges
Designs, Codes and Cryptography, 1992
The chemical abstract machine
Theoretical Computer Science, 1992
A hookup theorem for multilevel security
IEEE Transactions on Software Engineering, 1990
Using encryption for authentication in large networks of computers
Communications of the ACM, 1978
New directions in cryptography
IEEE Transactions on Information Theory, 1976