On the automated implementation of modal logics used to verify security protocols

: Formal verification provides a rigid and thorough means of evaluating the correctness of cryptographic protocols so that even subtle defects can be identified. As the application of formal techniques is highly involved, software has been developed in order to facilitate protocol verification. Protocol weaknesses or flaws can thus be identified and corrected during the design process. In this paper the verification process is illustrated by analysing the ASK protocol using the tool AAPA2. The virtues and limitations of the tool are discussed. Overall, the analysis shows that the use of automated tools in verifying security protocols offers significant advantages to the protocol designer.

• Type: Conference
• Year: 2003
• Where: ISICT
• Authors: Tom Coffey, Reiner Dojen, Tomas Flanagan
• Keywords: Formal Verification, Information Technology, ISICT 2003, Protocol Verification, Protocol Weaknesses