An Application of Justification Logic to Protocol Verification

Recently, Tsukada et al. propose to use multi-agent epistemic logic for a taxonomy of information-hiding/disclosure properties, in particular properties used in authentication protocols. We follow their proposal and introduce a new multi-agent justification logic for protocol analysis and verification. We show our logic at work analyzing a non-repudiation protocol due to Zhou and Gollmann. Based on this example, we then discuss the expressive power of the logic as well as possible further extensions.