安全协议是保证网络安全的重要技术之一，但安全协议自身的缺陷，往往会导致很严重的安全问题。如何验证安全协议能否实现其安全目标，成了研究中的热点问题。近年来，导师苏开乐教授提出了一种基于本地会话的安全协议验证逻辑(LLS)，能有效的对协议的安全性进行分析。由于该理论是一个全新的理论，需要对其进行扩展，以使其能分析更多的协议。 传输层安全协议(TLS，transport layer security)是由IETF在SSL3.0的基础上提出的互联网标准，得到了广泛的应用，其安全性的分析有很高的研究价值。 本文针对对称密钥协商协议的分析，在LLS逻辑的基础上进行了扩展。本文在LLS逻辑最核心的(n，1)-secrecy定理中加入了对协商密钥的分析，针对协商密钥协议要认证的安全规范增加了公理，并对扩展的部分做了证明。随后，本文使用扩展后的LLS逻辑分析了TLS协议的安全性。本文首先分析了认证密钥协商协议的实现目标，包括实体认证、密钥认证、密钥确认、消息完整性等，然后针对TLS协议给出了一系列的具体的验证目标，并对这些验证目标进行了验证。TLS协议允许通信双方新建或重用一个会话，本文对这两种情况分别进行了讨论，并将分析的结果和其他人的工作进行了比较，说明了LLS逻辑的TF确性和优点以及扩展后的LLS逻辑在分析这类协议时的有效性。