移动代理数据完整性保护协议分析与实现技术研究

移动代理技术是未来网络计算的一种新模式，特别适合于电子商务领域。其安全性是制约移动代理技术能否广泛应用的重要因素，数据完整性是其中的一个关键问题。 移动代理数据完整性保护协议的设计和安全性分析是移动代理安全性研究的重点和难点。本文从对移动代理环境下的数据完整性属性研究入手，给出了移动代理数据完整性新定义，以此为基础给出了一种分析移动代理协议完整性属性的有效方法，并以典型协议为实例验证了该方法的有效性，针对实例分析中所发现的缺陷，设计了一个可配置移动代理数据完整性保护协议。本文主要创新性工作包括： （1）对移动代理数据完整性进行了重新定义。通过划分安全目标和执行环境，从节点数据完整性和路径完整性两方面对比分析了移动代理数据完整性同传统消息完整性的联系和区别，给出了移动代理数据完整性的新内涵和形式化描述，为此类协议的形式化验证和设计提供了基础。 （2）采用CSP方法建立了典型移动代理数据完整性保护协议的形式化模型。通过对参与者信任程度的划分，建立了此类协议的通用模型结构，用CSP方法描述协议参与者进程和消息集合，建立了此类协议的形式化模型。该模型可以较好地表示协议在多轮次、参与者数量不确定情况下的执行情况。 （3）给出了移动代理路径完整性形式化规约，建立了基于阶函数的路径完整性分析方法。通过路径完整性形式化规约，建立了路径完整性同证据唯一性的关系，通过基于阶函数的路径完整性证明定理，给出了基于阶函数的移动代理路径证据唯一性证明方法，构建了一套移动代理路径完整性分析的形式化方法。 （4）构造了针对典型的移动代理数据完整性保护协议的新型攻击。采用基于阶函数的移动代理完整性分析方法，对PM协议和Cheng-Wei协议进行了分析，发现了协议中存在的路径完整性保护缺陷，并构造了针对该缺陷的概率攻击方案，验证了模型和分析方法的有效性。 （5）给出了移动代理数据完整性保护协议安全限制条件，设计了一个可配置移动代理完整性保护协议。该协议在一定条件下可以防止所发现的新攻击。并给出了该协议在具体条件下的形式化分析结果，证明了该协议在具体条件下能够保证数据的完整性。