Müller, ChristianArmknecht, FrederikBenenson, ZinaidaMorgner, PhilippMeier, MichaelReinhardt, DelphineWendzel, Steffen2017-06-212017-06-212016978-3-88579-650-3Specifications of security mechanisms often lack explicit descriptions of the envisioned security goals and the underlying assumptions. This makes it difficult for developers and customers to understand the level of security provided by the systems. Moreover, this omission has repeatedly resulted in practical attacks that violate the implicit security assumptions of the specifications. In this work, we illustrate this effect on the example of the ZigBee Light Link (ZLL) profile, currently one of the most popular standards for smart lighting in domestic environments. We first provide a concise description of ZLL commissioning procedure for initiating and extending a network of smart bulbs, extracted directly from the specification. We then discuss how the commissioning protocol can be transformed into a formal security model, but also highlight where this is subject to interpretations because of the unclear implicit security assumptions. The proposed security model is flexible, i.e., it can be extended to capture further security requirements or attacker classes, and hence provides a solid foundation for rigorous security analyses of ZLL and other ZigBee profiles.enText/Conference Paper1617-5468