摘要
首先提出了自动信任协商的通用形式化框架,并将典型的信任协商策略规约到上述框架内;其次,基于上述形式化框架对自动信任协商的形式化验证问题进行了定义,确定了形式化验证的目标以及一般流程;再次,研究了典型信任协商策略的形式化验证问题,讨论了相关问题的计算复杂性并得到系列结论;最后,利用逻辑编程方法和模型检测方法实现了自动信任协商的形式化验证。实验结果表明,规则数是影响形式化验证系统运行时间的关键因素,逻辑编程方法和模型检测方法在规则较少时效率较高,但逻辑编程方法的可扩展性不及模型检测方法。
First,a unified ATN formal framework was presented,into which typical negotiation strategies could be reduced.Second,the formal verification of ATN was defined based on the formal framework.The objectives and procedures of the formal verification of ATN were described.Third,several typical negotiation strategies were discussed,and the computational complexity of the corresponding verification problems was shown,several conclusions had been obtained.Last,the formal verification of ATN was implemented by using logic programming and model checking methods.The experimental results show that the number of rules is a crucial factor in determining the runtime.Both logic programming and model checking are efficient when the number of transition rules is small,and logic programming does not scale as well as model checking.
出处
《通信学报》
EI
CSCD
北大核心
2011年第2期86-99,共14页
Journal on Communications
基金
国家自然科学基金资助项目(60773118)
国家高技术研究发展计划("863"计划)基金资助项目(2006AA01A109
2009AA01Z108)~~
关键词
访问控制
信任协商
形式化方法
计算复杂性
安全性
access control
trust negotiation
formal methods
computational complexity
security
