Authentication Protocol Verification and Analysis
Summary
Cryptosystems
Cryptographic Protocols
Protocol Vulnerabilities - Ground Rules
Example - Needham-Schroeder
Denning-Sacco Attack
Folklore - Attack Terms
Design Principles
More Design Principles
Formal Methods
Dolev-Yao Model
Dolev-Yao, cont’d
Interrogator
Interrogator, cont’d
NRL Protocol Analyzer
NRL Protocol Analyzer, cont’d
Belief Logic
Constructs
BAN Inference Rules
More BAN Rules
Protocol Idealization
Example - Wide-Mouthed Frog
Analysis
Nessett’s Critique
Observations
Subsequent Developments
Model-Checking
Model-Checking Observations
NSPK Protocol
Lowe Attack on NSPK
Finiteness Limitation
Inductive Proofs
Fundamental Ideas I
Paulson’s Modeling Approach
Paulson’s Model, cont’d
Fundamental Ideas II
Fundamental Ideas III
More on the Ideal
Summary, cont’d
Email: millen@csl.sri.com
Home Page: www.csl.sri.com/~millen
Other information: Presented at ACM Computer and Communication Security symposium, 1998
Download presentation source