摘要: 基于概率模型检测技术,建立了需要保证ε-公平性的非否认协议的概率模型,根据不同行为将主体建立有限状态机模型。使用概率模型检测器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
董荣胜;陈大伟;郭云川;古天龙. 概率非否认协议的模型检测分析[J]. 计算机工程, 2007, 33(03): 163-166.
DONG Rongsheng; CHEN Dawei; GUO Yunchuan; GU Tianlong. Model Checking Analysis of Probabilistic Non-repudiation Protocol[J]. Computer Engineering, 2007, 33(03): 163-166.