Start Them Early And Keep On Keepin’ On. An Industry Perspective On Automated Protocol Analysis For Designing And Iterating Cryptographic Protocols

Due to the ever-evolving needs of applications, cryptographic best-practice recipes are sometimes ill-fitted to the problem at hand. Consequently, subtle changes to robust protocols are frequently introduced without rigorous analysis, leading to potentially catastrophic outcomes. The recently discovered vulnerabilities in Telegram, Threema, and MEGA demonstrate the importance of rigorous analysis. Although “Don’t roll your own” is helpful advice, it fails to provide tools to reduce the risks of novel cryptographic designs. In contrast, automated protocol analysis has the potential to help strengthen the initial protocol design and support future iterations of the protocol. This talk presents an industry perspective on automated protocol analysis, its impact on security audits we perform at Trail of Bits, and the value it provides to our customers. Automated analysis has limits, and we will discuss them. This talk is also a call to the community to reflect on possible improvements to existing tooling, including usability and continuous translation of insights from real-world attacks and formal analysis into actionable items for application developers. A fruitful collaboration on increased usability, meaningful security goals, and analyses with automated tooling has the potential to make automated analysis an invaluable layer in the Swiss-cheese model for security systems that rely on cryptography.