Interaction tracing for mobile agent security

This thesis develops a new technique, interaction tracing, to address the security issue of protecting mobile agents from potentially malicious hosts. In this technique, a mobile agent is modeled as a black box whose behaviour can be captured through a trace of its inputs and outputs during the process of execution. Formalization of the activity of creating and verifying traces is detailed for a simple agent programming language using operational semantics. An interaction protocol is developed to enable secure exchange of traces between entities in the system that are responsible for verifying the validity of the traces. This protocol is formally modeled and verified for specific security properties using a finite-state model checker. The protocol is extended to allow for the activity of trace reconciliation, which protects inter-agent communication between mobile agents operating in a multi-agent context. Implementation of this secure protocol in conjunction with the interaction tracing activity is undertaken in a mobile agent framework and is quantitatively evaluated against a non-secure mobile agent system and standard client-server approach. A trust model is introduced in the context of the protocol that allows trust relationships to be formed between the various entities in the system, permitting a more flexible deployment of the protocol