Mobile agent technology has received a big amount of attention throughout recent years because of its salient merits and promising future. But it also brings significant new security problems. Little work has been done to solve these problems through intuitive formal methods. In this paper, we proposed a new formal model of a secure mobile agent system based on Extended Elementary Object System (EEOS) which combines Object Oriented technology with Petri Nets. This model has three hierarchical levels: mobile agent platform level, mobile agent level and security mechanism level. We also proposed a security mechanism -- synchronous firing security mechanism to detect malicious host attack to mobile agent code or execution flow. This paper also discusses how to translate our EEOS model to a coloured Petri Net model supported by Design/CPN and presents the simulation-based analysis of our EEOS model.