[Winner of the Best Paper Award, REFINE 2005]
It is well known that security properties are not preserved by refinement, and that refinement can introduce new, covert , channels, such as timing channels. The finalisation step in refinement can be analysed to identify some of these channels, as unwanted finalisations that can break the assumptions of the formal model. We introduce a taxonomy of such unwanted finalisations, and give examples of attacks that exploit them.
@inproceedings(SS-REFINE05a, author = "John A. Clark and Susan Stepney and Howard Chivers", title = "Breaking the Model: finalisation and a taxonomy of security attacks", pages = "225--242", crossref = "REFINE05" ) @proceedings(REFINE05, title = "REFINE 2005 Workshop, Guildford, UK, April 2005", booktitle = "REFINE 2005 Workshop, Guildford, UK, April 2005", series = "ENTCS", volume = 137, number = 2, publisher = "Elsevier", year = 2005 )