Compositional reasoning about security properties of network protocols is a notoriously hard problem. I will illustrate some of the challenges by presenting a structured security analysis of the voice-over-IP
(VoIP) protocol stack. The VoIP stack consists of signaling, session description, key establishment, and secure media transport protocols. Using a combination of manual and tool-supported formal analysis, we uncovered several design flaws and attacks, most of which are caused by subtle inconsistencies between the assumptions that protocols at different layers of the VoIP stack make about each other.
Back to Workshop II: Applications of Internet MRA to Cyber-Security