AVISPA in the Validation of Ambient Intelligence Scenarios

Ambient intelligence (AmI) refers to an environment that is sensitive, responsive, interconnected, contextualized, transparent, intelligent, and acting on behalf of humans. AmI environments impose some constraints in the connectivity framework, power computing as well as energy budget. This makes of AmI a significantly different case within distributed systems. The combination of heterogeneity, dynamism, sheer number of devices, along with the growing demands placed on software security and dependability, make application development vastly more complex. Also, the provision of security and dependability for applications becomes increasingly difficult to achieve with the existing security engineering mechanisms and tools. Furthermore the validation of these mechanisms is even a hard task. In this paper we present an approach to model dynamic changes in ambient intelligence scenarios using the AVISPA (automated validation of Internet security protocols and applications) model-checking tool suite. The main goal of our approach consists on providing a starting point in the use of formal description techniques (FDM) for AmI scenarios. The paper studies and assesses the suitability of the AVISPA tool for security validation in ambient intelligent environments and proposes mechanisms to capture the dynamic context changes in these environments.