Increasingly, goods and services are purchased over the Internet without any form of physical currency. This practice, often called e-commerce, offers sellers and buyers a convenient way to trade globally as no physical currency must change hands and buyers from anywhere in the world can browse online store fronts from around the globe. Nevertheless, many transactions still require a physical presence. For these sorts of transactions, a new technology called Near Field Communication has emerged to provide buyers with some of the conveniences of e-commerce while still allowing them to purchase goods locally. Near Field Communication (NFC), an evolution of Radio-Frequency Identification (RFID), allows one electronic device to transmit short messages to another nearby device. A buyer can store his or her payment information on a tag and a cashier can retrieve that information with an appropriate reader. Advanced devices can store payment information for multiple credit and debit cards as well as gift cards and other credentials. By consolidating all of these payment forms into a single device, the buyer has fewer objects to carry with her. Further, proper implementation of such a device can offer increased security over plastic cards in the form of advanced encryption. Using a testing platform consisting of commercial, off-the-shelf components, this dissertation investigates the security of the NFC physical-layer protocols as well as the primary NFC security protocol, NFC-SEC. In addition, it analyzes a situation in which the NFC protocols appear to break, potentially compromising sensitive data. Finally, this dissertation provides a proof of security for the NFC-SEC-1 variation of NFC-SEC.

We address bootstrapping secure multicast in enterprise and public-safety settings. Our work is motivated by the fact that secure multicast has important applications in such settings, and that the application setting significantly influences the design of security systems and protocols. This document presents and analyzes two designs for the composition of the authentication protocol, Kerberos, and the key transport protocol, Multimedia Internet KEYing (MIKEY). The two designs are denoted to be KM1 and KM2 . The main aspect in which the objective impacts the design is the assumption of an additional trusted third party (called a Key Server) that is the final arbiter on whether a principal is authorized to receive a key. Secure composition can be a challenge, and therefore the designs were kept to be simple so they have intuitive appeal. Notwithstanding this, it was recognized that even simple, seemingly secure protocols can have flaws. Two main security properties of interest called safety and avail- ability were articulated. A rigorous analysis of KM1 and KM2 was conducted using Protocol Composition Logic (PCL), a symbolic approach to analyzing security protocols, to show that the designs have those properties. The value of the analysis is demonstrated by a possible weakness in KM1 that was discovered which lead to the design of KM2 . A prototype of KM1 and KM2 was implemented starting with the publicly available reference implementation of Kerberos, and an open-source implementation of MIKEY. This document also discusses the experience from the implementation, and present empirical results which demonstrate the inherent trade-off between security and performance in the design of KM1 and KM2 .

We address bootstrapping secure multicast in enterprise and public-safety settings. Our work is motivated by the fact that secure multicast has important applications in such settings, and that the application setting significantly influences the design of security systems and protocols. This document presents and analyzes two designs for the composition of the authentication protocol, Kerberos, and the key transport protocol, Multimedia Internet KEYing (MIKEY). The two designs are denoted to be KM1 and KM2 . The main aspect in which the objective impacts the design is the assumption of an additional trusted third party (called a Key Server) that is the final arbiter on whether a principal is authorized to receive a key. Secure composition can be a challenge, and therefore the designs were kept to be simple so they have intuitive appeal. Notwithstanding this, it was recognized that even simple, seemingly secure protocols can have flaws. Two main security properties of interest called safety and avail- ability were articulated. A rigorous analysis of KM1 and KM2 was conducted using Protocol Composition Logic (PCL), a symbolic approach to analyzing security protocols, to show that the designs have those properties. The value of the analysis is demonstrated by a possible weakness in KM1 that was discovered which lead to the design of KM2 . A prototype of KM1 and KM2 was implemented starting with the publicly available reference implementation of Kerberos, and an open-source implementation of MIKEY. This document also discusses the experience from the implementation, and present empirical results which demonstrate the inherent trade-off between security and performance in the design of KM1 and KM2 .