Security-Minded Modelling and Verification of Autonomous Satellite Docking⋆

Formal verification of autonomous systems is well established for safety and liveness analysis, yet the explicit modelling and verification of adversarial behaviour at the system level remains limited. In particular, attacker behaviour is often encoded implicitly, obscuring the distinction between attacker capability and system response. This paper presents a security-minded, state-based modelling approach in which the system and the attacker are represented as separate transition systems that interact exclusively through shared inputs. This separation preserves semantic clarity, enables compositional reasoning, and supports rigorous security analysis using standard model-checking techniques. The approach is demonstrated on an autonomous space docking system. An<br/>attacker transition system is systematically derived from CAPEC-148 (Content Spoofing) and models image-spoofing attacks against a visionbased navigation subsystem. Security countermeasures are modelled as constrained variations of the system transition semantics. Security properties are specified in LTL and verified using the SPIN model checker. The results show that explicit separation of system and attacker transition systems enables the identification of insecure configurations and the formal verification of mitigation effectiveness, providing design-time security assurance for autonomous systems.<br/>Keywords: Autonomous systems · Security v