Industrial systems, also called SCADA (for Supervisory Control And Data Acquisition),are targeted by cyberattacks since Stuxnet in 2010. Due to the criticality of theirinteraction with the real world, these systems can be really harmful for humans andenvironment. As industrial systems have historically been physically isolated from therest of the world, they focused on the protection against outages and human mistakes(also called safety). Cybersecurity differs from safety in the way that an adversary iswilling to harm the system and will learn from his mistakes. One of the difficulty interms of cybersecurity of industrial systems is to make coexist security properties withdomain specific constraints. We tackle this question with three main axes.First, we propose a filter dedicated to industrial communications, allowing to enforceapplicative properties. Then, we focus on formal verification of cryptographic protocolsapplied to industrial protocols such as MODBUS or OPC-UA. Using well-known toolsfrom the domain, we model the protocols in order to check if they provide securityproperties including confidentiality, authentication and integrity. Finally, we propose anapproach named ASPICS (for Applicative Attack Scenarios Production for IndustrialControl Systems) to study if safety properties (similar to those verified by our filter)can actually be jeopardized by attackers depending on their position and capacity. Weimplement this approach in the UPPAAL model-checker and study its results on aproof-of-concept example.