| Full text | Click to download. |
| Citation | In 4th Annual Conference on High Confidence Software and
Systems, April 2004
|
| Authors | Anupam Datta
Ante Derek John C. Mitchell Dusko Pavlovic |
This overview describes a partially formalized method for systematically deriving protocols and proving them correct. The derivation framework includes some basic protcol components, such as challenge-response, and three ways of combining or extending protocols: composition, refinement, and transformation. Composition combines separate protocols, refinements change the content or structure of individual messages, and transformations alter the message structure of a protocol. We associate logical proofs with protocls derivations using a security protocol logic that includes temporal, before-after, and invariance assertions. We currently have formal proof rules for reasoning about protocol composition and some forms of protocol refinement. The derivation method and formal proof system have been used for several families of protocols, including the IKE/JFK family, GDOI, and Kerberos. In future work, we plan to extend the derivation system to cover a wider class of protocols, further simplify the protocol logic, and develop formal proof methods associated with additional refinements and protocol transformations. Tool implementation efforts are also underway.