School of Computing

Security specification: completeness, feasibility, refinement

Eerke A. Boiten

In Jean-Raymond Abrial, Michael Butler, Rajeev Joshi, Elena Troubitsyna, and Jim C. P. Woodcock, editors, Refinement Based Methods for the Construction of Dependable Systems, number 09381 in Dagstuhl Seminar Proceedings, pages 182-196, Dagstuhl, Germany, January 2010. Schloss Dagstuhl - Leibniz-Zentrum f"ur Informatik, Germany http://drops.dagstuhl.de/opus/volltexte/2010/2374.

Abstract

The formal methods and refinement community should be able to contribute to the specification and verification of security protocols. This talk describes a few of the essential differences, or problems. First, security properties go beyond functional correctness, and are fundamentally different for different applications. Moreover, tomorrow's attacks may not be anticipated by yesterday's security properties. Second, notions of security may not be absolute: it may be good enough if guessing our secret is merely hard rather than impossible -- and in some cases that may be provably the best we can get. Where does that leave us in wanting to provide security protocols "correct by construction"?



Bibtex Record

@conference{2974,
author = {Eerke A. Boiten},
title = {Security specification: completeness, feasibility, refinement},
month = {January},
year = {2010},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {http://drops.dagstuhl.de/opus/volltexte/2010/2374},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2010/2974},
    publication_type = {conference},
    submission_id = {4294_1263482553},
    booktitle = {Refinement Based Methods for the Construction of Dependable Systems},
    editor = {Jean-Raymond Abrial and Michael Butler and Rajeev Joshi and Elena Troubitsyna and Jim C. P. Woodcock},
    number = {09381},
    series = {Dagstuhl Seminar Proceedings},
    address = {Dagstuhl, Germany},
    publisher = {Schloss Dagstuhl - Leibniz-Zentrum f"ur  Informatik, Germany},
    ISSN = {1862-4405},
    refereed = {no},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014