Various modern protocols tailored to emerging wireless networks, such as body area networks, rely on the proximity and honesty of devices within the network to achieve their security goals. However, there does not exist a security framework that supports the formal analysis of such protocols, leaving the door open to unexpected flaws. In this talk I'll present such a security framework, show how it can be implemented in the protocol verification tool TAMARIN, and use it to find previously unknown vulnerabilities on two recent key exchange protocols.

Dr. Rolando Trujillo is a Ramon y Cajal fellow at Rovira i Virgili University (URV). His research interests span the areas of formal methods, computer security and privacy protection. His work appears in important publication venues, such as ACM CCS, S&P, ESORICS and CSF.