在安全的分布式系统中，用户需要向通信的对方证实自己的身份，同时也需要建立秘密的会话秘钥，认证协议是使用户达到认证及交换会话秘钥的密码方案。但是认证协议的设计是容易出现错误而又难以发现的。因此，研究如何发现认证协议的漏洞及如何设计安全的认证协议是密码学中非常重要的研究领域。到目前为止，已有许多方法用于验证认证协议的安全性，其中，最著名的形式方法是由Burows, Abadi, Needham提出的BAN-逻辑。但这种逻辑具有许多局限性，其主要原因是没有精确的语义定义和形式的协议理想化方法。本文主要从下列几个方面研究BAN逻辑方法及若干协议的设计：●研究了BAN-逻辑中存在的问题，完善了逻辑分析过程中协议的理想化方法。●对消息重放攻击给出了详细的分类，并提出了防止重放攻击的方法：协议运行时，主体通过对敏感信息的判断，能够判断在协议的并行运行中，是否存在并行攻击。●指出了TMN-协议中存在的漏洞与两种可能的攻击，并对TMN-协议作了进一步的改进。●提出了BAN-逻辑新的语义定义及新的逻辑推理规则，这种语义定义及逻辑推理保留了BAN-逻辑中的大部分思想。区别是推理规则是基于逻辑真值的推理规则，使得“相信”公式具有“正确相信”与“错误相信”的区别。●详细讨论了多方/多项交换的公平性要求及公平交换框架；并设计了多项公平交换的协议，该协议是在“半-信任的”的第三方参与的假设下实施。●讨论了电子彩票及微电子彩票的性质与要求；提出了两种有效的电子彩票发行方案及微电子彩票的实施方案。