Automated Theorem Proving for Cryptographic Protocols with Automatic Attack Generation

Automated theorem proving is both automatic and can be quite efficient. When using theorem proving approaches for security protocol analysis, however, the problem is often that absence of a proof of security of a protocol may give little hint as to where the security weakness lies, to enable the protocol designer to improve the protocol. For our approach to verify cryptographic protocols using automated theorem provers for first-order logic (such as e-SETHEO or SPASS), we demonstrate a method for automatically generating an attack using the automated theorem prover. The approach is general and independent from the theorem prover used. The formalization in first-order logic is intuitive and allows a mechanical translation from cryptographic protocols written as UML sequence diagrams, which we also sketch. As an example of this approach for practical security analysis of communication protocols, we examine a TLS variant protocol example.     «

Automated theorem proving is both automatic and can be quite efficient. When using theorem proving approaches for security protocol analysis, however, the problem is often that absence of a proof of security of a protocol may give little hint as to where the security weakness lies, to enable the protocol designer to improve the protocol. For our approach to verify cryptographic protocols using automated theorem provers for first-order logic (such as e-SETHEO or SPASS), we demonstrate a method fo...     »