| Citation | Electronic Notes in Theorectical Computer Science 83 (2004)
|
| Authors | Anupam Datta
Ante Derek John C. Mitchell |
This paper continues the program initiated in [5], 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.