|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.|
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 .
|1) Download Document PS|
Open access Restricted Private