Peterson, Jordan T., authorRay, Indrakshi, advisorPrabhu, Vinayak, advisorGersch, Joseph, committee memberHayne, Stephen, committee member2021-06-072021-06-072021https://hdl.handle.net/10217/232471Smart homes have devices which are prone to attacks as seen in the 2016 Mirai botnet attacks. Authentication and access control form the first line of defense. Towards this end, we propose an attribute-based access control framework for smart homes that is inspired by the Next Generation Access Control (NGAC) model. Policies in a smart home can be complex. Towards this end, we demonstrate how the formal modeling language Alloy can be used for policy analysis. In this work we formally define an IoT environment, express an example security policy in the context of a smart home, and show the policy analysis using Alloy. This work introduces processes for identifying conflicting and redundant rules with respect to a given policy. This work also demonstrates a practical use case for the processes described. In other words, this work formalizes policy rule definition, home IoT environment definition, and rule analysis all in the context of NGAC and Alloy.born digitalmasters thesesengCopyright and other restrictions may apply. User is responsible for compliance with all applicable laws. For information about copyright law, please see https://libguides.colostate.edu/copyright.attribute-based access controlformal modelingredundancy identificationconflict identificationAlloyNext Generation Access ControlText