Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Lenzini G., Petrocchi M. Team Automata for Security Analysis of Multicast/Broadcast Communication. The document has been submitted to other Workshop on Issues in Security and Petri Nets (WISP), Eindhoven, The Netherlands, 2003. Technical report, 2003.
We show that team automata (TA) 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 TA. To this aim, we use TA 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 TA with the aim to embed TA in this well-established analysis framework. We intend to use this new setting for the formal verification of security properties for stream signature protocols.
Subject Team automata
multicast/broadcast communication
D.2.4 Software/Program Verification . Formal methods
D.4.6 Security and Protection . Verification
F.3.1 Specifying and Verifying and Reasoning about Programs .

Icona documento 1) Download Document PS

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional