Our project brings first-order theorem proving in the landscape of ensuring system security, complementing and improving other approaches in the area. The common theme of our project comes with our recently introduced trace logic, that is an instance of many-sorted first-order logic with equality. Our project extends trace logic with support for function calls and nested loops. We then use compositional analysis to scale first-order theorem proving in trace logic for finding and deriving system security properties in trace logic. Further, since security properties can be arbitrarily complex, we will design sophisticated reasoning methods in trace logic to prove security properties, possibly with alternations of quantifiers. We will also develop new approaches minimising the number of relevant security properties, with the overall goal to develop a fully automated, efficient and world-leading first-order theorem prover for trace logic. Our project will push the state-of-the-art in automated reasoning about system security, since first-order theorem proving and its applications in trace logic have not yet been fully addressed by other methods.