一种验证RFID安全协议不可追踪性的形式化分析方法

本申请涉及一种验证RFID安全协议不可追踪性的形式化分析方法。所述方法包括：利用进程演算对RFID安全协议中的消息进行形式化描述，将协议中的通信行为抽象为可操作的数学模型后根据项重写系统来构建攻击者的能力模型；基于攻击者的能力模型用约束系统符号化表示RFID安全协议的执行迹，利用执行迹定义不可追踪性标准来评估攻击者是否能从执行迹中推断出特定标签或用户的身份或行为；根据不可追踪性标准将验证不可追踪性的问题转化为判断两个约束系统是否具有相同解的问题，对约束系统进行约束求解，根据求解结果实现系统的不可追踪性分析。采用本方法能够实现快速的计算机自动化验证。