|Citation||Electronic Notes in Theorectical Computer Science 83 (2004)
John C. Mitchell
This paper continues the program initiated in , towards a derivation
system for security protocols. The general idea is that complex
protocols can be formally derived, starting from basic security
components, using a sequence of refinements and transformations, just
like logical proofs are derived starting from axioms, using proof rules
and transformations. The claim is that in practice, many protocols are
already derived in such a way, but informally. Capturing this practice
in a suitable formalism turns out to be a considerable task.
The present paper proposes rules for composing security protocols from given security components. In general, security protocols are, of course, not compositional: information revealed by one may interfere with the security of the other. However, annotating protocol steps by pre-and post-conditions, allows secure sequential composition. Establishing that protocols components satisfy each other's invariants allows more general forms of composition, ensuring that the individually secure sub-protocols will not interact insecurely in the composite protocol. The applicability of the method is demonstrated on modular derivations of two standard protocols, together with their simple security properties.
Back to publications
Back to previous page