The Complete Guide to SCION: From Design Principles to Formal Verification (Information Security and Cryptography)

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

When the SCION project started in 2009, the goal was to create an architecture offering high availability and security for basic point-to-point communication. In the five years since the publication of SCION: A Secure Internet Architecture, this next-generation Internet architecture has evolved in terms of both design and deployment. On the one hand, there has been development of exciting new concepts and systems, including a new global time-synchronization system, an inter-domain approach for bandwidth reservations called COLIBRI, and Green Networking, which allows combating global climate change on three fronts. On the other hand, SCION is now also in production use by the Swiss financial ecosystem, and enables participants such as the Swiss National Bank, the Swiss provider of clearing services (SIX), and all Swiss financial institutes to communicate securely and reliably with each other via the Secure Swiss Finance Network. This unique guidebook provides an updated description of SCION's main components, covering new research topics and the most recent deployments. In particular, it presents in-depth discussion of formal verification efforts. Importantly, it offers a comprehensive, thorough description of the current SCION system : Describes the principles that guided SCION's design as a secure and robust Internet architecture Provides a comprehensive description of the next evolution in the way data finds its way through the Internet Explains how SCION can contribute to reducing carbon emissions, by introducing SCION Green Networking Demonstrates how SCION not only functions in academic settings but also works in production deployments Discusses additional use cases for driving SCION's adoption Presents the approaches for formal verification of protocols and code Illustrated with many colorful figures, pictures, and diagrams, allowing easy access to the concepts and use cases Assembled by a team with extensive experience in the fields of computer networks and security, this text/reference is suitable for researchers, practitioners, and graduate students interested in network security. Also, readers with limited background in computer networking but with a desire to know more about SCION will benefit from an overview of relevant chapters in the beginning of the book.

Author(s): Laurent Chuat, Markus Legner, David Basin, David Hausheer, Samuel Hitz, Peter Müller, Adrian Perrig
Publisher: Springer
Year: 2022

Language: English
Commentary: Keep pirating ARRRRRR
Pages: 653

