Formal verification of integrity attacks on connected medical devices in battlefield hospitals

Abstract Field hospitals in battlefield settings increasingly rely on connected medical devices, including monitors, ventilators, infusion pumps, patient-identification services, and gateway-based communication. In such environments, integrity attacks may create patient-safety hazards even when the system appears operational, by tampering with data, replaying old messages, injecting false information, or swapping patient identities. This work presents a formal framework for analyzing these attacks as a stochastic clinical–cyber system that integrates patient-state evolution, intermittent communication, attacker actions, and gateway-centered defense policies. Safety is evaluated using bounded unsafe reachability, supported by formal verification and resource-aware strategy synthesis. A synthetic digital twin is used to generate benign and attacked traces without real patient data; therefore, the findings are interpreted as model-based and simulation-based evidence rather than clinical validation. Confirmatory Monte Carlo evaluation used 5000 trajectories per configuration under 20 fixed root seeds. Patient-ID swapping reached an empirical unsafe reachability of 0.297 (95% CI 0.284–0.310) at the largest evaluated per-step attack-capacity limit, while the combined adaptive attacker reached 0.384 (95% CI 0.371–0.397). Evaluation of the synthesized combined gateway policy reduced empirical model-estimated unsafe reachability from 0.392 (95% CI 0.378–0.406) to 0.119 (95% CI 0.110–0.128) in the evaluated synthetic scenario, corresponding to a 69.6% relative reduction in this formal safety proxy, but with increased workflow burden. A separate PRISM-games worst-case query returned 0.410 under the disclosed finite abstraction. Verification remained tractable at the evaluated scales, with median PRISM runtime increasing from 0.90 to 28.70 s as the abstract state space expanded. Overall, the study supports formal verification as an analytical framework for safety-aware cyber-defense evaluation in connected field-hospital medical systems under explicit modeling assumptions; it does not establish clinical risk reduction or deployment readiness.