We design and model-check a simple optimistic fair non-repudiation protocol. Our protocol is considerably simpler than current proposals, due mainly to the avoidance of using session labels. Our analysis technique is supported by exposing several vulnerabilities on weaker versions of our protocol. Some of the properties we check are liveness properties. To verify these, we use an intruder that respects the resilient communication channels assumption.
|Name||Lecture Notes in Computer Science|
|Conference||7th International Conference on Information and Communications Security, ICICS 2005|
|Period||10/12/05 → 13/12/05|
|Other||December 10-13, 2005|