On the Verificaiton of Non-repudiation Protocols

摘要

The design of cryptographic protocols is a challenging task as subtle protocol flaws and weaknesses can remain unidentified even after scrupulous checking. In order to provide assurance that a protocol is verifiable secure and trustworthy, it is necessary to perform a formal verification on its design specification. Non-repudiation plays an increasingly significant role in electronic commerce, protecting the transacting parties against any false denial that a particular event or action has taken place. The application of formal verification techniques on non-repudiation protocols is not straightforward, as these protocols need to satisfy' non-repudiation requirements while achieving security goals. In this paper, a logic-based method is proposed to formally analyze and verify nonrepudiation protocols. The proposed method utilizes the CS logic taking its advantage of time-indexed protocol verification. Extensions to CS logic are introduced to meet the requirements for analyzing non-repudiation protocols. As a case study, a nonrepudiation protocol is formally verified using the extended logic.