Description
The design and security analysis of protocols that use cryptographic
primitives is one of the most fundamental and challenging areas of
computer security research. This project focuses on three topics:
foundations of protocol analysis, automated tools, and application of
tools and methods to selected protocols. Foundational work centers on
relating and combining two previously separate approaches: logical methods
based on symbolic execution of protocols, and computational methods
involving probability and polynomial-time. The symbolic approach uses a
highly idealized representation of cryptographic primitives and has been
a successful basis for automated tools. Conversely, the computational
approach yields more insight into the strength and vulnerabilities of
protocols, but is difficult to apply and only accessible to a small
number of true experts in the field. Building on past success using
several automated tools, the project will devise tool-based methods that
leverage new scientific foundations.
This is a joint project with John Mitchell (Stanford),
Daniele Micciancio
(UCSD), and Andre
Scedrov (Univ. of Pennsylvania). It is supported by the NSF grant
CNS-0509033 (Oct 1, 2004 - Sep 30, 2009).
People (at UT Austin)
Alumni
-
Vishwas Bhat, MS (to Cisco)
-
Prateek Gupta, MS (to VMware)
-
Tim Wang, MS (to Amazon)
Publications (at UT Austin)
- E. Wong, P. Balasubramanian, L. Alvisi, M. Gouda, and V. Shmatikov.
Truth in Advertising:
Lightweight Verification of Route Integrity.
26th Annual ACM Symposium on Principles of
Distributed Computing (PODC),
2007.
- V. Shmatikov and M-H. Wang.
Secure Verification of Location Claims with Simultaneous
Distance Modification.
12th Annual Asian Computing Science Conference (ASIAN), 2007.
- P. Gupta and V. Shmatikov.
Security Analysis of Voice-over-IP Protocols.
20th IEEE Computer Security Foundations Symposium (CSF),
2007.
- R. Chang and V. Shmatikov.
Formal Analysis of Authentication in Bluetooth Device Pairing.
LICS/ICALP Workshop on Foundations of
Computer Security and Automated Reasoning for Security Protocol
Analysis (FCS-ARSPA), 2007.
- A. Mahimkar, J. Dange, V. Shmatikov, H. Vin, and Y. Zhang.
dFence: Transparent Network-based Denial of Service Mitigation.
4th USENIX Symposium on Networked Systems Design and
Implementation (NSDI), 2007.
- V. Shmatikov and M-H. Wang.
Measuring Relationship Anonymity in Mix Networks.
5th ACM Workshop on Privacy in the Electronic Society
(WPES), 2006.
- V. Shmatikov and M-H. Wang.
Timing Analysis in Low-Latency Mix Networks: Attacks and Defenses.
11th European Symposium on Research in Computer Security
(ESORICS), 2006.
- P. Gupta and V. Shmatikov.
Key Confirmation and Adaptive Corruptions in the Protocol Security
Logic.
Extended abstract in FLOC Joint Workshop on Foundations of
Computer Security and Automated Reasoning for Security Protocol
Analysis (FCS-ARSPA), 2006.
- A. Narayanan and V. Shmatikov.
Fast Dictionary Attacks on Passwords Using Time-Space Tradeoff.
12th ACM Conference on Computer and Communications Security
(CCS), 2005.
- P. Gupta and V. Shmatikov.
Towards Computationally Sound Symbolic Analysis of Key Exchange
Protocols.
Extended abstract in 3rd ACM Workshop on Formal Methods in
Security Engineering (FMSE), 2005.
- A. Datta, A. Derek, J.C. Mitchell, V. Shmatikov, and M. Turuani.
Probabilistic Polynomial-Time Semantics for a Protocol Security
Logic. 32nd International Colloquium on Automata,
Languages and Programming (ICALP), 2005.
- A. Mahimkar and V. Shmatikov.
Game-Based Analysis of Denial-of-Service Prevention Protocols.
18th IEEE Computer Security Foundations Workshop (CFSW), 2005.
Contact: shmat AT cs DOT utexas DOT edu