随着网络技术的不断发展,网络与信息安全的重要性日益引起人们的关注。安全协议是以密码学为基础的协议,为网络系统提供各种安全服务。安全协议分析涉及协议的机密性,完整性,非否认性,公平性等多个方面,是目前网络与信息安全研究的热点和难点。本文是进行安全协议的模型化认证研究。对主动网络下的需求装载协议进行了研究,指出了现有协议的不足之处,提出了一种基于Hash函数的新协议,经分析效率较现有协议更高,并利用Spi演算模型进行了安全证明。对OPT(一次一密认证系统)协议进行了分析,针对其存在的安全缺陷,提出了一种新的改进协议,有效的增强了安全性。利用串空间认证测试方法对TMN(移动通讯密钥交换协议)协议的安全性进行了证明,同时提出了两种新的协议,扩展了现有协议。论文主要工作和贡献如下:1、对主动网络平台下的需求装载协议进行了改进,并利用Spi演算对新协议进行了安全性证明;2、针对OPT认证技术的缺陷,提出了一种新认证技术,有效解决了其存在的问题;3、利用串空间认证测试方法对TMN协议进行了安全证明,提出了两种新的改进方案;