The design and analysis of security in distributed systems raises numerous questions about the available tools for modeling and verification. It is difficult to ensure the relationship between the selected security solutions and the security concerns in software architecture design. We address this challenge by proposing an integrated approach for specifying and verifying security objectives in component-based software architecture models via reusable formal model libraries of security properties and constraints. Our solution is based on metamodeling techniques for specifying the software architecture structure and on formal techniques for precisely specifying and verifying security properties of a modeled system. We explore a set of representative security objectives from the Confidentiality, Integrity, Availability (CIA) classification. We also use model-driven engineering techniques for the development of a tool suite to support our approach.