Smart home technology is an application of ubiquitous computing that equips living environments with different types of sensors, actuators, and appliances under computer control to improve the quality of life for inhabitants. Services such as health and behavior monitoring, personalized customization of home operation, control and automation of the environment, and assistance with physical or mental tasks enable inhabitants to live safer, more comfortable, and more independent lives. Many commercial and research efforts are investigating the vast potential that smart homes and related products provide to assist the activities of daily living. However, the resulting efforts frequently suffer from two main limitations that hinder their widespread use. First, resulting products are usually proprietary, offering closed services that are tailored to specific applications and cannot be easily reused or extended by other services in the smart home. Second, the invasiveness of the technology and use of personal information may allow the privacy of the inhabitants to be violated.;We have previously addressed the privacy issue by calling for a privacy policy-based framework [1][2] to control the collection, storage, use and dissemination of personal information in smart home environments. This framework supports several high level goals, including promoting inhabitant awareness of the abilities of devices/services contained in the smart home space, using privacy policies that express the contextual nature of privacy, providing mechanisms and tool support for the authoring, deployment, enforcement, and auditing of privacy policies, as well as creating and verifying policy models to detect conflicts and incorrect specification of privacy policies. In this thesis, we focus on the modeling and verification of policies by proposing a combination of the service-oriented computing and privacy policy paradigms to create a preliminary privacy model for smart homes. We then offer an example scenario and discuss how we employ model checking techniques to verify various aspects of our proposed policy model. The major contributions of this work are four-fold: (1) We extend the notion of personal privacy to include the control of how household objects are used by smart home services. (2) We introduce the use of service-oriented computing to bind resources to the policy space. (3) We define a novel service-oriented privacy policy model that authorizes both the flow of personally sensitive data and the control of environment objects based on inhabitant preferences and various system contexts. (4) We introduce the use of model checking techniques to verify correctness properties of privacy policy models and their enforcement.;The rest of the paper is organized as follows: section 2 gives background information about smart homes, information privacy, policy-based management in distributed systems, and model checking, section 3 presents existing privacy analyses and policy models, section 4 presents our novel privacy model, section 5 illustrates with an example scenario how model checking can be used to verify our privacy model, and section 6 concludes with discussion and future work. Appendix A contains model implementation files, and Appendix B contains property specification files.