Fairness of non-repudiation is naturally expressed as a liveness specification, as in [Sch98]; to formalize this idea, we apply the process algebra CSP to analyze the well-known Zhou-Gollmann protocol. We here model and verify a variant of the ZG protocol that includes a deadline (timestamp) for completion of the protocol, after which an agent can no longer initiate the recovery protocol with the TTP to get hold of the non-repudiation evidence. The verification itself is performed by the FDR model-checker.
展开▼
