Abstraction and refinement in protocol derivation
Anupam Datta, Ante Đerek, John C. Mitchell, Duško Pavlović · 2004
Many network protocols with security objectives aredesigned using a smaller set of common protocol concepts, such as challenge-response, Diffie-Hellman-likekey agreement, and "cookies " to reduce potential denial of service attacks. In previous work [6, 7, 8], weproposed a protocol derivation framework, based on the use of composition, refinement, and transforma-tion, and a formal logic for stating and proving properties of protocols. In this framework, a protocol de-signer may choose two initial protocol components, refine each of them, compose the results to get a candi-date protocol, then apply one or more transformations