密码协议的安全性分析和证明长期以来一直是信息安全研究的热点和难点问题，从事计算机科学和密码学研究的人员对此进行了不懈的研究，也取得了较为丰硕的研究成果：但是，时至今日，这个问题仍然没有很好地解决。密码协议和其他协议不同，人们也许永远无法知道攻击者下一步将采取什么样的攻击手段，有时甚至恰恰就是在那些被认为相当安全的细节出现了微妙的漏洞，要知道即便这样一个微小的漏洞或缺陷有时对于一个聪明的攻击者来说已经足够。也许，这也正是密码协议安全设计和分析的魅力所在。

　　证明密码协议的正确性与安全性的理论和方法通常可以分为两大类：形式化方法和计算复杂性方法。形式化方法可使协议设计者通过系统分析将注意力专注于接口、系统环境假设、系统在不同条件下的状态、条件不满足时系统出现的（异常）情况以及系统不变量等，并通过系统验证为协议提供必要的安全保证；而计算复杂性方法通常又被称为可证明安全性方法，它基于一些最基础的假设或公理（例如，假设单向函数存在，或某些计算问题的困难性等），采用规约的方法，将协议的安全目标规约到一个己知或公认的困难问题。关于这两种方法的详细介绍，请参见相关文献。

　　计算复杂性方法采用了演绎推理方法（例如，从某个已知的假设推出一个结论的逻辑过程），其重点则放在攻破协议到某个公认为困难问题的可证明规约。其中，随机预言机模型（rom）就是这样一种应用最广泛的成功模型，基于rom模型的理论和方法也被称为可证明安全理论。可证明安全理论和技术始于20世纪80年代初期，最初用于分析加密方案和签名方案的安全性，后来则用于分析密码协议的安全性。使用可证明安全性理论来证明协议的安全性主要包括以下5个主要过程：

　　（1）模型描述：

　　（2）该模型内安全目标定义；

　　（3）安全假设说明；

　　（4）协议描述；

　　（5）协议在该安全模型内达到其安全目标的证明。

　　1． 一种rfid协议攻击者模型

　　目前，使用上述两种方法专门来研究rfid协议安全性的公开成果几乎没有。本节仅讨论使用可证明安全性理论和方法来证明和分析reid协议的一些思考，主要讨论模型描述以及该模型内的安全目标定义（可证明安全性理论中最为关键的部分之一）。首先讨论一下rπd系统环境下的攻击者模型。一个rfid系统是由多个主体和通信信道构成的。对rfid协议进行安全性分析时，通常将后台数据库和读写器当作同一个独立和唯一的通信实体来对待。这种处理方法符合大多数rfid系统通信信道安全假设。鉴于前向信道与反向信道的不对称性（如图所示），对它们分别进行处理。这样，攻击者所能获得的信息仅来自于rfid系统的信道，如图所示。在该模型中，所有实体的通信都在攻击者的控制下，攻击者可以任意地读取、插入、删除、篡改、延迟发送、重放任何消息，也可以在任何时候发起与任何实体的任意应答。

　　图 reid系统信道模型用

　　下面用oracle查询来模型化攻击者的能力。用t表示标签，用r表示读写器，两者参与的rfid协议为p。协议双方都可以发起p的多个实例，用πⁱ_t表示第i个标签实例，用πⁱ_t表示第j个读写器实例。攻击者可以进行如下oracle查询。

　　query（πⁱ_t，m1，m3）：该查询刻画了攻击者通过前向信道向t发送消息m1，并在接收到t的应答后再向t发送消息m3。

　　send（πⁱ_t，m2）：该查询刻画了攻击者通过反向信道向r发送消息m2，并接收r的应答。

　　execute（πⁱ_t，πⁱ_r）：该查询刻画了攻击者执行t和r的协议p的一个实例，并获得通过前向信道和反向信道交换的所有消息。

　　execute*（πⁱ_t，πⁱ_r）：该查询刻画了攻击者执行t和r的协议p的一个实例，但是攻击者仅能获得通过前向信道交换的所有消息。

　　corrupt（πⁱ_t，sk）：该查询刻画了攻击者收买t的能力，使t泄漏自己私有存储空间内的密钥信息，并可能会使用攻击者提供的密钥信息sk来代替原t存储区中的内容（依据使用的算法和场景的不同，可能是共享密钥或者公钥）。

　　2． 安全目标定义

　　令t∈{q，s，e，e*，c}，其中q、s、e、e*、c分别表示上述几种oracle查询。攻击者与目标t以及可能的r进行一定的交互过程之后，获得一个交互记录ω（t）。攻击者的攻击目的是要区分t）和t2，以便确认出所攻击的目标。此时，攻击者也可以分别与t；和t2再次进行交互过程，并可以获得两个交互记录ω1（t）和ω2（t）。此时，给定协议p，攻击者的优势定义为：

　　advp（）＝2pr［t1＝t2］－1