ProtoEval: A Family-Based Dual-Verification Framework for Evolving IoT Authentication

Internet of Things (IOT) authentication protocols continuously evolve through structural revisions, including message consolidation and gateway rerouting, to satisfy shifting deployment constraints. Consequently, the engineering challenge transitions from establishing baseline correctness to managing trade-offs among reliability, attack exposure, and communication overhead. However, existing formal methods typically evaluate single protocol versions, treating verification as isolated proofs rather than continuous regression assessments. To bridge this gap, we propose ProtoEval, a family-based dual-verification framework to systematically quantify evolutionary regressions. By introducing a shared milestone semantics, ProtoEval seamlessly integrates qualitative state-space exploration with quantitative probabilistic boundary analysis. We formalize eight reusable evolution operators and evaluate a controlled protocol family comprising twelve base-variant pairs across diverse industry-standard architectures. The evaluation reveals highly protocol-dependent regression behaviors. For example, message consolidation significantly improves success rates in multi-round handshakes but yields marginal benefits in compact protocols, while cryptographic agility consistently acts as a Pareto improver. Validation against complex, real-world protocol evolution chains confirms the framework's directional fidelity and compositional accuracy. Ultimately, this approach reframes formal verification, transforming protocol models from disposable proofs into reusable engineering assets to guide comparative design decisions in evolving IoT ecosystems.