Please use this identifier to cite or link to this item:
|Title:||A CSP approach to the analysis of security protocols|
|Authors:||Hui, Mei Lin.|
|Presented at:||University of Leicester|
|Abstract:||Security protocols involve an exchange of messages in order to achieve a goal such as authentication of a user or secrecy of a session key. Many established protocols have been found to be flawed using protocol analysis techniques. In this thesis we will be extending current CSP-based protocol modelling techniques.;Recent techniques for analyzing security protocols have tended to concentrate upon the small protocols that are typically found in the academic literature. However, there is a huge gulf between these and most large commercial protocols. As a result, existing techniques are difficult to apply directly to these large protocols.;In this thesis we develop the notion of safe simplifying transformations: transformations that have the property of preserving insecurities; the effect of such transformations is that if we can verify the transformed protocol, then we will have verified the original protocol. We identify a number of safe simplifying transformations, and use them in the analysis of two commercial protocols, the CyberCash Main Sequence protocol and SET.;We extend the CSP-based analysis technique to model the property of non-repudiation and give a formal generalized definition. Our definition of non-repudiation is tested against our two case studies.;Another property we model is that of key compromise: the reuse of a compromised session key that might lead to an authentication or secrecy attack. We look at how to model the intruder learning the value of a key and then using it in an attack. We apply this technique to our case studies, looking for key compromise attacks using the session keys.|
|Rights:||Copyright © the author. All rights reserved.|
|Appears in Collections:||Theses, Dept. of Mathematics|
Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.