A formal analysis of auditing principles for electronic trade procedures

One of the major issues involved in establishing new trading relationships is the lock of an a priori trust relationship between the parties. This is an old and well-known problem in international commerce. Unless it can be solved, establishing new trading relationships will be virtually impossible. One way to create the necessary trust is by using procedures that involve exchanges of documents between the trading partners to verify that each party has fulfilled its part of the agreement. The paper documents Formerly used for this purpose are being replaced, in electronic commerce, by information exchanges. The issue of whether these are as trustworthy as pa per documents remains a crucial question. It is easy to guarantee the uniqueness of ownership documents in the case of signed paper documents, but much harder with electronic messages. Electronic commerce will not succeed in international trade unless the trustworthiness of electronic versions of trade procedures con be demonstrated beyond reasonable doubt. This article presents a formal specification of a set of design principles For trustworthy trade procedures that adapts the basic principles of internal auditing within a company. This auditing method has already been implemented in INTERPROCS, a Prolog-based tool For representation and analysis of procedures. The formal specification of this auditing method can be used to verify audit principles, and in particular the INTERPROCS implementation of these principles. It is based on a combination of deontic, dynamic, and illocutionary modal logics.