形式化验证基于可认证网络编码的网络传输协议安全性

he processing of network coding can improve network throughput, save network resources and reduce the times of forwarding messages in network. However, the information is very vulnerable to pollution attacks during the processing of building the encoded messages. Homomorphic signature scheme for network coding can resist pollution attacks. Authenticated network coding is network coding based on digital signature . As far as we know that few report come out at home and abroad according to formal validation on security of authenticated network coding. In this paper, we introduced AVISPA tools to validate formally the security of authenticated network coding based network transport protocols and built the formal model. Then we gave the major of HLPSL program and the result of formal validation and validated the security of authenticated network coding transport protocol.