國立高雄大學圖資館 |

Language: English

Back

Security analysis of network protoco...

Datta, Anupam.

Security analysis of network protocols: Compositional reasoning and complexity-theoretic foundations.

Record Type:	Electronic resources : Monograph/item
Title/Author:	Security analysis of network protocols: Compositional reasoning and complexity-theoretic foundations.
Author:	Datta, Anupam.
Description:	156 p.
Notes:	Adviser: John C. Mitchell.
Notes:	Source: Dissertation Abstracts International, Volume: 66-08, Section: B, page: 4315.
Contained By:	Dissertation Abstracts International66-08B.
Subject:	Computer Science.
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3187280
ISBN:	9780542294983

Security analysis of network protocols: Compositional reasoning and complexity-theoretic foundations.
Datta, Anupam.

Security analysis of network protocols: Compositional reasoning and complexity-theoretic foundations. - 156 p.

Adviser: John C. Mitchell.

Thesis (Ph.D.)--Stanford University, 2005.

The final result in the dissertation spans both the problems. An alternative way of specifying and reasoning about protocol composition is through simulation between the real protocol and an ideal protocol, which is secure by construction. We prove that, under reasonable assumptions about the communication model, three simulation-based definitions for protocol security: universal composability, black-box simulatability, and process observational equivalence, express the same properties of a protocol. The proofs are axiomatic and are carried out using process calculus equational principles.

ISBN: 9780542294983Subjects--Topical Terms:

212513
Computer Science.

Security analysis of network protocols: Compositional reasoning and complexity-theoretic foundations.
LDR:03492nmm _2200277 _450 001 170839
005 20061228142259.5
008 090528s2005 eng d
020 $a 9780542294983
035 $a 00242869
040 $a UnM $c UnM
100 0 $a Datta, Anupam. $3 244870
245 1 0 $a Security analysis of network protocols: Compositional reasoning and complexity-theoretic foundations.
300 $a 156 p.
500 $a Adviser: John C. Mitchell.
500 $a Source: Dissertation Abstracts International, Volume: 66-08, Section: B, page: 4315.
502 $a Thesis (Ph.D.)--Stanford University, 2005.
520 # $a The final result in the dissertation spans both the problems. An alternative way of specifying and reasoning about protocol composition is through simulation between the real protocol and an ideal protocol, which is secure by construction. We prove that, under reasonable assumptions about the communication model, three simulation-based definitions for protocol security: universal composability, black-box simulatability, and process observational equivalence, express the same properties of a protocol. The proofs are axiomatic and are carried out using process calculus equational principles.
520 # $a The second problem pertains to the computational soundness of symbolic protocol analysis. At a high-level, this means that a logical method for protocol analysis should have an associated soundness theorem, which guarantees that a completely symbolic proof has an interpretation in the standard complexity-theoretic model of modern cryptography. Our approach to this problem involves defining complexity-theoretic semantics and proving a soundness theorem for a variant of PCL, which we call Computational PCL.
520 # $a This dissertation addresses two central problems associated with the design and security analysis of network protocols that use cryptographic primitives. The first is the protocol composition problem. The goal here is to develop methods for proving properties of complex protocols by combining independent proofs of their parts. In order to address this problem, we have developed a framework consisting of two formal systems: Protocol Derivation System (PDS) and Protocol Composition Logic (PCL). PDS supports syntactic derivations of complex protocols, starting from basic components, and combining or extending them using a sequence of composition, refinement, and transformation operations. PCL is a Floyd-Hoare style logic that supports axiomatic proofs of protocol properties. The eventual goal is to develop proof methods for PCL for every derivation operation in PDS, thereby enabling the parallel development of protocols and their security proofs. In this dissertation, we present proof methods for reasoning about protocol composition and a class of protocol refinements. The composition theorems are formulated and proved by adapting ideas from the assume-guarantee paradigm for reasoning about distributed systems. PDS and PCL have been successfully applied to a number of industrial network security protocols, in several instances identifying serious security vulnerabilities.
590 $a School code: 0212.
650 # 0 $a Computer Science. $3 212513
690 $a 0984
710 0 # $a Stanford University. $3 212607
773 0 # $g 66-08B. $t Dissertation Abstracts International
790 $a 0212
790 1 0 $a Mitchell, John C., $e advisor
791 $a Ph.D.
792 $a 2005
856 4 0 $u http://libsw.nuk.edu.tw:81/login?url=http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3187280 $z http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3187280