NSA's SPECK128: an exhaustive SAT proof that the minimum weight of 12-round differential characteristics is 66

SPECK is a family of lightweight block ciphers designed by the U.S. National Security Agency (NSA) and standardized in ISO/IEC 29167-22 for RFID. For SPECK128, the minimum weight B_R of a non-trivial R-round XOR-differential characteristic (Lipmaa–Moriai transition probabilities, Markov assumption) is known up to eleven rounds, with B_10 = 49 and B_11 = 58; for twelve rounds a characteristic of weight 66 was known, so 58 ≤ B_12 ≤ 66. We show by an exhaustive SAT computation that no twelve-round characteristic has weight 65 or less, so B_12 = 66, conditional on the published values B_1, …, B_11 that enter Matsui's bounding conditions. The SAT model of Sun, Wang and Wang is split by partial weights into 272 subproblems, all shown unsatisfiable by kissat in 66.1 process-days. Nine further SAT problems show that the split misses no assignment; they and the 89 shortest subproblems carry DRAT certificates verified by drat-trim. We print a weight-66 characteristic and check it inside the same model. A second check with a separately written encoding and a different solver is in progress and will be added in a later version. Files: the preprint (PDF) and the archive (code, per-piece logs, SHA-256 manifest of all solved files, DRAT proofs of the coverage formulas, certification log, model checks, second-encoding scripts). Version 1.0.1 changes only the title, which now states the method; the content is that of version 1.0. Version 1.1 will add the completed re-check with the second encoding and CaDiCaL.