A formal methodology for integral security design and verification of network protocols
HighlightsAn iterative methodology for verifying communication protocols, combining formal and informal analysis, is presented.When security flaws are detected, it provides feedback for easing their resolution.Three case studies with real protocols are introduced to show the benefits of such methodology.The first two case studies (MANA III and WEP's Shared Key Authentication) show how some weaknesses could have been detected.The third case study shows the complete process of verification of a new protocol for obtaining digital identities. In this work we propose a methodology for incorporating the verification of the security properties of network protocols as a fundamental component of their design. This methodology can be separated in two main parts: context and requirements analysis along with its informal verification; and formal representation of protocols and the corresponding procedural verification. Although the procedural verification phase does not require any specific tool or approach, automated tools for model checking and/or theorem proving offer a good trade-off between effort and results. In general, any security protocol design methodology should be an iterative process addressing in each step critical contexts of increasing complexity as result of the considered protocol goals and the underlying threats. The effort required for detecting flaws is proportional to the complexity of the critical context under evaluation, and thus our methodology avoids wasting valuable system resources by analyzing simple flaws in the first stages of the design process. In this work we provide a methodology in coherence with the step-by-step goals definition and threat analysis using informal and formal procedures, being our main concern to highlight the adequacy of such a methodology for promoting trust in the accordingly implemented communication protocols. Our proposal is illustrated by its application to three communication protocols: MANA III, WEP's Shared Key Authentication and CHAT-SRP.