國立高雄大學圖資館 |

Language: English

Back

Operational semantics and verificati...

Cremers, Cas.

Operational semantics and verification of security protocols

Record Type:	Electronic resources : Monograph/item
Title/Author:	Operational semantics and verification of security protocolsby Cas Cremers, Sjouke Mauw.
Author:	Cremers, Cas.
other author:	Mauw, Sjouke.
Published:	Berlin, Heidelberg :Springer Berlin Heidelberg :2012.
Description:	xiii, 172 p. :ill., digital ;24 cm.
Contained By:	Springer eBooks
Subject:	Computer security.
Online resource:	http://dx.doi.org/10.1007/978-3-540-78636-8
ISBN:	9783540786368 (electronic bk.)

Operational semantics and verification of security protocols
Cremers, Cas.

Operational semantics and verification of security protocols[electronic resource] /by Cas Cremers, Sjouke Mauw. - Berlin, Heidelberg :Springer Berlin Heidelberg :2012. - xiii, 172 p. :ill., digital ;24 cm. - Information security and cryptography,1619-7100. - Information security and cryptography..

Introduction -- Preliminaries -- Operational Semantics -- Security Properties -- Verification -- Multiprotocol Attacks -- Generalizing NSL for Multiparty Authentication -- Related Work -- Conclusions and Future Work -- Index.

Security protocols are widely used to ensure secure communications over insecure networks, such as the internet or airwaves. These protocols use strong cryptography to prevent intruders from reading or modifying the messages. However, using cryptography is not enough to ensure their correctness. Combined with their typical small size, which suggests that one could easily assess their correctness, this often results in incorrectly designed protocols.The authors present a methodology for formally describing security protocols and their environment. This methodology includes a model for describing protocols, their execution model, and the intruder model. The models are extended with a number of well-defined security properties, which capture the notions of correct protocols, and secrecy of data. The methodology can be used to prove that protocols satisfy these properties. Based on the model they have developed a tool set called Scyther that can automatically find attacks on security protocols or prove their correctness. In case studies they show the application of the methodology as well as the effectiveness of the analysis tool.The methodology’s strong mathematical basis, the strong separation of concerns in the model, and the accompanying tool set make it ideally suited both for researchers and graduate students of information security or formal methods and for advanced professionals designing critical security protocols.

ISBN: 9783540786368 (electronic bk.)Subjects--Topical Terms:

184416
Computer security.

LC Class. No.: QA76.9.A25 / C74 2012

Dewey Class. No.: 005.8

Operational semantics and verification of security protocols
LDR:02595nmm a2200289 a 4500 001 353041
003 DE-He213
005 20121121152325.0
006 m d
007 cr nn 008maaau
008 121218s2012 gw s 0 eng d
020 $a 9783540786368 (electronic bk.)
020 $a 9783540786351 (paper)
035 $a 978-3-540-78636-8
040 $a GP $c GP
041 0 $a eng
050 4 $a QA76.9.A25 $b C74 2012
082 0 4 $a 005.8 $2 23
090 $a QA76.9.A25 $b C915 2012
100 1 $a Cremers, Cas. $3 585057
245 1 0 $a Operational semantics and verification of security protocols $h [electronic resource] / $c by Cas Cremers, Sjouke Mauw.
260 $a Berlin, Heidelberg : $b Springer Berlin Heidelberg : $b Imprint: Springer, $c 2012.
300 $a xiii, 172 p. : $b ill., digital ; $c 24 cm.
490 1 $a Information security and cryptography, $x 1619-7100
505 0 $a Introduction -- Preliminaries -- Operational Semantics -- Security Properties -- Verification -- Multiprotocol Attacks -- Generalizing NSL for Multiparty Authentication -- Related Work -- Conclusions and Future Work -- Index.
520 $a Security protocols are widely used to ensure secure communications over insecure networks, such as the internet or airwaves. These protocols use strong cryptography to prevent intruders from reading or modifying the messages. However, using cryptography is not enough to ensure their correctness. Combined with their typical small size, which suggests that one could easily assess their correctness, this often results in incorrectly designed protocols.The authors present a methodology for formally describing security protocols and their environment. This methodology includes a model for describing protocols, their execution model, and the intruder model. The models are extended with a number of well-defined security properties, which capture the notions of correct protocols, and secrecy of data. The methodology can be used to prove that protocols satisfy these properties. Based on the model they have developed a tool set called Scyther that can automatically find attacks on security protocols or prove their correctness. In case studies they show the application of the methodology as well as the effectiveness of the analysis tool.The methodology’s strong mathematical basis, the strong separation of concerns in the model, and the accompanying tool set make it ideally suited both for researchers and graduate students of information security or formal methods and for advanced professionals designing critical security protocols.
650 0 $a Computer security. $3 184416
650 0 $a Computer networks $x Security measures. $3 185597
650 0 $a Semantic computing. $3 384598
650 1 4 $a Computer Science. $3 212513
650 2 4 $a Data Structures, Cryptology and Information Theory. $3 273993
650 2 4 $a Computer Systems Organization and Communication Networks. $3 273709
650 2 4 $a Software Engineering/Programming and Operating Systems. $3 273711
700 1 $a Mauw, Sjouke. $3 283930
710 2 $a SpringerLink (Online service) $3 273601
773 0 $t Springer eBooks
830 0 $a Information security and cryptography. $3 567250
856 4 0 $u http://dx.doi.org/10.1007/978-3-540-78636-8
950 $a Computer Science (Springer-11645)