[ Last changed: 15th November 1995 ]
Security Group Seminar, 24th October 1995
- Speaker:
- Gavin Lowe, Oxford University
- Date:
- Tuesday 24th October
- Place:
- Room TP4, Computer Laboratory
- Title:
- USING PROCESS ALGEBRA TO BREAK SECURITY PROTOCOLS
In this talk I will describe how we may analyze security protocols
using CSP and its refinement checker FDR. Briefly, we encode the
protocol in CSP, produce a CSP model of the most general attacker
who can interact with the protocol, and use FDR to test whether the
resulting system is secure. I will show how to apply this method to
the well known Needham-Schroeder Public-Key Protocol. FDR discovers
an attack upon the protocol, which allows an intruder to
impersonate another agent. I will then show how to adapt the
protocol to prevent this attack, and briefly indicate how we may
use FDR to prove that the resulting protocol is secure.
Security Group Seminar, 24th October 1995 / Mark.Lomas@cl.cam.ac.uk