Automatic Analysis of a Non-Repudiation Protocol

We define a probabilistic model for the analysis of a Non-Repudiation protocol that guarantees fairness, without resorting to a trusted third party, by means of a probabilistic algorithm. By using the PRISM model checker, we estimate the probability for a malicious user to break the non-repudiation property, depending on various parameters of the protocol.