Call by Contract for Cryptographic Protocols
MITRE CORP BEDFORD MA COMPUTER AND DISPLAY DEVELOPMENT DEPT
Pagination or Media Count:
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.
- Computer Programming and Software
- Computer Hardware