摘要
基于概率模型检测技术,建立了需要保证ε-公平性的非否认协议的概率模型,根据不同行为将主体建立有限状态机模型。使用概率模型检测器PRISM,验证了概率非否认协议的有效性、公平性和时限性。在恶意实体能力和网络环境等不同情况下,分析了破坏协议公平性的概率。
A probabilistic model which based on probabilistic model checking is proposed for a e-fair non-repudiation protocol. According to entity's various behaviors, finite state automaton models are established. Using probabilistic model checker PRISM verifies viable, e-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.
出处
《计算机工程》
CAS
CSCD
北大核心
2007年第3期163-166,共4页
Computer Engineering
基金
广西壮族自治区自然科学基金资助项目(桂科自0542052)
关键词
非否认
概率模型检测
PRISM
有限状态机
Non-repudiation
Probabilistic model checking
PRISM
Finite state automaton