Introduction to security protocols
 | Introduction: Course outline, Computer security, Cryptographic
protocols, Security analysis, Needham-Schroeder example, Murphi
Lecture slides: ppt, pdf
|
| SSL/TLS Case Study: Starting with the RFC describing the protocol,
how to create an abstract model and code it up in Murphi, specify security
properties, and run Murphi to check whether security properties are
satisfied
Lecture slides: ppt, pdf
|
| Key Exchange Protocols: Key management, Kerberos, Public-Key infrastructure, Security properties and attacks on them, Needham-Schroeder Lowe protocol, Diffie-Hellman key exchange, IPsec, IKE |
Lecture slides: ppt
|
Projects and 802.11i Wireless Networking protocol We'll talk about some project ideas for this year, and then go through some of a case study on 802.11i. This case study started with a CS259 project in 2004, and led to three research papers and some changes to the networking standard.
Lecture slides: ppt |
More example protocols and other systems
| Contract-Signing Protocols: Fundamental limitation of
Contract-Signing and Fair-Exchange, Trusted third party, Optimistic
Contract-Signing, Asokan-Shoup-Waidner protocol, Desirable properties
(fairness, timeliness, accountability, balance), Abuse-Free Contract-Signing
Lecture slides: ppt,
|
|
Password Authentication: Hashed password files and salt; Web authentication issues:sniffing, phishing, spyware; Password-authenticated key exchange protocols
Lecture slides: ppt
|
| Probabilistic Model Checking: Crowds System, Probabilistic notions
of anonymity, Markov chains, PRISM, PCTL logic, Probabilistic fair
exchange
Lecture slides: ppt,
pdf
|
| Protocol Verification by the Inductive Method: Protocol analysis
using theorem proving, Inductive proofs, Isabelle theorem prover, Verifying
the Secure Electronic Transactions (SET) protocols using Isabelle
Lecture slides: ppt, pdf
|
| Probabilistic Contract Signing: Rabin’s Beacon, Rabin’s
Contract Signing protocol, BGMR probabilistic Contract Signing, Formal model
for the BGMR protocol
Lecture slides: ppt,
pdf
|
| Logic for Computer Security Protocols: Floyd-Hoare logic of
programs, BAN Logic, Compositional Logic for Proving Security Properties of
Protocols
Lecture slides (part 1): ppt,
pdf
|
| Symbolic Protocol Analysis: Strand space model, Symbolic analysis
problem, From protocols to constraints, SRI Constraint Solver
Lecture slides: ppt,
pdf
|
| Security in Process Calculus: Pi Calculus, Modeling secrecy with
scoping, Applied Pi Calculus, Security as observational equivalence, Testing
equivalence
Lecture slides: ppt,
pdf
|
| Game-Based Verification of Fair Exchange Protocols: The problem of
fair exchange, Protocol as a game tree, Alternating transition systems,
Alternating-time temporal logic, MOCHA Model Checker
Lecture slides: ppt,
pdf
|
| Probabilistic Polynomial-Time Process Calculus for Security Protocol
Analysis: Equivalence-based specification of correctness, Probabilistic
poly-time analysis, Security of encryption schemes, Process calculus,
Probabilistic observational equivalence
Lecture slides: ppt,
pdf
|