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.
|Publisher||Beta-Research School for Operation Management and Logics|
|Workshop||ATPN Workshop on Issues in Security and Petri Nets (WISP)|
|Period||23/06/03 → 23/06/03|
|Other||23 June 2003|