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