Formalizing security requirements has received a significant attention since the 70s. However, a general method for specifying security requirements is still missing. Especially, little work has been presented on specifying and verifying that a given application is a secure resource consumer. The purpose of this work is to set up a methodology for (1) specifying security requirements of service providers and (2) proving that some application securely uses some resources. The developed theory will be evaluated and applied in two different areas: secure mobile code development and secure COTS-based software development.