Formal Modeling and Security Analysis of Security Protocols

Security protocols are critical components for the construction of secure Internet services but their design and implementation are difficult and error prone. Formal modeling and verification can be extremely beneficial to support the development of secure software. This chapter introduces tools and techniques for the formal modeling and security analysis of cryptographic protocols. It considers the process of constructing a formal model from a given set of requirements, and discusses the theoretical and practical challenges in automated verification. Different specification languages and verification tools are considered to cater to different levels of user expertise and complexity of the protocols under analysis. The chapter includes case studies, demonstrating the practical applicability of these tools in different application fields: e-commerce, e-payments, and blockchain. It also considers modeling and verification in the context of security protocol development, and also introduces the fundamentals like the attacker model and security properties.