On-the-Fly Model Checking of Fair Non-repudiation Protocols

A fair non-repudiation protocol should guarantee, (1) when a sender sends a message to a receiver, neither the sender nor the receiver can deny having participated in this communication; (2) no principals can obtain evidence while the other principals cannot do so. This paper extends the model in our previous work [12], and gives a sound and complete on-the-fly model checking method for fair non-repudiation protocols under the assumption of a bounded number of sessions. We also implement the method using Maude. Our experiments automatically detect flaws of several fair non-repudiation protocols.

• Type: Conference
• Year: 2007
• Where: ATVA
• Authors: Guoqiang Li, Mizuhito Ogawa
• Keywords: ATVA 2007, Fair Non-repudiation Protocols, Hardware, Model Checking Method, Sender