logo资料库

形式化分析工具Scyther软件的说明手册.pdf

发布时间：2022-06-06 发布人：admin 分类：说明书 资料大小：0.37M 资料格式：pdf 举报 版权申诉
第1页 / 共52页
第2页 / 共52页
第3页 / 共52页
第4页 / 共52页
第5页 / 共52页
第6页 / 共52页
第7页 / 共52页
第8页 / 共52页
资料共52页，剩余部分请下载后查看
    Cas Cremers Scyther User Manual Draft February 18, 2014
    2
    Contents 1 Introduction 2 Background 3 Installation 4 Quick start tutorial 5 Input Language 5.1 A minimal input file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2.1 Atomic terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2.2 Pairing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2.3 Symmetric keys . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2.4 Asymmetric keys . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2.5 Hash functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2.6 Predefined types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2.7 Usertypes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3 Events . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3.1 Receive and send events . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3.2 Claim events and Security properties . . . . . . . . . . . . . . . . . . . . . 5.3.3 Internal computation/pattern match events . . . . . . . . . . . . . . . . . 5.4 Role definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.5 Protocol definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.6 Global declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.7 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.7.1 Macro . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.7.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.7.3 5.8 Language BNF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Input file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.8.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.8.2 Protocols 5.8.3 Roles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.8.4 Events . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.8.5 Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.8.6 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Include one-role-per-agent 3 5 7 9 11 15 15 15 15 16 16 17 17 17 17 18 18 18 19 20 20 21 21 21 22 23 23 23 23 23 24 24 24
    4 CONTENTS 6 Modeling security protocols 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.2 Example: Needham-Schroeder Public Key . . . . . . . . . . . . . . . . . . . . . . 7 Specifying security properties 7.1 Specifying secrecy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.2 Specifying authentication properties . . . . . . . . . . . . . . . . . . . . . . . . . 7.2.1 Aliveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.2.2 Non-injective synchronisation . . . . . . . . . . . . . . . . . . . . . . . . . 7.2.3 Non-injective agreement . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.2.4 Agreement over data . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Using the Scyther tool GUI 8.1 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8.2 Bounding the statespace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8.3 Attack graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8.3.1 Runs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8.3.2 Communication events . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8.3.3 Claims . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Using the Scyther command-line tools 10 Advanced topics 10.1 Modeling more than one asymmetric key pair . . . . . . . . . . . . . . . . . . . . 10.2 Approximating equational theories . . . . . . . . . . . . . . . . . . . . . . . . . . 10.3 Modeling time-stamps and global counters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10.4 Multi-protocol attacks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10.3.1 Modeling global counters 10.3.2 Modeling time-stamps using nonces 10.3.3 Modeling time-stamps using variables 11 Further reading A Full specification for Needham-Schroeder public key 25 25 25 29 29 29 29 29 29 29 31 31 33 33 33 35 36 37 39 39 39 41 41 41 42 42 45 49
    Chapter 1 Introduction Note: This is a draft of the new version of the Scyther manual. The manual may therefore be incomplete at points. Any feedback is welcome and can be sent to Cas Cremers by e-mail: cas.cremers@cs.ox.ac.uk. This is the user manual for the Scyther security protocol verification tool. The purpose of this manual is to explain the details of the Scyther input language, explain how to model basic protocols, and how to effectively use the Scyther tool. This manual does not detail the protocol execution model nor the adversary model used by the tool. It is therefore highly recommended to read the accompanying book [1]. The book includes a detailed description of Scyther’s underlying protocol model, security property specifications, and the algorithm. We proceed in the following way. Some background is given in Chapter 2. Chapter 3 explains how to install the Scyther tool on various platforms. In Chapter 4 we give a brief tutorial using simple examples to show the basics of the tool. Then we discuss things in more detail as we introduce the input language of the tool in Chapter 5. Modeling of basic protocols is described in Chapter 6, and Chapter 7 describes how to specify security properties. The usage of the GUI version of tool is then explained in more detail in Section 8. The underlying command-line tool is described in Section 9. Advanced topics are discussed in Section 10. Online information More help can be found online on the Scyther website: http://users.ox.ac.uk/~coml0529/scyther/index.html Users are advised to subscribe to the Scyther mailing list, whose details can also be found on the Scyther website. 5
    6 CHAPTER 1. INTRODUCTION
    Chapter 2 Background Scyther is a tool for the formal analysis of security protocols under the perfect cryptography assumption, in which it is assumed that all cryptographic functions are perfect: the adversary learns nothing from an encrypted message unless he knows the decryption key. The tool can be used to find problems that arise from the way the protocol is constructed. This problem is undecidable in general, but in practice many protocols can be either proven correct or attacks can be found. The full protocol model, its assumptions, the basic security properties, and the algorithm are described in [1]. This manual serves as a companion to the book. Thus, in this manual we assume the reader is familiar with the formal modeling of security protocols and their properties. 7
    8 CHAPTER 2. BACKGROUND
    分享到：
    赞 收藏

    相关推荐

    资料库

    安全技术

    共收录1285份资料，累计4个分类，关注成员有19位，主要包括：网络攻防,系统安全,其它,网络安全

    热门标签

    网络攻防 系统安全 其它 网络安全

    最新资料