身份认证/鉴别和密钥建立协议(在本文中简称为认证协议)作为网络安全的基础部分，直接影响着各种网络应用的安全。研究者们发现，虽然协议的参与主体和消息数目都很少，但设计一个安全的、低冗余的认证协议是很困难的。认证协议的形式化分析在经历二十余年的研究之后，从目标定义、理论模型到实际应用，仍面临着很多未解决的问题。 本文从认证协议的精确目标定义作为出发点，得出认证协议的目标实质为主体对绑定关系的认知获得。在确定研究采用的假设和攻击者模型后，给出了一套简单易行的认证协议安全性分析方法，其中的形式化部分—绑定逻辑—直接从数据的绑定关系分析出发，与以往的逻辑类分析方法有本质的不同。最后，基于绑定逻辑和模块化的协议设计思想，给出了一种模块化的认证协议设计方法。 本文的研究成果包括以下内容：1.认证协议的精确目标是什么，目前仍然争议很多，本文提出了一种通用的目标定义方法，并给出了常见认证目标的该方法应用。 2.给出了一种分步骤的认证协议分析方法，通过攻击环境的划分，使得较容易分析的部分可以从复杂的形式化部分剥离出来。 3.提出一种新的，用于分析认证目标的逻辑系统—绑定逻辑，该逻辑系统简单，易于使用，可直接用于认证目标的推导。 4.应用本文提出的分析方法，对部分认证协议进行了分析，发现了BBF、Neuman-Stubbine、Kryptoknight等协议中未被发布的4个新的攻击。发现了BBF协议、PS-set3协议存在的密钥不一致现象。发现了一些协议中存在的冗余。 5.借鉴CK模型提出的模块化协议设计思想，给出了一套简单易行的认证协议设计方法，通过分别设计被动环境下安全的认证协议和用于将之转换到主动攻击环境下的认证器，协议可以被分步骤地、模块化地的设计和分析。