作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2007, Vol. 33 ›› Issue (03): 163-166. doi: 10.3969/j.issn.1000-3428.2007.03.059

• 安全技术 • 上一篇    下一篇

概率非否认协议的模型检测分析

董荣胜,陈大伟,郭云川,古天龙   

  1. (桂林电子科技大学计算机科学系,桂林 541004)
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2007-02-05 发布日期:2007-02-05

Model Checking Analysis of Probabilistic Non-repudiation Protocol

DONG Rongsheng, CHEN Dawei, GUO Yunchuan, GU Tianlong   

  1. (Department of Computer Science, Guilin University of Electronic Technology, Guilin 541004)
  • Received:1900-01-01 Revised:1900-01-01 Online:2007-02-05 Published:2007-02-05

摘要: 基于概率模型检测技术,建立了需要保证ε-公平性的非否认协议的概率模型,根据不同行为将主体建立有限状态机模型。使用概率模型检测器PRISM,验证了概率非否认协议的有效性、公平性和时限性。在恶意实体能力和网络环境等不同情况下,分析了破坏协议公平性的概率。

关键词: 非否认, 概率模型检测, PRISM, 有限状态机

Abstract: A probabilistic model which based on probabilistic model checking is proposed for a ε-fair non-repudiation protocol. According to entity’s various behaviors, finite state automaton models are established. Using probabilistic model checker PRISM verifies viable, ε-fair and time-bounded of probabilistic non-repudiation protocol. With malice entity’s ability and network environment various conditions, probabilistic distribution of protocol’s fairness being destroying is analyzed.

Key words: Non-repudiation, Probabilistic model checking, PRISM, Finite state automaton