ENDL: A Logical Framework for Verifying Secure Transaction Protocols

摘要

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.