Home
Course description
Syllabus
Projects
Lecture slides
Tools and reference | |
Introduction to security protocols
 | Introduction: Course outline, Computer security, Cryptographic
protocols, Security analysis, Needham-Schroeder example, Murphi
Lecture slides: ppt, pdf
Readings:
|
| 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
Readings:
|
| 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, pdf
Formal analysis techniques
| Experiences in the Formal Analysis of the
GDOI protocol (guest lecture by Catherine Meadows): Group Domain of
Interpretation (GDOI) protocol, NRL Protocol Analyzer, NPATRL temporal
requirements language, Analysis of GDOI Using NPA/NPATRL, Logic for
protocol analysis
Lecture slides: ppt, pdf |
| 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,
pdf
Readings:
|
| Protocols for Anonymity: Applications of anonymity, Chaum’s MIX,
Dining Cryptographers, Anonymity via random routing (Onion Routing, Crowds
System)
Lecture slides: ppt,
pdf
Readings:
|
| Probabilistic Model Checking: Crowds System, Probabilistic notions
of anonymity, Markov chains, PRISM, PCTL logic, Probabilistic fair
exchange
Lecture slides: ppt,
pdf
Readings:
|
| 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
Readings:
|
| 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
Readings:
|
| 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
Lecture slides (part 2): ppt,
pdf
Readings:
 | A Logic of Authentication, Michael
Burrows, Martin Abadi, Roger Needham |
| A
Compositional Logic for Proving Security Properties of Protocols,
Nancy Durgin, John Mitchell, Dusko Pavlovic |
| A Derivation
System for Security Protocols and its Logical Formalization, Anupam
Datta, Ante Derek, John Mitchell, Dusko Pavlovic |
|
| Symbolic Protocol Analysis: Strand space model, Symbolic analysis
problem, From protocols to constraints, SRI Constraint Solver
Lecture slides: ppt,
pdf
Readings:
|
| Security in Process Calculus: Pi Calculus, Modeling secrecy with
scoping, Applied Pi Calculus, Security as observational equivalence, Testing
equivalence
Lecture slides: ppt,
pdf
Readings:
|
| 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
Readings:
| Alternating-time
Temporal Logic, Rajeev Alur, Thomas Henzinger, Orna Kupferman |
| Mocha:
Modularity in Model Checking, Rajeev Alur, Thomas Henzinger, F.Y.C.
Mang, Shaz Qadeer, Sriram Rajamani, Serdar Tasiran |
| A
Game-Based Verification of Non-Repudiation and Fair Exchange Protocols,
Steve Kremer, Jean-Francois Raskin |
| Game Analysis
of Abuse-free Contract Signing, Steve Kremer, Jean-Francois Raskin |
|
| 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
Readings:
|
Project Presentations
| iKP: i-Key-Protocol (Secure Electronic Payment), Christopher Hsu |
| Analysis of an Internet Voting Protocol, Dale Neal, Garrett Smith |
| XML Security, Jun Yoshida |
|
