Keywords

Security protocols, authentication, 802.11i, strand space system, multi-agent model

Abstract

The security objectives enforce the security policy, which defines what is to be protected in a network environment. The violation of these security objectives induces security threats. We introduce an explicit notion of security objectives for a security protocol. This notion should precede the formal verification process. In the absence of such a notion, the security protocol may be proven correct despite the fact that it is not equipped to defend against all potential threats. In order to establish the correctness of security objectives, we present a formal model that provides basis for the formal verification of security protocols. We also develop the modal logic, proof based, and multi-agent approaches using the Strand Space framework. In our modal logic approach, we present the logical constructs to model a protocol's behavior in such a way that the participants can verify different security parameters by looking at their own run of the protocol. In our proof based model, we present a generic set of proofs to establish the correctness of a security protocol. We model the 802.11i protocol into our proof based system and then perform the formal verification of the authentication property. The intruder in our model is imbued with powerful capabilities and repercussions to possible attacks are evaluated. Our analysis proves that the authentication of 802.11i is not compromised in the presented model. We further demonstrate how changes in our model will yield a successful man-in-the-middle attack. Our multi-agent approach includes an explicit notion of multi-agent, which was missing in the Strand Space framework. The limitation of Strand Space framework is the assumption that all the information available to a principal is either supplied initially or is contained in messages received by that principal. However, other important information may also be available to a principal in a security setting, such as a principal may combine information from different roles played by him in a protocol to launch a powerful attack. Our presented approach models the behavior of a distributed system as a multi-agent system. The presented model captures the combined information, the formal model of knowledge, and the belief of agents over time. After building this formal model, we present a formal proof of authentication of the 4-way handshake of the 802.11i protocol.

Notes

If this is your thesis or dissertation, and want to learn how to access it or for more information about readership statistics, contact us at STARS@ucf.edu

Graduation Date

2007

Semester

Summer

Advisor

Guha, Ratan

Degree

Doctor of Philosophy (Ph.D.)

College

College of Engineering and Computer Science

Department

Electrical Engineering and Computer Science

Degree Program

Computer Science

Format

application/pdf

Identifier

CFE0001801

URL

http://purl.fcla.edu/fcla/etd/CFE0001801

Language

English

Release Date

July 2008

Length of Campus-only Access

None

Access Status

Doctoral Dissertation (Open Access)

Download

Share

COinS