Model Checking Analysis of Probabilistic Non-repudiation Protocol
Tianlong Gu · Jisuanji gongcheng · 2007
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.