Formal Analysis of Timeliness in Non-Repudiation Protocols

While SVO logic has been widely used in the analysis of non-repudiation protocols for its simplicity, its lack of the ability in time description makes it helpless in the analysis of timeliness, which is one of the most important properties of non-repudiation protocols. SVO logic is extended by adding a simple time expression and analysis method into it. Then a widely discussed fair non-repudiation proposed by Zhou and Gollmann in 1996 and one of its improvements are analyzed with the newly extended logic. The result shows that Zhou-Gollmann's fair non-repudiation protocol does not provide timeliness while its improvement does. Therefore, the new logic is able to analyze timeliness of non-repudiation protocols. In addition, the new logic can be used to analyze other time-related properties of cryptographic protocols.