Computer Sciences Dept.

Computer Security and CryptographyReading Group
March 2004 List

Date &
Location
Reading
1 Mar. 2004
1304 CS
2:30 - 3:30 PM
Nevin Heintze, Jon G. Riecke
Bell Labs, Murray Hill
The SLam Calculus: Programming with Secrecy and Integrity
Published in POPL'98

URL: http://citeseer.nj.nec.com/heintze98slam.html

The SLam calculus is a typed λ-calculus that maintains security information as well as type information. The type system propagates security information for each object in four forms: the object's creators and readers, and the object's indirect creators and readers (i.e., those agents who, through flow-of-control or the actions of other agents, can influence or be influenced by the content of the object). We prove that the type system prevents security violations and give some examples of its power.

8 Mar. 2004
3331 CS 2:30 - 3:30 PM
Matt Blaze
AT&T Labs
Rights Amplification in Master-Keyed Mechanical Locks
Published in IEEE Security & Privacy, March/April 2003

URL: http://www.crypto.com/papers/mk.pdf

This paper examines mechanical lock security from the perspective of computer science and cryptology. We focus on new and practical attacks for amplifying rights in mechanical pin tumbler locks. Given access to a single master-keyed lock and its associated key, a procedure is given that allows discovery and creation of a working master key for the system. No special skill or equipment, beyond a small number of blank keys and a metal file, is required, and the attacker need engage in no suspicious behavior at the lock's location. Countermeasures are also described that may provide limited protection under certain circumstances. We conclude with directions for research in this area and the suggestion that mechanical locks are worthy objects for study and scrutiny.

15 Mar. 2004
3331 CS 2:30 - 3:30 PM
John C. Mitchell, Vitaly Shmatikov, Ulrich Stern
Stanford
Finite-State Analysis of SSL 3.0
Published in 7th USENIX Security Symposium (1998), San Antonio, Texas

URL: http://www.usenix.org/publications/library/proceedings/sec98/mitchell.html

The Secure Sockets Layer (SSL) protocol is analyzed using a finite-state enumeration tool called Murφ. The analysis is presented using a sequence of incremental approximations to the SSL 3.0 handshake protocol. Each simplified protocol is ``model-checked'' using Murφ, with the next protocol in the sequence obtained by correcting errors that Murφ finds automatically. This process identifies the main shortcomings in SSL 2.0 that led to the design of SSL 3.0, as well as a few anomalies in the protocol that is used to resume a session in SSL 3.0. In addition to some insight into SSL, this study demonstrates the feasibility of using formal methods to analyze commercial protocols.

24 Mar. 2004
5331 CS 11:30 AM - 12:30 PM
Steven M. Bellovin
AT&T Labs, Murray Hill
Security Problems in the TCP/IP Protocol Suite
Published in ACM SIGCOMM Computer Communications Review, April 1989

URL: http://www.research.att.com/~smb/papers/ipext.pdf

The TCP/IP protocol suite, which is very widely used today, was developed under the sponsorship of the Department of Defense. Despite that, there are a number of serious security flaws inherent in the protocols, regardless of the correctness of any implementations. We describe a variety of attacks based on these flaws, including sequence number spoofing, routing attacks, source address spoofing, and authentication attacks. We also present defenses against these attacks, and conclude with a discussion of broad-spectrum defenses such as encryption.

31 Mar. 2004
5331 CS 11:30 AM - 12:30 PM
A. Yaar, A. Perrig, D. Song
CMU
Pi: A Path Identification Mechanism to Defend against DDoS Attacks
Published in Oakland'03

URL: http://www.ece.cmu.edu/~adrian/projects/pi.pdf

Distributed Denial of Service (DDoS) attacks continue to plague the Internet. Defense against these attacks is complicated by spoofed source IP addresses, which make it difficult to determine a packet's true origin. We propose Pi (short for Path Identifier), a new packet marking approach in which a path fingerprint is embedded in each packet, enabling a victim to identify packets traversing the same paths through the Internet on a per packet basis, regardless of source IP address spoofing.

Pi features many unique properties. It is a per-packet deterministic mechanism: each packet traveling along the same path carries the same identifier. This allows the victim to take a proactive role in defending against a DDoS attack by using the Pi mark to filter out packets matching the attackers' identifiers on a per packet basis. The Pi scheme performs well under large-scale DDoS attacks consisting of thousands of attackers, and is effective even when only half the routers in the Internet participate in packet marking. Pi marking and filtering are both extremely light-weight and require negligible state.

We use traceroute maps of real Internet topologies (e.g., CAIDA's Skitter and Burch and Cheswick's Internet Map) to simulate DDoS attacks and validate our design.


< Back to the Sec & Crypto reading group page
Created and maintained by Mihai Christodorescu (http://www.cs.wisc.edu/~mihai)
Created: Wed Aug 13 10:30:10 CDT 2003
Last modified: Thu Apr 01 10:29:26 CDT 2004
 
Computer Science | UW Home