A team automaton scenario for the analysis of security properties of communication protocols

Formal methods are a popular means to specify and verify security properties of avariety of communication protocols. In this article we take a step towards the use ofteam automata for the analysis of security aspects in such protocols. To this aim, wedefine an insecure communication scenario for team automata that is general enoughto encompass various communication protocols. We then reformulate the GeneralizedNon-Deducibility on Compositions schema--originally introduced in the contextof process algebrae--in terms of team automata. Based on the resulting team automataframework, we subsequently develop two analysis strategies that can be used to verifysecurity properties of communication protocols. Indeed, the paper concludes with twocase studies in which we show how our framework can be used to prove integrity andsecrecy in two different settings: We show how integrity is guaranteed in a team automatonmodel of a particular instance of the Efficient Multi-chained Stream Signatureprotocol, a communication protocol for signing digital streams that provides some robustnessagainst packet loss, and we show how secrecy is preserved when a member ofa multicast group leaves the group in a particular run of the complementary variableapproach to the N-Root/Leaf pairwise keys protocol.