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

Model Checking Analysis of Probabilistic Non-repudiation Protocol

基于概率模型检测技术,建立了需要保证ε-公平性的非否认协议的概率模型,根据不同行为将主体建立有限状态机模型。使用概率模型检测器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.