From Automata Learning to Model Checking: Formal Security Verification of Black-Box Protocols
The episode discusses a paper from Stefan Marksteiner et al. that uses active automata learning to map black-box protocols and then applies model checking with context-based proposition maps for formal security verification. The discussion covers how this bridges physical hardware interaction with mathematical proofs, allowing automated systems to audit proprietary protocols for vulnerabilities.