安全协议是用来保证电子商务等网络通信安全的重要工具。形式化方法是当今分析安全协议的一类主流方法，但是不同的形式化方法各有优劣，且应用形式化方法研究安全协议在理论和实践上还不够充分。 本文对BAN逻辑进行了较为全面地介绍，并在此基础上探讨了将其应用于协议认证性形式化分析中的优势和具体方法。为分析Yahalom协议认证性，论文给出了Yahalom协议基于SVO逻辑的模型，并通过详细的推理分析了Yahalom协议的认证性质。为了进一步分析协议的机密性等性质并对协议本身进行更深入研究，论文引入串空间理论，接着对其中的丛理论、攻击者行为定义、“理想”和“诚实”等概念作了深入剖析。然后，利用串空间方法建立BAN-Yahalom协议的形式化模型，并全面分析了其安全性质，证明了其中的安全缺陷并找出其原因，随后提出了积极的修改方案并对协议进行修改。为使对安全协议的分析能逐渐自动化，论文详细介绍了使用模型自动校验器Spin的基本方法，以及Promela语言的关键技术。以NSPK协议为例，论文提出了利用Spin进行协议建模的基本思想、算法和技术，并深入介绍了建立NSPK协议模型的具体方法，模型仿真执行的结果也反映出文中所述的建模方法是可以收到良好效果的。