A logic for signature based security protocols

This paper presents a logic for signature-based security protocols. We propose an object-oriented model for the execution of security protocols, where protocol roles are modeled as classes and the programs executed by them are modeled as member functions. Unlike most of the formal verification logics, our logic is closer to the cryptography used in security protocols, and can formalize and utilize the different security levels of public-key signature schemes. We demonstrate the power of the logic by verifying the standard signature-based challenge-response protocol using signature algorithms with different security notions.