Formal security analysis of authentication in SNMPv3 protocol by an automated tool

Recently, the verification of network management protocols has been the subject of many research works. SNMP (Simple Network Management Protocol) is a widely used protocol for monitoring and managing devices on IP networks. Three significant security features (authentication, encryption, access control) are added to SNMPv3 under the User-based Security Model (USM). Until now, no formal and automated verification methods have been proposed for network management protocols and they have been analyzed only with informal techniques or with symbolic methods which is a hard, time-consuming and error-prone task when done by hand. Hence, in this paper, we first describe the SNMPv3 protocol and propose an abstract model of it to formalize our understanding of SNMP, and provide a specification of SNMPv3 in the applied π-calculus. We verify authenticity in SNMPv3 protocol without bounding the number of sessions of the protocol, using an automated protocol verifier, ProVerif and we show a proof of authenticity for the SNMPv3 protocol.