Reasoning about recognizability in security protocols

1 online resource (155 pages) : PDF

2012

University of North Carolina at Charlotte

Although verifying a message has long been recognized as an important concept, which has been used explicitly or implicitly in security protocol analysis, there is no consensus on its exact meaning. Such a lack of formal treatment of the concept makes it extremely difficult to evaluate the vulnerability of security protocols.This dissertation offers a precise answer to the question: What is meant by saying that a message can be ``verified''? The core technical innovation is a third notion of knowledge in security protocols --- recognizability. It can be considered as intermediate between deduction and static equivalence, two classical knowledge notions in security protocols. We believe that the notion of recognizability sheds important lights on the study of security protocols. More specifically, this thesis makes four contributions.First, we develop a knowledge model to capture an agent's cognitive ability to understand messages. Thanks to a clear distinction between de re/dicto interpretations of a message, the knowledge model unifies both computational and symbolic views of cryptography gracefully.Second, we propose a new notion of knowledge in security protocols --- recognizability --- to fully capture one's ability or inability to cope with potentially ambiguous messages. A terminating procedure is given to decide recognizability under the standard Dolev-Yao model. Third, we establish a faithful view of the attacker based on recognizability. This yields new insights into protocol compilations and protocol implementations. Specifically, we identify two types of attacks that can be thawed through adjusting the protocol implementation; and show that an ideal implementation that corresponds to the intended protocol semantics does not always exist. Overall, the obtained attacker's view provides a path to more secure protocol designs and implementations.Fourth, we use recognizability to provide a new perspective on type-flaw attacks. Unlike most previous approaches that have focused on heuristic schemes to detect or prevent type-flaw attacks, our approach exposes the enabling factors of such attacks. Similarly, we apply the notion of recognizability to analyze off-line guessing attacks. Without enumerating rules to determine whether a guess can be ``verified'', we derive a new definition based on recognizability to fully capture the attacker's guessing capabilities. This definition offers a general framework to reason about guessing attacks in a symbolic setting, independent of specific intruder models. We show how the framework can be used to analyze both passive and active guessing attacks.

doctoral dissertations

Computer science

Ph.D.

Information Technology

Wang, Weichao

Wu, Xintao
Shehab, Mohamed
Lu, Aidong
Brown, Mary

Thesis (Ph.D.)--University of North Carolina at Charlotte, 2012.

This Item is protected by copyright and/or related rights. You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s). For additional information, see http://rightsstatements.org/page/InC/1.0/.

Copyright is held by the author unless otherwise indicated.

Li_uncc_0694D_10394

http://hdl.handle.net/20.500.13093/etd:1209