A non-repudiation protocol of Zhou and Gollmann [18] has been mechanically verified. A non-repudiation protocol gives each party evidence that the other party indeed participated, evidence sufficient to present to a judge in the event of a dispute. We use the theorem-prover Isabelle [10] and model the security protocol by an inductive definition, as described elsewhere [1,12]. We prove the protocol goals of validity of evidence and of fairness using simple strategies. A typical theorem states that a given piece of evidence can only exist if a specific event took place involving the other party.
CITATION STYLE
Bella, G., & Paulson, L. C. (2001). Mechanical proofs about a non-repudiation protocol. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2152, pp. 91–104). Springer Verlag. https://doi.org/10.1007/3-540-44755-5_8
Mendeley helps you to discover research relevant for your work.