目前,网络通信与人们的日常生产、生活联系日趋紧密,然而它在给人们带来便利的同时,通信的安全问题也凸显出来,这个问题的解决很大程度上需要有好的安全协议来对其进行保障。目前在安全协议的研究领域,当以形式化方法最为流行,目前已经演化成两大领域：符号理论和可证明安全理论。其中,可证明安全理论,是近些年来发展起来的研究方法。该理论是以计算复杂度为基础的,与符号理论相反,它着重于对密码体制的研究,以此来分析、验证、设计安全协议,由于其将安全协议的安全性进行了量化,因此,使协议的安全性更加接近现实、更加可信。本文的理论基础为可证明安全理论,研究重点为该理论下的安全协议分析方法,研究目的是用其来解决实际协议的安全性问题,主要完成了以下工作：1.利用可证明安全思想,在相应的攻击模型下,发现了由于RSA签名算法的缺陷给TLS协议所带来的新攻击。这种攻击是用符号理论方法难以发现的。2.针对RFID搜索协议所存在的标签成本高、安全性差等问题,设计了一个成本较低的RFID搜索协议,并在通用可组合(UC)模型下对其安全性进行了形式化证明。