安全协议验证是保证网络安全的重要技术之一，本文以导师苏开乐教授提出的一种新的基于知识理论的安全协议形式化验证逻辑(本文称其为SPV逻辑)为基础。选取一系列具有代表性的对称密钥交换协议，应用该逻辑对其进行形式化验证，从而研究该逻辑对共享密钥和动态对称密钥加密信息处理的正确性和足够完备性。 文中给出密钥交换认证协议KaoChow和密钥交换协议Yahalom的较为详细的形式化验证过程，通过严格的数学推导证明了协议的认证性等安全性质。从而也进一步证明SPV逻辑在对称密钥交换协议中应用的可靠性。并且，在KaoChow协议的形式化验证过程中，我们发现传输信息的冗余，并在不影响协议安全性质的前提下将协议简化；在Yahalom协议验证过程中我们发现该验证方法公理系统中最为重要的(n，1)-secrecy定理不完备，使得协议本身满足的安全性质无法得到证明。从而发现(n，1)-secrecy定理定义的一个缺陷，并在导师的指导下将定理修正。 为进一步考察SPV逻辑对对称密钥交换协议的处理能力及SPV工具开发的正确性，我们应用SPV工具对大量的密钥交换协议进行了形式化验证。验证结果表明SPV工具可以处理复杂协议及协议的诸如二重规范等复杂安全规范。并且，验证过程中，由于KaoChow的工具验证结果与手工推导出现不一致性，从而发现SPV工具开发存在漏洞。