Abstract:Strand space is a new model for the analysis of security protocols. In this paper, a systematic study is made on how to prove the existence of vulnerabilities in authentication protocols based on the Strand space. During the proof procedure, the authentication property is proved by using the goal-refined method. Moreover, by introducing type-check mechanism into this model, the proof procedure is simplified significantly. In addition, this method is also applied to authentication protocols involved three prinvolved three principals.At last,the results are got as the relevant literatures.