Formal Verification of a Type Flaw Attack on a Security Protocol using Object-Z

Speaker: Ben Long

When: 10:00, Friday, 18 March 2005

Venue: 78-420

We have identified a type flaw attack on the Amended Needham Schroeder Protocol with Conventional Keys due to a potential oversight at the presentation layer of the network architecture. Using Object-Z, a formal specification of the protocol is presented allowing us to state the assumed properties of the presentation layer explicitly. Object-Z's schema calculus is used to verify the attack we have found and the weaknesses upon which the attack depends, thus enabling us to minimise the effort required to prevent the attack and to specify this as part of the model accordingly.

Hospitality: Roger Duke

Contact: Phil Cook (SSE seminar co-ordinator) (philc@itee.uq.edu.au)

SSE seminar web page: http://www.itee.uq.edu.au/~sse/Seminars.html