Learn

You don't need a security background. You don't need to know what a capability token is. You do need to understand what AI agents are — that they call tools, read files, and make decisions. Everything beyond that, we build from scratch.

This section takes you from "I use AI tools but I don't know how they're secured" all the way to understanding how an MCP gateway enforces least privilege, information flow control, and cryptographic identity for AI agent teams.

Part I: The Threat Model

#	Topic	What you'll understand
0	What Agents Actually Do	Tool calls, not just chat — why agents are processes, not users
1	Why Prompts Aren't Security	System prompts as access control — and why they fail
2	Prompt Injection	The fundamental unsolvable problem in AI security
3	The Multi-Agent Surface	How delegation, shared context, and tool chains multiply risk
4	What a Gateway Can and Cannot Do	Infrastructure-level enforcement vs semantic-level attacks

Part II: OS Security Primitives

#	Topic	What you'll understand
5	Agents as Processes	Why the OS analogy works — isolation, scheduling, identity
6	Capabilities	Dennis & Van Horn to Capsicum — unforgeable tokens for access control
7	Privilege Rings	Ring 0/1/2, deny-wins, why outer rings can't escalate
8	Information Flow Control	Bell-LaPadula, lattices, taint labels — preventing data exfiltration
9	The Microkernel Idea	Mach → L4 → seL4 — small trusted base, everything else is userland

Part III: Cryptographic Identity

#	Topic	What you'll understand
10	Digital Signatures	Ed25519 — how signing works and why agents need it
11	Decentralized Identifiers	DIDs and did:key — identity without a registry
12	Capability Tokens	CBOR encoding, attenuation, expiry — why not JWT
13	Delegation Chains	How a leader issues narrower tokens to specialists
14	Post-Quantum Readiness	ML-DSA, hybrid signatures, algorithm agility

Part IV: The MCP Protocol

#	Topic	What you'll understand
15	JSON-RPC and Transports	The wire format — JSON-RPC 2.0 over HTTP, stdio, WebSocket
16	Tools, Resources, Prompts	The three MCP primitives and what flows through each
17	The Security Chokepoint	Where enforcement happens — handle_call_tool as the system call boundary
18	Upstream and Proxy	How the gateway mediates access to external MCP servers
19	Agent-to-Agent Protocol	A2A for inter-agent communication — agent cards, task lifecycle

Part V: Formal Verification

#	Topic	What you'll understand
20	What Kani Proves	Bounded model checking, SAT solvers, "all inputs within bounds"
21	Reading a Kani Harness	Annotated walkthrough of a real proof from navra
22	TLA+ Specifications	Protocol-level model checking — what temporal logic adds
23	Property Testing	Where proofs end and tests begin — complementary approaches
24	The Verification Gap	What remains unproven and why

Part VI: Privacy Engineering

#	Topic	What you'll understand
25	PII Detection with Regex	Fast pattern matching — SSNs, credit cards, emails
26	Named Entity Recognition	ONNX models for detecting names, addresses, organizations
27	The Privacy Router	Routing, short-circuit, language detection — coordinating 5 detectors
28	False Positives and Thresholds	The tradeoff between safety and usability
29	Compliance Mapping	EU AI Act, SOC2, ISO 42001 — what the blackbox addresses

How to read this

Part I stands alone — stop after Chapter 4 and you'll understand why navra exists and what problem it solves.

Part II explains the classical OS security concepts that navra adapts — capabilities, rings, IFC, microkernels. If you're a security person, skim this. If you're an AI person, read it carefully.

Part III covers the cryptography behind agent identity and capability tokens — Ed25519, DIDs, CBOR, delegation chains.

Part IV explains the MCP protocol and where security enforcement happens in the request lifecycle.

Part V covers formal verification — what Kani and TLA+ prove about navra's security properties, and what they don't.

Part VI covers privacy engineering — how content filtering works at the gateway layer, from regex to ONNX models.

Go in order within each part. After Part I, the other parts can be read in any order based on interest.