Abstract. This paper introduces the subject of secrecy models development by transformation, with formal validation. In an enterprise, constructing a secrecy model is a participatory exercise involving policy makers and implementers. Policy makers iteratively provide business governance requirements, while policy implementers formulate rules of access in computer-executable terms. The process is error prone and may lead to undesirable situations thus threatening the security of the enterprise. At each iteration, a security officer (SO) needs to guarantee business continuity by ensuring property preservation; as well, the SO needs to check for potential threats due to policy changes. This paper proposes a method that is meant to address both aspects. The goal is to allow not only the formal analysis of the results of transformations, but also the formal proof that transformations are property preserving. UML is used for expressing and transforming models [1], and the Alloy analyzer is u...