We outline the analysis of the HMQV protocol and use it as an example to show how much ”provable security” matters to both theory and practice: Not only does provable security serve as a major tool for analyzing protocols under well defined security properties but also serves as a design tool to achieve more secure, more efficient and simpler protocols. (And, as with any powerful weapon, much care needs to be exercised when using it...)