Call by Contract for Cryptographic Protocols

A compositional approach to protocol design and analysis is recognized as advantageous. We wish to perform design decomposition in a way that permits independent design and verification of components, and preserves security and correctness goals when the components are recombined. There are many dif...

Full description

Saved in:
Bibliographic Details
Main Authors: Millen, Jon, Guttman, Joshua, Ramsdell, John, Sheehy, Justin, Sniffen, Brian
Format: Report
Language:English
Subjects:
ABSTRACTS
ALGORITHMS
APPLICATION PROGRAMMING INTERFACE
Computer Hardware
COMPUTER LOGIC
Computer Programming and Software
CRYPTOGRAPHY
Cybernetics
DATALOG RUNTIME ENGINES
DESIGN CRITERIA
ENCRYPTION
INFORMATION SCIENCES
INPUT
PROTOCOL COMPILERS
VERIFICATION
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:A compositional approach to protocol design and analysis is recognized as advantageous. We wish to perform design decomposition in a way that permits independent design and verification of components, and preserves security and correctness goals when the components are recombined. There are many different ways in which composition can be interpreted and implemented. Our version of composition applies to the design of secure protocols. Our objective is to extend verification techniques based on abstract encryption models to protocols that incorporate or implement encapsulated services. One use for such services is to invoke computations that are not included in the vocabulary of operations built into the protocol specification language, such as the special operations of a Trusted Platform Module or some other specialized cryptographic application interface. Another use is to allow flexibility in the choice of means to implement an operation. For a public-key lookup, for example, there may be two alternative services, one that fetches a locally cached certificate, and another that initiates a protocol with a directory server to retrieve one. A service might even establish a shared session key between two parties who have already begun a protocol. With encapsulation of services, we can create and maintain a library of services that could be shared by all protocol processes running on the same system. The service library can be updated with improved implementations without disturbing existing protocols, and new services can be added at any time for use by future protocols. New services can also be used by older protocols if they extend older services, that is, if their functionality is more general or their input requirements are less strict.