Website Maintenance Alert
Due to scheduled maintenance, the USENIX website will not be available on Tuesday, December 17, from 10:00 am to 2:00 pm Pacific Daylight Time (UTC -7). We apologize for the inconvenience.
If you are trying to register for Enigma 2020, please complete your registration before or after this time period.
Security Analysis of Network Protocols
Network security protocols, such as key-exchange and key-management protocols, are notoriously difficult to design and debug. Anomalies and shortcomings have been discovered in standards and proposed standards for a wide range of protocols, including public-key and Diffie-Hellman–based variants of Kerberos, SSL/TLS, and the 802.11i (Wi-Fi2) wireless authentication protocols. Although many of these protocols may seem relatively simple, security protocols must achieve their goals when an arbitrary number of sessions are executed concurrently, and an attacker may use information provided by one session to compromise the security of another.
Since security protocols form the cornerstone of modern secure networked systems, it is important to develop informative, accurate, and deployable methods for finding errors and proving that protocols meet their security requirements. This talk will summarize two methods and discuss some of the case studies carried out over the past several years. One method is a relatively simple automated finite-state approach that has been used by our research group, others, and several years of students in a project course at Stanford to find flaws and develop improvements in a wide range of protocols and security mechanisms. The second method, Protocol Composition Logic (PCL), is a way of thinking about protocols that is designed to make it possible to prove security properties of large practical protocols. The two methods are complemen- tary, since the first method can find errors, but only the second is suitable for proving their absence. The talk will focus on basic principles and examples from the IEEE and IETF standardization process.
Open Access Media
USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.