Skip to main content
Kent Academic Repository

Security specification: completeness, feasibility, refinement

Boiten, Eerke Albert (2010) Security specification: completeness, feasibility, refinement. In: Extended Abstracts Collection -- Refinement Based Methods for the Construction of Dependable Systems, Dagstuhl, Germany. (KAR id:30692)


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''?

Item Type: Conference or workshop item (Paper)
Additional information:
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Eerke Boiten
Date Deposited: 21 Sep 2012 09:49 UTC
Last Modified: 16 Nov 2021 10:08 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Boiten, Eerke Albert.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.