网构软件信任机制的形式化研究

Study on formalization of trust mechanism for Internetware

Internet环境下构件群体间信任关系的形式化建模是实现其仿真的关键环节,给出了信念逻辑及信任关系的形式化定义,包括形式化描述、分析、逻辑推理及证明过程,以及信任链建立和传递过程中成立的语义解释和约束条件,并结合PKI模型实例对信任链的建立过程进行了形式化描述与推演.提出了一种可行的最优化信任链搜索算法(GSTC)和多路径信任聚合算法(MPTA).通过仿真实验对比了GSTC算法和RSTC算法、以及MPTA算法在受限和非受限条件下的性能.网构软件信任逻辑形式化方法的建立,揭示了构件间信任逻辑的建立和推理过程,不仅能够满足构件信任方面服务质量的需求,有效的提高整个网络的信任水平;而且有助于解决真实环境下构件实体间存在的安全问题,为构件集群环境下安全控制及信任系统形式化研究提供了有价值的新思路.

The formal modeling of the trust relationship between Internetware systems is a crucial link in the realization of its simulation.In this paper the formal definition of belief logic and trust relationship was presented,including formal specification,logical reasoning,and the analyzing and proving processes.The semantic interpretation and constraints during the establishment and transmission process of the trust chain were given.Combined with a PKI model and instances,the formalization description and deduction of the trust chain＇s establishing process were demonstrated.In particular,an optimum and feasible trust chain＇s searching algorithm was put forward-greedy strategy for trust chain（GSTC）-along with a multiple path trust aggregation algorithm-multiple path trust aggregation（MPTA）.Through experimental analysis the capability of the GSTC and RSTC algorithms was compared.Furthermore,the performance of MPTA algorithm under restrained and non-restrained conditions was compared.With the build-up of the formalization approach for Internetware trust logic,the establishing and reasoning process of trust logic between Internetware components was revealed.It not only satisfied the requirements of quality of service on the Internetware＇s trust mechanism and effectively enhanced the trust level of the entire network,but assisted in solving the secure problems existing in component entities under real environments,and provided a valuable new thread for studying secure component control under a cluster environment and formalization of trust systems.