Protocol State Machines and Session Languages

Explore the intricacies of protocol state machines and session languages in this IEEE conference talk presented at the 2015 LangSec Workshop. Delve into the critical role of input languages in language-theoretic security and their impact on application vulnerabilities. Examine the complexities of session languages, which involve sequences of messages forming dialogues between two parties. Discover how poorly specified and implemented session languages can lead to security issues. Learn about the potential of automatically inferring formal specifications of these languages through protocol state machines using black box testing. Gain insights into various examples, including OpenSSH, EMV, and TLS implementations, to understand the practical implications of broken state machines. Explore visual indications, Lstar algorithm, and the Disstate tool for state machine inference. Conclude with a discussion on practical problems and engage in a Q&A session to deepen your understanding of this crucial aspect of cybersecurity.

Introduction
Motivation
Visual Indication
Broken State Machines
OpenSSH
State Machines
Lstar
EMV
State Machine
Inference
Disstate
TLS
TLS implementations
Conclusion
Practical Problems
Questions