Advanced Metering Infrastructure (AMI) connects smart meters, data concentrator units, and utility control centers through persistent two-way communication. This architecture improves demand response and distributed-energy management, but it also exposes resource-constrained meters to replay, false-data injection, physical extraction, and long-term key compromise. This article develops a formally verified and statistically evaluated lightweight AMI authentication and key agreement protocol for resource-constrained smart-grid deployments. We first reconstruct the AMI authentication workflow as a four-message lightweight authenticated key exchange and map each entity, message, and key dependency to a smart-grid deployment model guided by NISTIR 7628 and IEC 62351. We then identify replay-within-window exposure, insufficient responder freshness, weak identity-to-key binding, missing key-compromise impersonation protection, and retrospective session-key recovery. To address these weaknesses, we propose AMI-AKE, a transcript-bound protocol using ephemeral Curve25519 contributions, session identifiers, nonce and timestamp binding, binding signatures, and separate key-derivation function (KDF) outputs for encryption and integrity. ProVerif-style verification queries and an extended Canetti-Krawczyk (eCK)-oriented game proof are provided for mutual authentication, secrecy, forward secrecy, and key-compromise impersonation (KCI) resistance. A Contiki-OS and ARM Cortex-M4 benchmark with 1,000 repeated trials reports 18.4 +/- 1.2 ms authentication latency, 542 +/- 9.1 sessions/s throughput, and 99.2 +/- 0.4% false-data-injection detection under controlled prototype conditions. The proposed design replaces subjective security labels with objective metrics, confidence intervals, and a reproducible simulation plan for 1,000-10,000 smart meters.