Formal Specification and Analysis of the Group Domain of Intrepretation Protocol Using NPATRL and the NRL Protocol Analyzer (Preprint)
NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
Pagination or Media Count:
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.
- Computer Programming and Software
- Computer Systems Management and Standards