Assume-Guarantee Synthesis for Digital Contract Signing

TL;DR

This paper introduces an assume-guarantee synthesis approach for designing fair non-repudiation protocols in digital contract signing, automatically ensuring fairness and attack-freedom, and demonstrating its effectiveness on known protocols.

Contribution

It applies assume-guarantee synthesis to fair non-repudiation protocols, showing it can automatically verify security properties and generate attack-free protocols, a novel approach in this domain.

Findings

AGS succeeds where other synthesis methods fail.

The approach identifies vulnerabilities in existing protocols.

It produces attack-free, symmetric non-repudiation protocols.

Abstract

We study the automatic synthesis of fair non-repudiation protocols, a class of fair exchange protocols, used for digital contract signing. First, we show how to specify the objectives of the participating agents and the trusted third party (TTP) as path formulas in LTL and prove that the satisfaction of these objectives imply fairness; a property required of fair exchange protocols. We then show that weak (co-operative) co-synthesis and classical (strictly competitive) co-synthesis fail, whereas assume-guarantee synthesis (AGS) succeeds. We demonstrate the success of assume-guarantee synthesis as follows: (a) any solution of assume-guarantee synthesis is attack-free; no subset of participants can violate the objectives of the other participants; (b) the Asokan-Shoup-Waidner (ASW) certified mail protocol that has known vulnerabilities is not a solution of AGS; (c) the Kremer-Markowitch (KM) non-repudiation protocol is a solution of AGS; and (d) AGS presents a new and symmetric fair non-repudiation protocol that is attack-free. To our knowledge this is the first application of synthesis to fair non-repudiation protocols, and our results show how synthesis can both automatically discover vulnerabilities in protocols and generate correct protocols. The solution to assume-guarantee synthesis can be computed efficiently as the secure equilibrium solution of three-player graph games.