Tom Chothia (University of Birmingham)

Blackbox and Grey-box Approaches to Protocol State Machine Learning (With Lots of Attacks Against TLS and WPA)

Protocol state machine learning has been used to analyse many cryptographic protocols. Unlike fuzzing it can find logical flaws in protocols and unlike formal modelling it can find vulnerabilities in implementations. I will outline how black box state machine methods work, and describe how we have applied them to WPA to find two downgrade attacks. I will then describe a grey box learning method we have developed that uses memory snapshots and symbolic execution of the binary, combined with observations of run-time memory and a protocol's inputs and outputs to learn its state machine. We show that this grey box method is much more efficient than black box learning, allowing us to test protocols in much more detail and leading to the discovery of new attacks against implementations of TLS and WPA.

Jam Ramanujam (IMSc Chennai)

Insecurity, going from terms to formulas

Abstract: Reasoning about cryptographic protocols starts with a term algebra of communicated terms over which an appropriate logic is built, with variables designating terms. In logics of announcements, formulas are communicated, blurring the distinction between terms and formulas. Constructs such as zero knowledge proofs and certificates are akin to formulas, motivating a similar extension to reasoning about security protocols as well. However, the interaction between equality and the existential quantifier leads to interesting twists: witnesses for existential quantifiers may be unbounded, and obtaining small witness terms while maintaining equality proofs complicates the analysis considerably. In this talk we attempt to highlight the challenges in reasoning about insecurity when formulas are communicated.
This work is joint with Vaishnavi Sundararajan and S P Suresh.

Fulvio Valenza (Politecnico di Torino)

Formal and Automatic Network Security Configuration

The next-generation networks introduced higher flexibility and dynamicity in networking systems, but at the same time, they led to new threats and challenges. The traditional approach of a manual configuration of Network Security Functions (NSFs) such as firewalls and VPN gateways is not feasible anymore since it is not adequate for the ever-changing nature of modern networks and it is prone to human errors. To overcome this problem, the native flexibility provided by virtualization could be exploited to automate network security management. However, achieving a high level of automation while providing formal assurance that security management operations (e.g., configuration and orchestration) fulfill some security properties is still a complex research challenge. This presentation describes some novel approaches that combine automation, formal verification, and optimization for network security management. This is a joint seminar with FM-SEC. Attendance via Zoom (ID: 933 8257 2879, Passcode: 546836) Livestream via Youtube