Formal modeling and automatic enforcement of Bring Your Own Device policies