随着计算机网络通信的迅猛发展,网络安全开始被人们所重视,其中安全协议分析验证已成为一个研究热点。对安全协议的分析验证的方法和手段有很多,其中形式化分析方法已被证明是分析和验证安全协议的最为有效手段。RFID(Radio Frequency Identification)技术近年来得到了长足的发展,成功的应用于各个领域,但由于RFID系统组成的特殊性,分析与设计安全、高效、低成本的RFID安全协议仍然是一个具有挑战性的课题,它的研究对安全协议、电子商务、RFID系统领域具有重要的意义。首先,本文以串空间理论作为基础建立动作集合、事件集合、串以及串空间,将协议实体模型化,并通过通信端的理想与诚实界定攻击者的能力,用以发现协议实体中可能出现的漏洞。然后,分析了现有的RFID安全协议的优缺点,使用串空间理论方法着重分析了其中的数字图书馆RFID协议,根据分析结果提出了一个RFID系统的安全协议,并根据BAN逻辑分析方法的分析结果对其进行了相应修改,得到了一个适用于RFID系统的DRAP协议模型,随后通过串空间理论对其优缺点以及攻击者能力作出了精确的描述。最后,本文根据先前的分析结果,采用三方通信密码命中的模拟方式进行试验。使用基于ACE(Adaptive Communication Environment)框架的C++语言对上述协议模型进行实现,得到相关试验数据,经对比分析试验数据验证了分析结果的正确性。