We adapt the Strand Spaces model to reason abstractly about layered security protocols, where an Application Layer protocol is layered on top of a secure transport protocol. The model abstracts away from the implementation of the secure transport protocol and just captures the properties that it provides to the Application Layer. We illustrate the usefulness of the model by using it to verify a small single sign-on protocol.
展开▼
