Beyond the  \(\mathcal {U}\) -Method: Automating the Search for UID-Based Contradictions with Constraint Programming

Impossible differential (ID) and zero-correlation (ZC) linear distinguishers are key tools for evaluating symmetric primitives. Word-level automated searches typically enforce miss-in-the-middle contradictions via deterministic truncated propagation, most often within the classical \(\mathcal {U}\) -method. However, existing constraint programming (CP) encodings track only a very limited set of composite patterns, typically no more than \(\textsf{N}\oplus \textsf{N}^{*}\) . This restriction prevents a systematic automation of UID reasoning, even though UID-based contradictions often drive the longest known distinguishers for generalized Feistel constructions. In this paper, we go beyond the \(\mathcal {U}\) -method by proposing a generic CP framework that automates the discovery of UID-based contradictions. Our central idea is a refined word-level representation that separates deterministic, nonzero-but-undetermined, and fully undetermined components, while encoding their provenance (the round index and the responsible F-function) via a power-of-two decomposition. This representation supports the propagation of arbitrary linear combinations over the basic patterns \(\textsf{Z}\) , \(\textsf{N}\) , \(\textsf{N}^{*}\) , and \(\textsf{U}\) , and enables UID inconsistencies to be detected through XOR-aggregated constraints over automatically selected subsets of branches. We instantiate the framework on a broad range of generalized Feistel structures and ciphers, recovering the best-known ID and ZC distinguishers and further obtaining a new 18-round ZC linear distinguisher for Four-Cell. We also show that UID-based contradictions can arise in SPN designs by applying our model to SKINNY, where we identify new UID-type contradictions underlying previously known 12.5-round ID and 11.5-round ZC linear distinguishers. These results demonstrate the practical value of UID-aware automation beyond the \(\mathcal {U}\) -method.