Modeling and Analyzing Security Protocols with Tamarin: A Comprehensive Guide
暫譯: 使用 Tamarin 建模與分析安全協議：全面指南
Basin, David, Cremers, Cas, Dreier, Jannik
- 出版商: Springer
- 出版日期: 2025-07-28
- 售價: $2,490
- 貴賓價: 9.5 折 $2,366
- 語言: 英文
- 頁數: 325
- 裝訂: Hardcover - also called cloth, retail trade, or trade
- ISBN: 3031909356
- ISBN-13: 9783031909351
-
相關分類:
Penetration-test
海外代購書籍(需單獨結帳)
相關主題
商品描述
The Tamarin prover is an open-source analysis tool for cryptographic protocols. Given a specification of a protocol, possible adversaries, and the desired security properties, Tamarin either verifies the protocol or provides counter examples witnessing attacks. Tamarin is a robust and powerful analysis tool: it has been under development for over a decade and has reached a state of maturity where it can be applied to model and analyze a wide range of real-world cryptographic protocols. It is now one of the leading tools in this domain, with a wide and active user community spanning both academia and industry.
The objective of this book is to help both researchers and practitioners to gain a general understanding of how Formal Methods tools like Tamarin can be used to analyze and improve the quality of real-world protocols. Moreover, we specifically showcase the Tamarin prover and provide guidance on its usage. In this sense, this book provides a user's manual forTamarin. But it goes far beyond that, highlighting Tamarin's underlying theory and its use in modeling and applications.
商品描述(中文翻譯)
Tamarin prover 是一個開源的加密協議分析工具。給定一個協議的規範、可能的對手以及所需的安全性屬性，Tamarin 要麼驗證該協議，要麼提供反例以證明攻擊的存在。Tamarin 是一個穩健且強大的分析工具：它已經開發超過十年，並達到了可以應用於建模和分析各種現實世界加密協議的成熟狀態。它現在是這一領域的領先工具之一，擁有一個廣泛且活躍的用戶社群，涵蓋學術界和業界。
本書的目標是幫助研究人員和實務工作者對如何使用像 Tamarin 這樣的形式方法工具來分析和改善現實世界協議的質量有一個一般性的理解。此外，我們特別展示 Tamarin prover 並提供其使用指南。在這個意義上，本書提供了 Tamarin 的用戶手冊。但它的內容遠不止於此，還強調了 Tamarin 的基本理論及其在建模和應用中的使用。
作者簡介
David Basin is a professor in the Department of Computer Science, ETH Zurich since 2003, where he heads the Information Security Group. His research focuses on Information Security, in particular on foundations, methods, and tools for modeling, building, and validating secure and reliable systems. He is Editor-in-Chief of Springer-Verlag's book series on Information Security and Cryptography and, from 2015 - 2020, of ACM Transactions on Privacy and Security. He is also the founding director of ZISC, the Zurich Information Security Center, which he led from 2003-2011. He is a Fellow of the ACM and of the IEEE.
Cas Cremers is a faculty member at the CISPA Helmholtz Center for Information Security in Saarbruecken, Germany, and honorary professor at Saarland University. From 2006 - 2013 he was a postdoctoral researcher, and senior researcher and lecturer, at ETH Zurich. In 2013 he joined the University of Oxford as an Associate Professor, becoming full Professor in 2015. In 2018 he joined CISPA. His work includes co-developing the Scyther and Tamarin tools, and contributing to the TLS and MLS standards of the IETF. His research focuses on formal methods, applied cryptography, and foundations for secure communications.
Jannik Dreier is an associate professor at the Université de Lorraine in Nancy, France. He studied computer science at Karlsruhe Institute of Technology and ENSIMAG, Grenoble, and completed a PhD in computer science at the University Grenoble Alpes in 2013. He then was a postdoctoral researcher at ETH Zurich until 2015. Since 2021, he has been co-chairing the working group on formal methods for security of the CNRS research network on IT security. His research focuses on the design and analysis of cryptographic protocols, for example for electronic voting, using rigorous methods and automated tools.
Ralf Sasse is a senior scientist and lecturer at the Department of Computer Science at ETH Zurich. He received his M.Sc. degree in computer science from Karlsruhe Institute of Technology in 2005, and his Ph.D. in computer science from the University of Illinois at Urbana-Champaign in 2012. His research focuses on the theory and practice of cryptographic security protocol verification, and particularly on developing tools that assist in this task. Recent work applied this to 5G mobile communication and EMV payment card security.
作者簡介(中文翻譯)
David Basin 自2003年以來擔任蘇黎世聯邦理工學院（ETH Zurich）計算機科學系的教授，並負責資訊安全組。他的研究專注於資訊安全，特別是建模、構建和驗證安全可靠系統的基礎、方法和工具。他是Springer-Verlag資訊安全與密碼學書系的主編，並於2015年至2020年擔任ACM《隱私與安全交易》的主編。他也是蘇黎世資訊安全中心（ZISC）的創始主任，並於2003年至2011年期間領導該中心。他是ACM和IEEE的會士。
Cas Cremers 是德國薩爾布呂肯CISPA亥姆霍茲資訊安全中心的教職員，並擔任薩爾蘭大學的名譽教授。從2006年至2013年，他在ETH Zurich擔任博士後研究員、高級研究員和講師。2013年，他加入牛津大學擔任副教授，並於2015年晉升為正教授。2018年，他加入CISPA。他的工作包括共同開發Scyther和Tamarin工具，並為IETF的TLS和MLS標準做出貢獻。他的研究專注於形式方法、應用密碼學和安全通信的基礎。
Jannik Dreier 是法國南錫洛林大學的副教授。他在卡爾斯魯厄理工學院和格勒諾布爾的ENSIMAG學習計算機科學，並於2013年在格勒諾布爾阿爾卑斯大學獲得計算機科學博士學位。隨後，他在ETH Zurich擔任博士後研究員，直到2015年。自2021年以來，他一直共同主持CNRS資訊安全研究網絡的安全形式方法工作組。他的研究專注於加密協議的設計和分析，例如使用嚴謹的方法和自動化工具進行電子投票。
Ralf Sasse 是ETH Zurich計算機科學系的高級科學家和講師。他於2005年在卡爾斯魯厄理工學院獲得計算機科學碩士學位，並於2012年在伊利諾伊大學香檳分校獲得計算機科學博士學位。他的研究專注於密碼安全協議驗證的理論和實踐，特別是開發協助此任務的工具。最近的工作將此應用於5G行動通信和EMV支付卡安全。
