|
|||||
|
|
| 移动代理完整性协议形式化分析方法研究 | |
| 引用本文： | 李鹏飞,马恒太,侯玉文,邱田.移动代理完整性协议形式化分析方法研究[J].电子学报,2009,37(8):1669-1674. |
| 作者姓名： | 李鹏飞 马恒太 侯玉文 邱田 |
| 作者单位： | 1. 中国科学院综合信息技术国家级重点实验室,北京,100190;中国科学院软件研究所,北京,100190;中国科学院研究生院,北京,100039 2. 中国科学院综合信息技术国家级重点实验室,北京,100190;中国科学院软件研究所,北京,100190 3. 中国科学院综合信息技术国家级重点实验室,北京,100190;中国科学院软件研究所,北京,100190;天津大学电子信息学院,天津,300072 |
| 基金项目： | 国家自然科学基金(No.60573042);;中国科学院创新基金(No.CXJJ251) |
| 摘 要： | 本文给出了移动代理协议数据完整性属性的定义,指出了采用传统认证性属性来分析移动代理数据完整性属性的不足,从而给出了移动代理完整性证明的两个形式化规约:数据完整性规约和序列完整性规约.在此基础上,针对典型协议实例进行CPS建模,并采用阶函数的方法证明了其完整性,验证了完整性规约的正确性和有效性. |
| 关 键 词： | 移动代理 数据完整性 形式化方法 形式化模型 |
| 收稿时间： | 2008-07-16 |
Research on Formal Analysis Method of Mobile Agent Data Integrity Protocol |
|
| LI Peng-fei,MA Heng-tai,HOU Yu-wen,QIU Tian.Research on Formal Analysis Method of Mobile Agent Data Integrity Protocol[J].Acta Electronica Sinica,2009,37(8):1669-1674. | |
| Authors: | LI Peng-fei MA Heng-tai HOU Yu-wen QIU Tian |
| Institution: | 1;2;3;1;2;1;4;1;3;1.National Key Laboratory of Integrated Information System Technology;Bejing 100190;China;2.Institute of Software;The Chinese Academy of Sciences;Beijing 100190;3.Graduate School;Beijing 100039;4.Electronic Information Technical School;Tianjin University;Tianjin 300072;China |
| Abstract: | This paper gives a formal analysis method of mobile agent data integrity protocol.We pointed out that authentication property is not suit to analysis mobile agent data integrity,and proposed two formal specifications for mobile agent data integrity. We constructed a CSP model for a concrete mobile agent data integrity protocol.checked its integrity using rank function.These works prove formal analysis method is effective in analyzing mobile agent data integrity protocol. |
| Keywords: | mobile agents data integrity path integrity formal analysis formal model |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |
| 点击此处可从《电子学报》浏览原始摘要信息 | |
| 点击此处可从《电子学报》下载免费的PDF全文 | |