Abstract

Formal verification and attack sequence generation of cryptographic protocol based on CP-nets

Author(s): Bai Yunli, Yang Ting, Mi Xiaoqin

An attack sequence is an execution sequence that is guaranteed to lead to a failure if the cryptographic protocol model under verification does not meet its security properties. The efficiency of generating the attack sequences for a cryptographic protocol model N is improved if N has a sub-model of security property violation events, which effectively reduced the searching scope of the state space of the protocol model. Previous work shown that, cryptographic protocol formal modelling and attack sequence generation method using CPnets is based mainly high complexity of the whole state space search methods. This paper presents an improved security property violation events based model validation and attack sequence generation method, using the method for modelling and analyzing NS protocol, experimental results are used to evaluate the proposed method.