1. Nathan
Marz, Raylene Yung - BitTorrent:
We used the probabilistic model checker PRISM to analyze the BitTorrent protocol. Our attacker model does not have control over the network and instead finds attacks based on forging messages. We used PHP to generate our PRISM models since they are quite large. As a result, we discovered many interesting higher-level techniques for constructing probabilistic models and dealing with non-determinism. Our model exceeded the limitations of PRISM, but through the process of modeling BitTorrent in detail, we found several security weaknesses. Finally we propose modifications to the protocol which solve these issues.
2. Andre
Encarnacao, Greg Bayer - Mobile IPv6 Binding Update - Return Routability
Procedure:
The Return Routability Procedure (RRP) attempts to provide basic authentication and integrity for Mobile IPv6 Binding Updates, without relying on Public Key Infrastructure (PKI). This project analyzes the RRP with the Murphi model checker and verifies protocol design decisions through a rational reconstruction approach. Two major attacks are discovered in the final version of the protocol and two solution ideas are discussed.
3. Chris
Brigham, Tom Wang - An Analysis of Fast Handover Key Distribution Using SEND in
In Mobile IPv6 with Fast Handover, a key is distributed to a mobile node from its access router prior to handover. We examine the security properties of this key distribution protocol using Murphi. By modeling the complete protocol and various decomposed versions, we determine that the SEND-based protocol proposed in the draft is both sufficient and necessary for a secure handover-key exchange.
4. John
Jersin, Jonathan Wheeler - Security Analysis of Bluetooth v2.1 + EDR Pairing
Authentication Protocol:
Bluetooth is designed for wireless communication between mobile devices. This paper provides a security analysis of the Bluetooth Version 2.1 + EDR pairing authentication protocol. An overview of how we modeled the security properties of Bluetooth using the Murphi verification tool is provided, followed by our findings and analysis. Three different types of attacks were confirmed: rollback attacks, brute force attacks, and a denial of service attack.
5. Ben
Newman, Shivaram Lingamneni - OpenID 2.0:
We used Murphi
to analyze the OpenID 2.0 protocol (http://openid.net/specs/openid-authentication-2_0.html)
for security vulnerabilities. We found one Cross-Site Request Forgery
(XSRF)
vulnerability that is an instance of a class of "session swapping"
attacks identified by Adam Barth. In this particular attack, the victim
is tricked into logging into a trusted site with the credentials of a malicious
party. Our model was general enough to capture this vulnerability, but
also limited enough that exploration of the state space terminates without
errors when this attack is suppressed. We hope that our design will be
helpful in future efforts to model XSRF attacks.
6. Matt
Bravo - Security During Handoffs in 802.16g-2007 (Management Plan Procedures
and Services):
The recent amendment to 802.16 of "Management Plane Procedures and Services" provides an opportunity to examine WiMAX security at the management level. We present an analysis of the procedures added to WiMAX in the 802.16g-2007 amendment, with emphasis on the exchange of subscriber cryptographic information of all devices. We find that in the interest of functionality, the 802.16g-2007 amendment defines procedures in the mobile handoff management section for requesting cryptographic information without verifying a base stations legitimate need for the keys. This leads to a real-time interception vulnerability in the network. We conclude with suggestions on how an implementation of WiMAX can protect against this vulnerability.
7. Anthony
Ho, Sharada Sundaram - A prolog based HIPAA online compliance auditor:
Our project consisted of a model of HIPAA using Prolog. We attempted to analyze the security properties of HIPAA as well as the efficacy of Prolog as a tool for modeling laws. Using our model of HIPAA, we discovered two flaws in the HIPAA law. We also discuss a number of insights on using Prolog as an analysis tool and law verifier obtained throughout the course of our project.
8. Lavina
Jain, Jayesh Vyas - Security Analysis of Remote Attestation:
Remote attestation is a method by which a host (client) authenticates its hardware and software configuration to a remote host (server). The goal of remote attestation is to enable a remote system (challenger) to determine the level of trust in the integrity of platform of another system (attestator). The architecture for remote attestation consists of two major components: Integrity measurement architecture and remote attestation protocol. The remote attestation protocol proposed by IBM is vulnerable to Man-In-The-Middle attack. We propose a modified version of the protocol that is secure. We have implemented a model of our proposed protocol on Murphi to analyse the security properties of the protocol. This report describes the design of our protocol and its analysis using Murphi. We conclude that our proposed protocol is secure under certain assumptions of trust and can be used for remote attestation.
9. Sudip
Regmi, Ilya Pirkin - Analysis of Direct Anonymous Attestation (DAA) Protocol
using Murphi:
In this project,
we modeled and analyzed the security properties of the Direct Anonymous Protocol
[1] using Murphi. We simplified the protocol model using security primitives
which we
considered
unbreakable and modeled our abstractions in Murphi. Running simulations in
Murphi, we were able to confirm several known attacks in the protocol explained
in [2] and [3]. In
addition, the model uncovered an issue with cross-site verifications.
10. Fred Wulff - Analyzing
the Pynchon Gate Protocol:
I analyzed the Pynchon Gate Protocol, a pseudonymous mail reply handling protocol introduced by Sassaman, Coen, and Mathewson, and in particular BitTorrent's suitability for it's purpose within that protocol. After an unfulfilling attempt at using PRISM, I wrote a BitTorrent simulator and used that to verify the feasibility of an attack delaying the distribution of the mail and possibly removing anonymity. I also detail an attack I found during the process of codifying the protocol for PRISM centered on spamming.