Abstract: The security protocol model is the basis of the security protocol analysis and verification. Existing modeling methods have some shortcomings, such as high complexity, bad reusability, and so on. A typed π calculus—π/+t calculus is presented in this paper, and its type rules and evaluation rules are also given. It is proved that π/+t calculus is a safely typed system. π/+t calculus can be used to build formal models of security protocols and their attackers. NRL protocol is taken for an example to show how to build a security protocol model based on π/+t calculus. The attacker model for a security protocol is also presented in this paper. The action ability which the attacker model based on π/+t calculus has is proved the same to the D-Y attacker model. So the correctness of the results which come from verifying the security protocol models based on π/+t calculus is promised. The security protocol modeling approach based on π/+t calculus can give more detailed description of the semantics of protocol data and the knowledge of participators. Compared with other kinds of methods, this method has better usability and high reusability and can provide more analysis support. The analysis result shows that the method can detect flaws of a security protocol in its modeling process.