Protocols, Strands, and Logic: Essays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday (Security and Cryptology)

This Festschrift was published in honor of Joshua Guttman on the occasion of his 66.66 birthday. The impact of his work is reflected in the 23 contributions enclosed in this volume. Joshua’s most influential and enduring contribution to the field has been the development of the strand space formalism for analyzing cryptographic protocols. It is one of several “symbolic approaches” to security protocol analysis in which the underlying details of cryptographic primitives are abstracted away, allowing a focus on potential flaws in the communication patterns between participants. His attention to the underlying logic of strand spaces has also allowed him to merge domain-specific reasoning about protocols with general purpose, first-order logical theories. The identification of clear principles in a domain paves the way to automated reasoning, and Joshua has been a leader in the development and distribution of several tools for security analysis. Preface Contents Securing Node-RED Applications 1 Introduction 2 Node-RED Vulnerabilities 2.1 Node-RED Platform 2.2 Platform-Level Isolation Vulnerabilities 2.3 Application-Level Context Vulnerabilities 3 Formalization 3.1 Language Syntax and Semantics 3.2 Security Condition and Enforcement 4 Related Work 5 Conclusion References Protocol Analysis with Time and Space 1 Introduction 1.1 Related Work 2 Two Time and Space Protocols 3 A Time and Space Process Algebra 3.1 New Syntax for Location 3.2 Time and Space Intruder Model 3.3 Time and Space Process Semantics 4 Time and Space Process Algebra into Untimed Process Algebra 5 Timed Process Algebra into Strands in Maude-NPA 6 Conclusions References Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer 1 Introduction 2 Background 2.1 Cryptographic Protocol Shapes Analyser 2.2 TLS 1.3 Pre Shared Key Authentication 2.3 Selfie Attack 3 Modeling TLS 1.3 PSK Authentication 3.1 Models of the TLS 1.3 PSK Authentication 3.2 Modeling the Proposed Fixes to the Selfie Attack 4 Discussion 5 Conclusions A Appendix References A Tutorial-Style Introduction to DY 1 Introduction 2 The DY Framework 3 The ISO-DH Protocol 4 Modeling ISO-DH in DY 5 Security Analysis 5.1 Forward Secrecy 5.2 Authentication Properties 6 Conclusion References Security Protocols as Choreographies 1 Introduction 2 The Envelope Protocol and Its Choreographic Description 3 Projection and Refinement 3.1 Projection 3.2 Refinement 4 Verification in Tamarin 5 Related Work 6 Conclusion References How to Explain Security Protocols to Your Children 1 Introduction 2 Storyboard 2.1 Our First Security Protocol 2.2 How the Postman Steals Isabelle's Cake 2.3 A Fix: Asymmetric Encryption 2.4 Denial of Service? 3 When it Gets Really Dark 3.1 Challenge and Respond 3.2 Man in the Middle Attack 3.3 A Countermeasure 4 A Practical Session 4.1 The Material 4.2 A Typical Session 4.3 Long-Term Variants of the Design-Attack Parts (advanced) 5 Conclusion: Have Fun! References Verifying a Blockchain-Based Remote Debugging Protocol for Bug Bounty 1 Introduction 2 Background: VeriOSS 2.1 Workflow Overview 2.2 Challenge-Response Interaction 2.3 Remote Debugging, and Challenge Generation and Solution 3 Protocol Encoding 4 Verification in ProVerif 5 Conclusion References Quantum Machine Learning and Fraud Detection 1 Introduction 2 Detecting Fraudulent Transactions 2.1 Support Vector Machines 2.2 Quantum Matrix Inversion and Probabilistic Abstract Interpretation 3 Quantum Machine Learning 3.1 Quantum Support Vector Machines 3.2 Quantum Support Vector Machines as PAI 4 Implementation of Quantum Fraud Detection 4.1 Experiments on the IBM Quantum Platform 5 Conclusion References Model Finding for Exploration 1 Introduction 2 Foundations 2.1 Homomorphism Orderings 3 Approaches to Model Finding 4 Three Principles for Model Finding Assistants 4.1 Fitness 4.2 Exploration of Individual Models 4.3 Completeness 5 Geometric Logic 6 Direct Model Finding Methods 6.1 Chase-Based Approaches 6.2 cpsa 7 Programming Against a Solver: Theory 7.1 Building Blocks 7.2 Minimization 7.3 Set of Support 8 Programming Against a Solver: Practice 8.1 Constructing HomTo and HomFrom for Arbitrary Homomorphisms 8.2 Constructing HomTo and HomFrom for Submodel Morphisms 8.3 Constructing homTo and homFrom for Injective Morphisms 9 Conclusion References Secure Key Management Policies in Strand Spaces 1 Introduction 2 Background and Related Work 2.1 The Strand Space Model 2.2 The CPSA Tool 2.3 Attacks on the PKCS#11 API 2.4 Related Work 3 Key Management Policies 4 Key Management APIs 4.1 An Untyped, Vulnerable API 4.2 A Secure, Typed API 4.3 Examples 5 Conclusion References A Declaration of Software Independence 1 Introduction 2 Formalizing Software Independence 2.1 Software Independence... of What? 2.2 Voting System and Its Software 2.3 Available Audits 3 Possibilistic Formulation of Software Independence 3.1 Basic Formulation 3.2 Relationship to End-to-End Verifiability 3.3 SI with Adaptive Audits 3.4 A Refinement 3.5 Software Resilience 3.6 Thought Experiment 3.7 Software Independence for Probabilistic Audits 4 Probabilistic/Game-Theoretic Definition 4.1 Terminology and Notation 4.2 Game-Theoretic Definition of SI 5 Conclusions References Formal Methods and Mathematical Intuition 1 Introduction 2 Formal Methods and Research at MITRE 3 Mathematical Intuition and Heuristics 4 Example: Development of Dimension Concepts and Dimension Theories 5 L. E. J. Brouwer's Breakthrough to Invariance of Dimension 6 Conclusion: Formal Methods, Mathematical Intuition, and Rigorous Mathematical Exposition References Establishing the Price of Privacy in Federated Data Trading 1 Introduction 2 Preliminaries 2.1 Differential Privacy 2.2 Shapley Value 3 Related Works 4 Differentially Private Data Trading Mechanism 4.1 Mechanism Outline 4.2 Earning Splitting 5 Experimental Results 5.1 Experimental Environments 5.2 Number of Rounds Needed for Data Collection 5.3 Number of Free Riders by Penalty Scheme 5.4 Reduced Shapley Value Computation Time 6 Conclusion A Proofs References On the Complexity of Verification of Time-Sensitive Distributed Systems 1 Introduction 2 Multiset Rewriting Systems 2.1 Progressing Timed Systems 3 Quantitative Temporal Properties 3.1 Critical Configurations and Compliant Traces 3.2 Time Sampling 3.3 Verification Problems 4 Relations Among Properties of Timed MSR 4.1 Relations Among Different Properties of Timed MSR and PTS 5 Complexity Results for PTSes 5.1 PSPACE-Completeness of Verification Problems for PTSes 6 Related and Future Work References Adapting Constraint Solving to Automatically Analyze UPI Protocols 1 Introduction 2 Background 3 Constraint Solving 4 CSolver 5 Modeling in the Constraint Solver 6 Representation of SMS 7 Implementation and Testing 8 Conclusion References Three Branches of Accountability 1 Introduction 2 The Agent Model 3 The Legislative Branch 4 The Executive Branch 5 The Judicial Branch 6 Security Based on Perfect Crimes 7 Løglog 8 Related Work and Conclusion References Benign Interaction of Security Domains 1 Introduction 2 Syntax 3 Local Security: Information Flow Type System 4 Global Security: Change of Security Domain 5 Taking Security Violations into Account 6 Conclusion A Semantics References Probabilistic Annotations for Protocol Models 1 Introduction 2 Crypto-Logical Systems 2.1 Crude and Overly General Definition 2.2 Information Sets and Preorders of States 2.3 Refining the Definition of Crypto-Logical Systems 2.4 Probability vs. Knowledge 2.5 Global Semantics 2.6 Knowledge of Probability vs Probability of Knowledge 3 Cryptographic Definitions in Crypto-Logic 4 Examples of Reasoning in Crypto-Logic 4.1 Security of the Vernam Cryptosystem 4.2 El-Gamal 4.3 Towards Protocols for Noisy Muddy Mistrustful Children References Joshua Guttman: Pioneering Strand Spaces 1 Introduction 2 Strand Spaces 3 Concluding Remarks References Cryptographic Protocol Analysis and Compilation Using CPSA and Roletran 1 Introduction 2 Message Algebras 3 Strand Spaces with Channels 3.1 Unilateral Protocol Example 3.2 Channel Assumptions 4 Abstract Execution Semantics 4.1 Correctness 5 A Runtime with Probabilistic Encryption 6 Concrete Execution Semantics 7 Relating Execution Semantics 8 Epilogue References On Orderings in Security Models 1 Introduction 2 Preliminaries 3 Attack Trees 4 Copland 5 Attribute Domains 6 Copland Trust Ordering 7 Cryptographic Protocols 8 Conclusion References Prototyping Formal Methods Tools: A Protocol Analysis Case Study 1 Introduction 2 End-To-End Language-Oriented Modeling 2.1 Protocol Analysts: Custom Visualization and Queries 2.2 The Protocol Creator: Translating Domain-Specific Input 2.3 Scripting and Extensibility 3 Relational Model Finding 4 Modeling Protocol Executions 5 Processing cpsa Declarations 5.1 Deriving Relational Constraints 5.2 Queries and Predicates 6 Visualizing Strands 7 Prototype Performance 8 Related Work 9 Discussion References Principles of Remote Sattestation 1 Introduction 2 Overview of Self-authenticating Traditional Addresses 2.1 Third-Party Sattestation 2.2 Trust Yourself..., But Verify 3 Principles of (S)attestation References Author Index