An Extension of Formal Analysis Method with Reasoning for Anonymity

摘要

Formal analysis method with reasoning has been proposed as an alternative formal analysis method for cryptographic protocols. In the method, at first, analysts formalize the participant's and attacker's behaviors in order to carry out forward reasoning, then analysts check whether the logic formulas that represents security flaws of the target protocol exist or not in deduced logical formulas. However, the current method can deal with security flaws related to authentication, confidentiality, fairness, and non-repudiation, but not anonymity. This paper proposes an extension of formal analysis method with reasoning for dealing with security flaws related to anonymity. The paper also gives a case study with the proposed method in the Bolignano protocol. The result shows that the extension method is useful to detect security flaws related to anonymity.