Automated formal analysis of NetConf protocol for authentication properties

Author

Izadi, F. ; Shahhoseini, Hadi Shahriar

Author_Institution

Iran Univ. of Sci. & Technol., Tehran, Iran

fYear

2012

Firstpage

1055

Lastpage

1059

Abstract

When a network manager wants to install, manipulate, and delete network devices configuration, he needs to use NetConf protocol. NetConf is a one of the famous protocols for configuration and management of network devices, based on a flexible XML-encoded message format. This protocol is recently proposed by the IETF and under RFC6241. We work with pi calculus and extensive model applied pi calculus of Abadi and Fournet which are the input languages our tool used. In this paper, using the ProVerif cryptographic protocol verifier, we first analyze the NetConf protocol defined in the RFC6241, which relies on transport layer for authentication. Then identity manager for device will be authenticated.

Keywords

XML; cryptographic protocols; formal verification; message authentication; pi calculus; IETF; NetConf protocol; ProVerif cryptographic protocol verifier; RFC6241; XML-encoded message format; authentication property; automated formal analysis; identity manager; pi calculus; transport layer; Authentication; Calculus; Cryptographic protocols; Cryptography; Servers; NetConf protocols; Proverif tool; authentication properties; pi calculus; verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Telecommunications (IST), 2012 Sixth International Symposium on

Conference_Location

Tehran

Print_ISBN

978-1-4673-2072-6

Type

conf

DOI

10.1109/ISTEL.2012.6483142

Filename

6483142