ENDL: A logical framework for verifying secure transaction protocols
- Publication Type:
- Journal Article
- Knowledge and Information Systems, 2005, 7 (1), pp. 84 - 109
- Issue Date:
This paper proposes a new logic for verifying secure transaction protocols. We have named this logic the ENDL (extension of non-monotonic dynamic logic). In this logic, timestamps and signed certificates are used for protecting against replays of old keys or the substitution of bogus keys. The logic is useful for verifying the authentication properties of secure protocols, and especially for protecting data integrity. To evaluate the logic, three practical instances of secure protocols are illustrated. This evaluation demonstrates that the ENDL is effective and promising. © 2004 Springer-Verlag London Ltd.
Please use this identifier to cite or link to this item: