Our paper “Formal Security Analysis of Deep Neural Network Architecture” is now available online. In this paper, we propose a formal approach to verify some security properties of neural networks. The overall approach goes through three steps: (1) specify security objectives as properties of a modeled neural network in a technology-independent specification language; (2) implement the developed model in a suitable tooled language for analysis; and (3) suggest a set of security requirements necessary to fulfill the targeted security objectives. We use first-order logic and modal logic as abstract and technology independent formalism and Alloy as a tooled language. To validate our work, we explore a set of representative security objectives from the Confidentiality, Integrity, and Availability classification in a use case from the unmanned aircraft domain. This paper was presented at the 17th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS 2024). See Publications for more details!