Session 1.4 - GARAY & RLA Models

Learning Objectives

By the end of this session, you will be able to:

Compare and contrast the GARAY and RLA formal models
Understand the mathematical foundations of blockchain security analysis
Explain the key assumptions and parameters in each model
Analyze how these models help prove blockchain properties
Evaluate the strengths and limitations of formal modeling approaches

Why Formal Models Matter

The Need for Mathematical Rigor

Blockchain systems handle valuable assets and critical data. We need mathematical proofs to guarantee security properties, not just intuitive arguments or empirical testing.

What Formal Models Provide

Precise Definitions: Exact mathematical descriptions of system behavior
Security Proofs: Mathematical guarantees about system properties
Parameter Analysis: Understanding how system parameters affect security
Comparison Framework: Objective way to compare different protocols

Real-World Analogy

Bridge Engineering: Just as engineers use mathematical models to prove a bridge can support certain weights before building it, blockchain researchers use formal models to prove security properties before deploying protocols.

The GARAY Model

Overview

The GARAY model (by Garay, Kiayias, and Leonardos) provides a formal framework for analyzing proof-of-work blockchain protocols like Bitcoin.

Key Components

Time Model

Discrete rounds: Time progresses in steps
Synchronous: All messages delivered within one round
Round duration: Fixed time intervals

Adversary Model

Computational bound: Limited computing power
Adaptive: Can corrupt nodes during execution
Minority constraint: Controls < 50% of hash power

Key Parameters

Important Variables:

n: Total number of participants
t: Maximum number of corrupted participants
f: Mining difficulty (probability of finding a block)
Δ: Maximum network delay
k: Security parameter (confirmation depth)

Security Properties Proven

Chain Quality

Honest blocks appear regularly in the chain

Chain Growth

The chain grows at a predictable rate

Common Prefix

Honest parties agree on chain prefixes

The RLA Model

Overview

The RLA model (Robust Ledger Architecture) focuses on the abstract properties of distributed ledgers, independent of specific consensus mechanisms.

Key Differences from GARAY

GARAY Model

Specific to Proof-of-Work
Synchronous network model
Focus on chain structure
Mining-based analysis

RLA Model

Consensus-mechanism agnostic
Partially synchronous networks
Focus on ledger properties
Abstract transaction analysis

RLA Core Concepts

Ledger Abstraction

RLA treats the blockchain as an abstract ledger that supports two main operations:

READ: Query the current state of the ledger
WRITE: Submit new transactions to the ledger

RLA Security Properties

Liveness

Valid transactions submitted by honest parties will eventually be included in the ledger

∀ valid tx: eventually included

Safety

Once a transaction is confirmed, it cannot be removed or modified

∀ confirmed tx: immutable

Comparing GARAY and RLA Models

Aspect	GARAY Model	RLA Model
Scope	Proof-of-Work specific	General blockchain systems
Network Model	Synchronous	Partially synchronous
Focus	Chain structure and mining	Ledger operations and properties
Adversary	Computational bound	More general adversary models
Applications	Bitcoin, Ethereum (PoW)	Any blockchain system

When to Use Which Model

Use GARAY when analyzing specific PoW protocols, mining strategies, or chain-based properties
Use RLA when designing general blockchain applications, comparing different consensus mechanisms, or focusing on transaction-level properties

Mathematical Foundations

Probability Theory

Key Concepts Used:

Random Variables: Block arrival times, mining success
Probability Distributions: Poisson process for block generation
Concentration Bounds: Chernoff bounds for security analysis
Martingales: For analyzing adversarial strategies

Cryptographic Assumptions

Hash Functions

Random oracle model
Collision resistance
Uniform output distribution

Digital Signatures

Existential unforgeability
Public key infrastructure
Non-repudiation

Practical Applications

Protocol Design

Parameter selection (block time, difficulty)
Security threshold determination
Confirmation time analysis
Attack resistance evaluation

Security Analysis

Double-spending attack analysis
Selfish mining detection
Network partition resilience
Long-range attack prevention

Bitcoin Example

Using the GARAY model, researchers proved that Bitcoin is secure if:

Honest miners control > 50% of hash power
Network delay < block generation time
Confirmation depth k ≥ 6 blocks for high security

Limitations and Future Directions

Current Limitations

Idealized Assumptions: Perfect cryptography, rational actors
Network Models: May not capture real network behavior
Economic Factors: Limited modeling of economic incentives
Implementation Gaps: Theory vs. practice differences

Future Research

Hybrid Models: Combining different approaches
Economic Security: Game-theoretic analysis
Quantum Resistance: Post-quantum cryptography
Scalability Models: Sharding and layer-2 analysis

Session Summary

Key Takeaways

Formal models provide mathematical rigor for blockchain security analysis
GARAY model is specific to PoW systems with detailed chain analysis
RLA model is more general and focuses on ledger properties
Both models help prove security properties and guide protocol design
Mathematical foundations include probability theory and cryptographic assumptions
Models have limitations but continue to evolve with new research

What's Next?

In the next session, we'll explore Peer-to-Peer Networks, examining how blockchain nodes communicate, handle network churn, and maintain connectivity in distributed environments.

Next: Peer-to-Peer Networks Previous: Consensus Problem Back to Course Home