The design and analysis of security in distributed computing systems raises numerous questions on the tools available for modeling and verification. Particularly, it is difficult to ensure the correctness when using different validation processes in software architecture design. Assuring cross-platform validation manually is labor intensive, expertise dependent, and error prone. This paper proposes an approach for the design and analysis of secure software architecture in the context of a component-port-connector architecture model and message passing communication. We use the Event-B formal method to create the software architecture model and security in successive steps using the refinement process. We also use proof obligations to verify the security of the successive software architecture models. Furthermore, we use the ProB model-checker and animator for the model validation.