Action system analysis of an authentication protocol (extended abstract)
We present an abstract specification of a simple authenticated communications service and then refine it in such a way that the communication and authentication of messages is achieved using the fixed version of the Needham-Schroeder authentication protocol. Three stages of development are presented: 1) The abstract system, which is a simple description of a service that allows agents to exchange authenticated messages. 2) The first refinement of the abstract system, which implements the exchange of each individual message using the protocol. 3) The second refinement, which introduces an explicit model of how a spy could fake and replay messages to attempt to violate the authentication. For the entire collection see [Zbl 0877.00014].
- On the use of data refinement in the development of secure communications systems
- On the Clark-Jacob version of SPLICE/AS
- scientific article; zbMATH DE number 1543079 (Why is no real title available?)
- Automated type-based analysis of injective agreement in the presence of compromised principals
- Foundations of Security Analysis and Design III
- Information Security and Cryptology
- On the security of SPLICE/AS -- The authentication system in WIDE Internet
This page was built for publication: Action system analysis of an authentication protocol (extended abstract)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4370271)
