Binding telecooperation -: a formal model for electronic commerce

This paper formally defines the concept "electronic contract" and identifies its "goals", "obligations" and "binding phase". The definitions obtained here are used first for the specification of electronic contracts and secondly for the verification of local implementations of electronic cooperation contracts. The local representation of contracts and the communication between them, multiple and overlapping runs through a binding phase and the role of proofs are treated separately. The definitions are based on the theory of formal languages and automata. They are demonstrated by a simple example of a bilateral offer-order-deliver-pay cooperation. (C) 2001 Elsevier Science B.V. All rights reserved.