Formal analysis of cryptographic protocols by reasoning based on deontic relevant logic: A case study in Needham-Schroeder Shared-Key protocol

Formal analysis of cryptographic protocols is necessary to assure security before using it. In traditional approaches, analysts have to specify security goals or necessary conditions of the analysis firstly. However, it is difficult to specify all security goals or necessary conditions. A reasoning approach without the problem was proposed, but its concrete method is not established. In this paper, as the first step to elaborate the reasoning approach of cryptographic protocols, we analyzed Needham-Schroeder Shared-Key protocol by reasoning based on deontic relevant logic. By the case study, we show that the reasoning approach can find vulnerability of the cryptographic protocol as well as traditional approach, and can expect to find new vulnerability that has not been recognized. Then, we discuss about the concrete method for formal analysis of cryptographic protocols by the reasoning approach.