Formal description and verification of interaction protocols is an important field of MAS. In this paper a calculus for describing interaction protocols of MAS is defined. The calculus is based on process algebra and is independent of any particular model of rational agency. This makes it applicable to verify the protocol of heterogeneous agent systems. With the formal semantics of calculus, some properties of session protocols, e.g. termination, deadlock, can be verified. The approach can avoid the problem of semantic verification, because the states of the protocol are defined in the protocol itself. The formal interaction protocol specifies the complex concurrent and asynchronous pattern of communication between agents and can be verified straightforward that whether an agent acts in accordance with the protocol or not.