TY - GEN
T1 - Sums and lovers
T2 - 2nd World Congress on Formal Methods, FM 2009
AU - McIver, Annabelle K.
AU - Morgan, Carroll C.
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=70649085848&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-05089-3_19
DO - 10.1007/978-3-642-05089-3_19
M3 - Conference proceeding contribution
AN - SCOPUS:70649085848
SN - 9783642050886
T3 - Lecture Notes in Computer Science
SP - 289
EP - 304
BT - FM 2009: Formal Methods
A2 - Cavalcanti, Ana
A2 - Dams, Dennis R.
PB - Springer, Springer Nature
CY - Berlin
Y2 - 2 November 2009 through 6 November 2009
ER -