摘要： 首先提出了自动信任协商的通用形式化框架，并将典型的信任协商策略规约到上述框架内；其次，基于上述形式化框架对自动信任协商的形式化验证问题进行了定义，确定了形式化验证的目标以及一般流程；再次，研究了典型信任协商策略的形式化验证问题，讨论了相关问题的计算复杂性并得到系列结论；最后，利用逻辑编程方法和模型检测方法实现了自动信任协商的形式化验证。实验结果表明，规则数是影响形式化验证系统运行时间的关键因素，逻辑编程方法和模型检测方法在规则较少时效率较高，但逻辑编程方法的可扩展性不及模型检测方法。