Weaving Authentication and Authorization Requirements into the Functional Model of a System Using Z Promotion

Ali�Nasrat Haidar, Ali E. Abdallah

    Research output: Chapter in Book/Report/Conference proceedingChapter

    Abstract

    The use of Z in software development has focused on specifying the functionality of a system. However, when developing secure system, it is important to address fundamental security aspects, such as authentication, authorization, and auditing. In this paper, we show an approach for building systems from generic and modular security components using promotion technique in Z. The approach focuses on weaving security component into the functionality of a system using promotion technique in Z. For each component, Z notation is used to construct its state-based model and the relevant operations. Once a component is introduced, the defined local operations are promoted to work on the global state. We illustrate this approach on the development of a ?secure? model for a conference management system. With this approach, it is possible to specify the core functionalities of a system independently from the security mechanisms. Authentication and authorization are viewed as components which are carefully integrated with the functional system.
    Original languageEnglish
    Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation
    PublisherSpringer
    Pages831-846
    Number of pages16
    ISBN (Print)0302-9743
    Publication statusPublished (VoR) - 2008

    Keywords

    • Large Scale Embedded Software Systems
    • Comprehensive Architecture
    • Specification
    • Verification

    Fingerprint

    Dive into the research topics of 'Weaving Authentication and Authorization Requirements into the Functional Model of a System Using Z Promotion'. Together they form a unique fingerprint.

    Cite this