随着电子商务的飞速发展和广泛应用，网络安全及其形式化分析引起社会的密切关注，逐步成为计算机科学研究的热点领域。非否认技术作为网络安全中最具价值的研究问题之一，在避免电子商务参与主体因事后否认所进行的交易行为，而给对方造成经济损失或推卸己方的责任方面发挥着重要的作用。非否认协议是非否认技术的一种具体实现，它通过协议设计使得协议主体无法否认其交易行为，即达成协议的非否认性。 本文在已有相关研究成果的基础上，系统地研究了非否认协议的设计和形式化分析。主要工作内容和研究成果有： (1)给出了一种非否认协议的设计方法。该方法将非否认协议分成安全协议和密码系统两部分，在假设密码系统是完善的基础上，分别从认证保密性和非否认性两部分对安全协议进行设计与分析。 (2)在认证保密性的设计和分析中，指出了A(0)协议存在的不能抵抗重放和伪冒攻击的不足，在修改原协议的消息格式和增加握手确认消息的基础上，提出了一种A(0)协议的改进方案，并应用SVO逻辑对修改后的协议进行了形式化分析，验证了其满足主体身份的认证性和临时会话秘钥的保密性。 (3)在非否认性的设计和分析中，对ZG协议及其改进协议进行了分析，指出了它们的缺陷与不足，提出了NZG协议，并对NZG协议的安全性和效率进行了分析。 (4)在SVO逻辑、Kailar逻辑和卿斯汉的形式化分析方法的基础上，进行了改进和扩充，提出了一种新的非否认协议形式化分析方法BSFA。新方法不仅能分析非否认协议的可追究性和公平性，还能对协议中的时限性问题进行分析。 (5)设计了一个非否认协议：并根据在电子交易中对安全性要求的高低不同，分别给出了满足安全性要求的两种变型协议。