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 s olved, 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 par ty has fulfilled its part of the agreement. The paper documents Formerly us ed for this purpose are being replaced, in electronic commerce, by informat ion exchanges. The issue of whether these are as trustworthy as pa per docu ments 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 internat ional trade unless the trustworthiness of electronic versions of trade proc edures con be demonstrated beyond reasonable doubt. This article presents a formal specification of a set of design principles For trustworthy trade p rocedures that adapts the basic principles of internal auditing within a co mpany. This auditing method has already been implemented in INTERPROCS, a P rolog-based tool For representation and analysis of procedures. The formal specification of this auditing method can be used to verify audit principle s, and in particular the INTERPROCS implementation of these principles. It is based on a combination of deontic, dynamic, and illocutionary modal logi cs.