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:
Filename Description Size
Thumbnail2005000878.pdf1.54 MB
Adobe PDF
Full metadata record
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: