從串空間模型理論人手，提出了三種典型的串空間形式化方法(基于極小元理論的串空間方法、基于理想與誠實理論的串空間方法、基于認證測試理論的串空間方法)，并對每一種方法的證明步驟及優(yōu)缺點進行了分析。在此基礎上，應用提出的串空間方法對Yahalom協(xié)議的秘密性和認證性進行了分析。分析結果表明利用不同方法的優(yōu)點，能更好地保證安全協(xié)議形式化分析的準確性。