×

A proof of non-repudiation. (English) Zbl 1017.68574

Christianson, Bruce (ed.) et al., Security protocols. 9th international workshop, Cambridge, UK, April 25-27, 2001. Revised papers. Berlin: Springer. Lect. Notes Comput. Sci. 2467, 119-125 (2002).
Summary: The Inductive Approach for protocol verification, extended with a formalisation of message reception and agents’ knowledge, is adopted here for reasoning about non-repudiation protocols. The fair non-repudiation protocol due to Zhou and Gollmann is modelled inductively in Isabelle/HOL. The verification focuses on the validity of evidence goal: that the evidence held by each peer at the end of a session suffices to refute the other’s denial of participation. The proof strategies appear to be general thus far, but the fairness goal is yet to be studied.
For the entire collection see [Zbl 1010.68829].

MSC:

68U99 Computing methodologies and applications
68M12 Network protocols
68P25 Data encryption (aspects in computer science)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI