Specification and verification of security protocols and their utilization in scenario-based requirements engineering / by Thorsten Koch ; supervised by: Prof. Dr. Eric Bodden. Paderborn, 2024
Inhalt
- Abstract
- Zusammenfassung
- Danksagung
- 1 Introduction
- 1.1 Problem Description
- 1.1.1 Specification and Analysis of Security Protocols
- 1.1.2 Specification and Analysis of Functional and Security Requirements
- 1.2 Contributions
- 1.3 Thesis Structure
- 2 Foundations
- 2.1 Modal Sequence Diagrams (MSDs)
- 2.1.1 Structure of MSD Specifications
- 2.1.2 Semantics of MSD Specifications
- 2.1.3 Analysis Techniques for MSD Specifications
- 2.1.4 The Modal Profile
- 2.2 Specification and Analysis of Security Protocols
- 3 Specification of Security MSDs
- 3.1 Contributions
- 3.2 Requirements on the Security Modeling Profile
- 3.3 Exemplary Application of the Security Modeling Profile
- 3.3.1 Modeling the Andrew Secure RPC Security Protocol
- 3.3.2 Modeling the Needham-Schroeder Public Key Security Protocol
- 3.3.3 Summarizing the Exemplary Application of the Security Modeling Profile
- 3.4 The Security Modeling Profile in Detail
- 3.4.1 Subprofile SecurityModelingProfile::ProtocolModeling
- 3.4.2 Subprofile SecurityModelingProfile::CryptographicKeyModeling
- 3.4.3 Subprofile SecurityModelingProfile::SecureElementModeling
- 3.4.4 Metamodel SecurityModelingProfile::SecurityAssignment
- 3.4.5 Metamodel SecurityModelingProfile::SecurityCondition
- 3.5 Extension of the Runtime Semantics to Support the Security Modeling Profile
- 3.6 Implementation
- 3.7 Evaluation
- 3.7.1 Case Study Context
- 3.7.2 Setting the Hypotheses
- 3.7.3 Validating the Hypotheses
- 3.7.4 Analyzing the Results
- 3.7.5 Threats to Validity
- 3.8 Related Work
- 3.9 Summary
- 4 Verification of Security MSDs
- 4.1 Contributions
- 4.2 Overview of the Model-Checking Approach for Verifying Security Protocols
- 4.3 Translation from MSDs to the VerificationModel
- 4.3.1 Overview of the Metamodel Verification
- 4.3.2 Translate an MSD Specification to the SecurityProtocolModel
- 4.3.3 Translate an MSD Specification to the QueryModel
- 4.4 Translation from the VerificationModel to Proverif input models
- 4.4.1 Overview of the Capabilities of Proverif in relation to the Security Modeling Profile
- 4.4.2 Translate the SecurityProtocolModel to Proverif
- 4.4.3 Translate the QueryModel to Proverif
- 4.5 Translation from the VerificationModel to Tamarin input models
- 4.5.1 Overview of the Capabilities of Tamarin in relation to the Security Modeling Profile
- 4.5.2 Translate the SecurityProtocolModel to Tamarin
- 4.5.3 Translate the QueryModel to Tamarin
- 4.6 Back-Translation from Security Model Checkers to MSDs
- 4.6.1 Overview of the Metamodel Result
- 4.6.2 Translate the Analysis Results to the Security Modeling Profile
- 4.7 Implementation
- 4.8 Evaluation
- 4.8.1 Case Study Context
- 4.8.2 Setting the Hypotheses
- 4.8.3 Validating the Hypotheses
- 4.8.4 Analyzing the Results
- 4.8.5 Threats to Validity
- 4.9 Related Work
- 4.9.1 Model-based approaches for the automated verification of security protocols
- 4.9.2 Text-based approaches for the automated verification of security protocols
- 4.10 Summary
- 5 Incorporation of Functional and Security MSDs
- 5.1 Contributions
- 5.2 Exemplary Application of the Misuse Case Modeling Profile and the Security Protocol Template Profile
- 5.3 Specification of Misuse Cases
- 5.3.1 The Misuse Case Modeling Profile in Detail
- 5.3.2 Extension of the Runtime Semantics to Support the Misuse Case Modeling Profile
- 5.4 Integrating Security Protocols into Scenario-based Requirements Specifications
- 5.4.1 The Security Protocol Template Profile in Detail
- 5.4.2 Extension of the Runtime Semantics to Support the Security Protocol Template Profile
- 5.5 Implementation
- 5.6 Evaluation
- 5.6.1 Case Study Context
- 5.6.2 Setting the Hypotheses
- 5.6.3 Validating the Hypotheses
- 5.6.4 Analyzing the Results
- 5.6.5 Threats to Validity
- 5.7 Related Work
- 5.7.1 Approaches for the Identification and Analysis of Misuse Cases
- 5.7.2 Approaches for the Specification of Security Mechanisms
- 5.8 Summary
- 6 Conclusion
- Bibliography
- List of Figures
- List of Tables
- List of Listings
- List of Algorithms
- A Supplementing Materials for the Specification of Security MSDs
- A.1 Analyzing the Usage of Cryptographic Primitives in Security Protocols
- A.2 Analyzing the Usage of Algebraic Operations in Security Protocols
- A.3 Analyzing the Usage of Data Types in Security Protocols
- B Supplementing Materials for the Verification of Security MSDs
- B.1 Supplementing Materials for the Translation from MSDs to the VerificationModel
- B.1.1 Overview of the Package Verification::Protocol::Primitives
- B.1.2 Overview of the Package Verification::Protocol::Types
- B.2 Supplementing Materials for the Translation from the SecurityProtocolModel to Proverif
- B.3 Supplementing Materials for the Translation from the Security Protocol Model to Tamarin
- C Own Publication Contributions