Verified security protocols often turn out to be insecurely implemented, with vulnerabilities that were abstracted away in modelling. One way to alleviate this problem is to develop a flexible derivational framework, supporting refinement and composition of reusable protocol components, where actual systems could be feasibly approximated up to a desired level of precision. The general idea is that complex protocols can be formally derived from basic components, using a sequence of refinements and transformations --- just like the proofs of their security properties can be derived from axioms, using proof rules and transformations. The claim is that in practice, many protocols are already derived in such a way, albeit informally. Capturing this practice in a suitable formalism turns out to be an interesting challenge. In the first part of the talk, I shall outline the general protocol derivation framework, and provide a high-level overview of the derivational reconstructions of two key agreement protocols (JFK and MQV), recently proposed in two unrelated standardization efforts. The design patterns, extracted from these two derivations, will then be composed, resulting in a new protocol, with combined security properties. In the second part of the talk, I shall present a more detailed view of the formalism, and show how a failed derivation of one of the agents' goals leads to a derivation of an attack on a previously verified and recently standardized protocol (GDOI). If the time permits, I shall demonstrate a tool prototype. Various parts of the presented work have been done done in collaborations with the colleagues from Stanford (Datta, Derek and Mitchell), NRL (Meadows), and Kestrel (Anlauff).