Contents
Foreword by Joël Mesot
Foreword by Fritz Steinmann
Preface
How to Read This Book
Acknowledgments
1 Introduction
1.1 Today’s Internet
1.2 Goals for a Secure Internet Architecture
Part I SCION Core Components
2 Overview
2.1 Infrastructure Components
2.2 Authentication
2.3 Control Plane
2.4 Data Plane
2.5 ISD and AS Numbering
3 Authentication
3.1 The Control-Plane PKI (CP-PKI)
3.2 DRKey: Dynamically Recreatable Keys
3.3 SCION Packet Authenticator Option
4 Control Plane
4.1 Path-Segment Construction Beacons (PCBs)
4.2 Path Exploration (Beaconing)
4.3 Path-Segment Registration
4.4 PCB and Path-Segment Selection
4.5 Path Lookup
4.6 Service Discovery
4.7 SCION Control Message Protocol (SCMP)
5 Data Plane
5.1 Inter- and Intra-domain Forwarding
5.2 Packet Format
5.3 Path Authorization
5.4 The SCION Path Type
5.5 Path Construction (Segment Combinations)
5.6 Packet Initialization and Forwarding
5.7 Path Revocation
5.8 Data-Plane Extensions
Part II Analysis of the Core Components
6 Functional Properties and Scalability
6.1 Dependency Analysis
6.2 SCION Path Policy
6.3 Scalability Analysis
6.4 Beaconing Overhead and Path Quality
7 Security Analysis
7.1 Security Goals and Properties
7.2 Threat Model
7.3 Overview
7.4 Control-Plane Security
7.5 Path Authorization
7.6 Data-Plane Security
7.7 Source Authentication
7.8 Absence of Kill Switches
7.9 Other Security Properties
7.10 Summary
Part III Achieving Global Availability Guarantees
8 Extensions for the Control Plane
8.1 Hidden Paths
8.2 Time Synchronization
8.3 Path Metadata in PCBs
9 Monitoring and Filtering
9.1 Replay Suppression
9.2 High-Speed Traffic Filtering with LightningFilter
9.3 Probabilistic Traffic Monitoring with LOFT
10 Extensions for the Data Plane
10.1 Source Authentication and Path Validation with EPIC
10.2 Bandwidth Reservations with COLIBRI
11 Availability Guarantees
11.1 Availability Goals and Threat Landscape
11.2 Overview
11.3 Defense Systems
11.4 Traffic Prioritization
11.5 Protected DRKey Bootstrapping
11.6 Protection of Control-Plane Services
11.7 AS Certification
11.8 Security Discussion
Part IV SCION in the Real World
12 Host Structure
12.1 Host Components
12.2 Future Approaches
13 Deployment and Operation
13.1 Global Deployment
13.2 End-Host Deployment and Bootstrapping
13.3 The SCION–IP Gateway (SIG)
13.4 SIG Coordination Systems
13.5 SCION as a Secure Backbone AS (SBAS)
13.6 Example: Life of a SCION Data Packet
14 SCIONLAB Research Testbed
14.1 Architecture
14.2 Research Projects
14.3 Comparison to Related Systems
15 Use Cases and Applications
15.1 Use Cases
15.2 Applications
15.3 Case Study: Secure Swiss Finance Network (SSFN)
15.4 Case Study: SCI-ED, a SCION-Based National Academic and Research Network
16 Green Networking with SCION
16.1 Direct Power Savings with SCION
16.2 SCION Enables Green Inter-domain Routing
16.3 Incentives for ISPs to Use Renewable Energy Resources
17 Cryptography
17.1 How Cryptography Is Used in SCION
17.2 Cryptographic Primitives
17.3 Local Cryptographic Primitives
17.4 Global Cryptographic Primitives
17.5 Post-Quantum Cryptography
Part V Additional Security Systems
18 F-PKI: A Flexible End-Entity Public-Key Infrastructure
18.1 Trust Model
18.2 Overview of F-PKI
18.3 Policies
18.4 Verifiable Data Structures
18.5 Selection of Map Servers
18.6 Proof Delivery
18.7 Certificate Validation
19 RHINE: Secure and Reliable Internet Naming Service
19.1 Background
19.2 Why a Fresh Start?
19.3 Overview of RHINE
19.4 Authentication
19.5 Data Model
19.6 Secure Name Resolution
19.7 Deployment
20 PILA: Pervasive Internet-Wide Low-Latency Authentication
20.1 Trust-Amplification Model
20.2 Overview of PILA
20.3 ASes as Opportunistically Trusted Entities
20.4 Authentication Based on End-Host Addresses
20.5 Certificate Service
20.6 NAT Devices
20.7 Session Resumption
20.8 Downgrade Prevention
Part VI Formal Verification
21 Motivation for Formal Verification
21.1 Local and Global Properties
21.2 Quantitative Properties
21.3 Adversarial Environments
21.4 Design-Level and Code-Level Verification
22 Design-Level Verification
22.1 Overview of Design-Level Verification
22.2 Background on Event Systems and Refinement
22.3 Example: Authentication Protocol
22.4 Verification of the SCION Data Plane
22.5 Quantitative Verification of the N-Tube Bandwidth Reservation Algorithm
23 Code-Level Verification
23.1 Why Code-Level Verification?
23.2 Introduction to Program Verification
23.3 Verification of Go Programs
23.4 Verification of Protocol Implementations
23.5 Secure Information Flow
24 Current Status and Plans
24.1 Completed Work
24.2 Ongoing Work
24.3 Future Plans and Open Challenges
Part VII Back Matter
25 Related Work
25.1 Future Internet Architectures
25.2 Deployment of New Internet Architectures
25.3 Inter-domain Multipath Routing Protocols
Bibliography
Glossary
Abbreviations
Index