AppSec Israel 2018

By Ofer Rivlin

The presentation slides can be found at:
https://www.slideshare.net/OferRivlin/how-to-hack-cryptographic-protocols-with-formal-methods


tl;dr: The design of even the smallest security protocols is prone to vulnerabilities. For example, the security protocols of federation & connected cars networks are extremely complex. I explore the use of formal methods for automating validation and hacking cryptographic protocols.
---
Long description:
Key exchange and trust establishment protocols are high risk and complex. Manual security verification of these protocols is error-prone, incomplete, and time-consuming.
Protocol designers are not necessarily security experts. We want to give them the methods and tools that will simplify security assessment and help understand security requirements.
Many standard web protocols for establishing trust between service providers and clients, and with identity providers have proven vulnerable, as well as custom protocols to enable some specific B2B communication (i.e. online payments, cross-domain authentication, etc.)
The target of the talk is to share high-level practicle knowledge of formal methods and to recognize the benefits of using formal methods when designing or attacking cryptography protocols.
I will discuss the following subjects:
Logical issues and attack scenarios in protocols.
Simplifying the secure designing of complex key exchange and trust establishment protocols by using formal methods, automation and the change of mindset.
Demonstrating analysis and hacking of security protocol formal models in domains like SSO & access delegation, IOT and connected vehicles (V2X and VANET - Vehicle Ad Hock Networks).