Automotive architectures are evolving with increased computational power and network connectivity, including mandatory overthe- air updates. This transformation enlarges the attack surface and increases security risks that impact safety. This contribution investigates the security of automotive network architectures (ANAs) and application protocols via formal modeling and verification approaches. The focus is on resilience against a strong adversary that is capable of partial component and network compromise. The key questions that are addressed include the formal modeling of ANAs, the impact of compromised components, and the comprehensive evaluation of security properties (SPs). Attack Resilience Hyperproperties (ARHs) are introduced to model complex SPs that involve compromised components. A prototype tool, ExACT, is provided for the analysis of ARHs with the Tamarin Prover. Additionally, a scoring system is proposed to evaluate the robustness of architectural variants. The real-world applicability of these approaches is demonstrated through a case study involving an ANAs and a secure log file upload protocol.