Connector-based software development: Deriving secure protocols

Abstract

While most branches of engineering consist of methodologies for building complex systems from simple components, formulating incremental and compositional methods for Security Engineering has been a daunting task: in general, security properties are not preserved under refinement or composition. The reason is that the nondestructive composition operations require that their static assumptions about the environment are maintained; but Security Engineering is concerned with dynamic, adversarial environments, and what happens when the assumptions fail. The problem is compounded by the fact that establishing security of a system often involves not only logical and computational structures, but also a wide range of mathematical methods of cryptography. The notions of security thus span across a multi-dimensional space of methods and approaches, which have not yet been systematized on a solid semantical foundation. But practice is faster than theory, and complex secure protocols are being designed and deployed in many systems, often complex and critical. The goal of our research effort towards the Protocol Derivation System (PDS), and of our development towards the Protocol Derivation Assistant (PDA) is to capture, formalize and advance the sound rules and methods of incremental protocol development, that have evolved in practice of Security Engineering. In this talk, I shall summarize the results of this effort so far, and present a case study of GDoI, the standard protocol for group communication and multicast over IPSec [3]. Although carefully designed and thoroughly analyzed, through seven internet drafts prior to standardization, this protocol turned out to have vulnerabilities invalidating the basic stated requirements: an attempt to derive it incrementally, together with the desired security properties, led to a derivation of an attack, which in turn allowed evaluation of the repair options [4]. The derivations were built and will be presented using the Protocol Derivation Assistant, a development environment with support for collaboration and integration [1,2]. GDoI was analyzed in joint work with Catherine Meadows. PDA can be freely downloaded from [I]. © Springer-Verlag Berlin Heidelberg 2006.