|
|||||
|
|
| 自动信任协商安全性的形式化分析与验证 | |
| 作者姓名： | 刘欣欣 唐韶华 |
| 作者单位： | 华南理工大学计算机科学与工程学院 |
| 基金项目： | 广东省自然科学基金团队项目(9351064101000003);广东省高等学校珠江学者岗位计划资助项目(2011);广东省高等学校高层次人才项目(2012);广州市科技计划项目(2011J4300028) |
| 摘 要： | 为了对自动信任协商(ATN)的安全性进行形式化分析与验证,文中借鉴安全协议的形式化分析方法,提出一种用进程代数Applied π演算对ATN建模并验证其安全性的方法.该方法将ATN形式化为两个协商者进程的并发执行,其中一个协商者的进程就是对其拥有的证书及授权策略的静态建模;ATN的安全性被定义为Applied π演算的观察等价性,从而使该方法不仅能检查授权策略执行的安全性,而且能对协商者的隐私安全进行验证.借助安全协议的自动分析工具ProVerif,文中实现了对ATN安全性的自动分析.实验结果表明,用Applied π演算形式化及验证ATN的安全性是可行的,安全性验证可自动完成,并且效率较高. |
| 关 键 词： | 自动信任协商 安全性 形式化分析 Applied π演算 观察等价 ProVerif |
| 本文献已被 CNKI 等数据库收录！ | |