Formal Specification and Analysis of the Group Domain of Interpretation using NPATR and the NRL Protocol Analyzer

Although research has been going on in the formal analysis of cryptographic protocols for a number of years, they are only slowly being integrated into the protocol design process. In this paper we describe how we furthered the integration of analysis and design by working closely with the Multicast Security Working Group in the Internet Engineering Task Force on the analysis of a proposed Internet Standard, the Group Domain Of Interpretation (GDOI) Protocol. We describe the challenges that had to be met before the analysis could be successfully completed, and some of the challenges that still remain. Perhaps not surprisingly, some of the most challenging work was in understanding the security requirements for group protocols in general. We give a detailed specification of the requirements for GDOI, describe our formal analysis of the protocol with respect to these requirements, and show how our analysis impacted the development of GDOI.