Team Automata for Security Analysis of Multicast/Broadcast Communication

Maurice ter Beek, Gabriele Lenzini, Marinella Petrocchi

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    21 Downloads (Pure)


    We show that team automata (TeA) are well suited to model secure multicast/broadcast communication with possible packet loss. This is a consequence of the natural way in which one-to-many (one-to-all) transmissions typical of multicast (broadcast) sessions can be modelled as communications between the component automata (CA) constituting a TeA. To this aim, we use TeA to model an instance of the EMSS multicast protocol family. In addition we investigate a formulation of the Generalized Non-Deducibility on Compositions (GNDC) schema in terms of TeA with the aim to embed TeA in this well-established analysis framework. We intend to use this new setting for the formal verification of security properties for stream signature protocols.
    Original languageUndefined
    Title of host publicationATPN Workshop on Issues in Security and Petri Nets (WISP)
    EditorsN. Busi, R. Gorrieri, F. Martinelli
    Place of PublicationEindhoven, The Netherlands
    PublisherBETA Research School for Operations Management and Logistics
    Number of pages6
    ISBN (Print)not assigned
    Publication statusPublished - Jun 2003
    EventATPN Workshop on Issues in Security and Petri Nets (WISP) - Eindhoven, The Netherlands
    Duration: 23 Jun 200323 Jun 2003

    Publication series

    PublisherBeta-Research School for Operation Management and Logics


    WorkshopATPN Workshop on Issues in Security and Petri Nets (WISP)
    Other23 June 2003


    • EWI-846
    • IR-46130
    • METIS-214097

    Cite this