Automatic Analysis of a Non-Repudiation Protocol
Ruggero Lanotte, Andrea Maggiolo–Schettini, Angelo Troina · Electronic Notes in Theoretical Computer Science · 2005
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.