The vision of global agent-based e-commerce environments that enable dy-namic trading between business partners requires the study and development of suitable formal modeling frameworks. In particular, negotiation is a necessary and importantactivity to allow engagement of business parties in non-trivial business relationships. In this paper we propose a formal framework based on finite state process algebra formodeling and analysis of interaction protocols in agent-based negotiations. The approach is demonstrated by applying the framework to model agent interactions in asingle-item English auction scenario.

multi-agent system, formal specification, process algebra, English auction