Formal analysis of security protocols based on web services

Shabbir, Fatima 2011. Formal analysis of security protocols based on web services. PhD Thesis, Cardiff University.

PDF - Accepted Post-Print Version Download (12MB)

Abstract

This thesis examines the use of multi-stack pushdown automata to model the behaviour and properties of Web services based cryptographic protocols. The protocols are modelled in Promela and verified using the Spin model checker. The Simple Message Exchange Protocol and the Security Token Protocol are protocols that underlie the WS-Security and WS-Trust specifications, respectively. These two protocols are tested for correctness in the presence of an intruder that conforms to the Dolev-Yao model, i.e., it is tested whether the required properties the protocols hold in the presence of a Dolev-Yao intruder. The thesis also extends the Dolev-Yao intruder model to encompass attacks targeted specifically at Web services. An intruder model in Promela is created based on the Dolev-Yao abstraction which is extended to incorporate an XML injection attack model. The behaviour and properties of the Simple Message Exchange Protocol and the Security Token Protocol are then examined when subjected to an XML injection attack using this extended Dolev-Yao model.

Item Type:	Thesis (PhD)
Status:	Unpublished
Schools:	Computer Science & Informatics
Subjects:	Q Science > QA Mathematics > QA76 Computer software
ISBN:	9781303222498
Date of First Compliant Deposit:	30 March 2016
Last Modified:	19 Mar 2016 23:31
URI:	https://orca.cardiff.ac.uk/id/eprint/55091

Actions (repository staff only)

Edit Item