Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.14/148612
7 Visitors
9 Hits
0 Downloads
- Title
- Sums and lovers : case studies in security, compositionality and refinement
- Related
- International Symposium of Formal Methods Europe (16th : 2009) (2 - 6 November 2009 : Eindhoven, Netherlands)
- Related
- Cavalcanti, Ana and Dam, Dennis. FM 2009 : formal methods : second world congress, Eindhoven, the Netherlands, November 2-6, 2009 : proceedings, p.289-304
- DOI
- 10.1007/978-3-642-05089-3_19
- Related
- Lecture notes in computer science Vol. 5850
- Publisher
- Berlin ; New York : Springer-Verlag
- Date
- 2009
- FoR/RFCD Code(s)
-
080200 Computation Theory and Mathematics
- Author/Creator
- McIver, Annabelle K
- Author/Creator
- Morgan, Carroll C
- Description
- A truly secure protocol is one which never violates its security requirements, no matter how bizarre the circumstances, provided those circumstances are within its terms of reference. Such cast-iron guarantees, as far as they are possible, require formal techniques: proof or model-checking. Informally, they are difficult or impossible to achieve. Our technique is refinement, until recently not much applied to security. We argue its benefits by giving rigorous formal developments, in refinement-based program algebra, of several security case studies. A conspicuous feature of our studies is their layers of abstraction and –for the main study, in particular– that the protocol is unbounded in state, placing its verification beyond the reach of model checkers. Correctness in all contexts is crucial for our goal of layered, refinement-based developments. This is ensured by our semantics in which the program constructors are monotonic with respect to “security-aware” refinement, which is in turn a generalisation of compositionality.
- Description
- 16 page(s)
- Subject Keyword
- 080200 Computation Theory and Mathematics
- Subject Keyword
- Refinement of security
- Subject Keyword
- formalised secrecy
- Subject Keyword
- hierarchical security reasoning
- Subject Keyword
- compositional semantics
- Resource Type
- conference paper
- Organisation
- Macquarie University. Dept. of Computing
- Identifier
- http://hdl.handle.net/1959.14/148612
- Identifier
- ISBN:9783642050893
- Identifier
- ISSN:0302-9743
- Identifier
- mq-rm-2009004456
- Language
- eng
- Reviewed
