Research on formal description and verification of automated trust negotiation

GUAN Shang-yuan 1; WU Wei-guo 1; DONG Xiao-she 1; QIAN De-pei1

您当前的位置：

首页 >

文章列表页 >

Research on formal description and verification of automated trust negotiation

更新时间：2024-10-14

- Research on formal description and verification of automated trust negotiation
- Vol. 32, Issue 2, Pages: 86-99(2011)
- 作者机构：
  
  1. 西安交通大学计算机科学与技术系
  2. 北京航空航天大学计算机科学与工程学院
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP393.08
- Published：2011
- 稿件说明：
移动端阅览
GUAN Shang-yuan 1, WU Wei-guo 1, DONG Xiao-she 1, et al. Research on formal description and verification of automated trust negotiation[J]. 2011, 32(2): 86-99.
DOI：

GUAN Shang-yuan 1, WU Wei-guo 1, DONG Xiao-she 1, et al. Research on formal description and verification of automated trust negotiation[J]. 2011, 32(2): 86-99. DOI：

摘要

首先提出了自动信任协商的通用形式化框架

并将典型的信任协商策略规约到上述框架内;其次

基于上述形式化框架对自动信任协商的形式化验证问题进行了定义

确定了形式化验证的目标以及一般流程;再次

研究了典型信任协商策略的形式化验证问题

讨论了相关问题的计算复杂性并得到系列结论;最后

利用逻辑编程方法和模型检测方法实现了自动信任协商的形式化验证。实验结果表明

规则数是影响形式化验证系统运行时间的关键因素

逻辑编程方法和模型检测方法在规则较少时效率较高

但逻辑编程方法的可扩展性不及模型检测方法。

Abstract

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.

关键词

Keywords

references

Views

870

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Reversible data hiding in encrypted domain based on fine-grained access control

Byzantine fault-tolerant distributed access control mechanism for the Internet of things

Modeling and verification of data circulation control based on timed automata

Multi-keyword attribute-based searchable encryption scheme supporting re-encryption for cloud storage

Blockchain-based noisy data sharing control protocol

Related Author

ZHANG Minqing

PENG Shen

JIANG Chao

DI Fuqiang

DONG Yufeng

CHAI Rong

AI Liping

YANG Ningyu

Related Institution

College of Cryptography Engineering, Engineering University of PAP

Key laboratory of CTC&IE (Engineering University of PAP), Ministry of Education

School of Communications and Information Engineering, Chongqing University of Posts and Telecommunications

Chongqing Key Laboratory of Mobile Communication Technology

Institute of Information Engineering, Chinese Academy of Sciences

AI问答

⁰