Security modeling based on CSP for network protocol

The secure vulnerabilities of network protocols are likely exploited by malicious users to cause damage even disaster. In the paper we proposed an approach to analyze, model and verify the network protocols using the process algebra CSP. First, extract the basic grammar, semantics and rules by analyzing the network protocol. Model the basic logic structure of the protocol, potential intruders in real environment and security constraints of the protocol as CSP processes; then use model checking techniques to verify the model and find out the vulnerabilities of protocol. With this method we modeled and verified Border Gateway Protocol (BGP). From the result analysis we have found manin- the-middle attack which may arise because of lacking authentication between two interconnected peers.