Derivation of the JFK protocol
Duško Pavlović · 2002
We introduce a basic framework for deriving securityprotocols from simple components, like proofs are derivedfrom axioms. As an initial case study, we derive the re-cently proposed key agreement protocol JFK (Just Fast Key-ing), starting from the basic Diffie-Hellman exchange, andthe generic challenge-response scheme, and refining themby the other required security features, formalized in ourderivation system by suitable refinement and transforma-tion rules.