Formal specification of automated auditing of trustworthy trade procedures for open electronic commerce

Abstract

Without an a priori trust relationship between parties it is virtually impossible to establish new trade relationships. One way to create the necessary trust is by using trade procedures that involve exchanges of documents between the trading partners to verify that the counter party has fulfilled his part of the agreement. In electronic commerce these paper documents are replaced by information exchanges. Electronic commerce can only become a success in international trade if the trustworthiness of electronic versions of trade procedures can be proven beyond reasonable doubt. We present the formal specification of the audit daemons method in the procedure analysis tool INTERPROCS for checking automatically the trustworthiness of electronic inter-organizational trade procedures. In the formal specification given in this paper we give an abstract specification of the auditing method, which gives a structured semantics for the key concepts of the auditing method.