Sulla Crittoanalisi Logica e il Cifrario Leggero SIMECK

La crittografia rappresenta il fondamento della sicurezza informatica moderna, proteggendo comunicazioni, transazioni e infrastrutture digitali di uso quotidiano. In questo contesto, il presente elaborato esplora l’applicazione della crittoanalisi logica al cifrario leggero SIMECK, con l’obiettivo di valutare la capacità dei moderni solver SAT di analizzare la sicurezza strutturale di cifrari a bassa complessità. L’attività di ricerca si è concentrata sulla creazione e l’utilizzo della libreria Esther, un tool in Python progettato per automatizzare la conversione di circuiti booleani in formule logiche in forma normale congiuntiva (CNF) mediante la codifica di Tseitin, rendendo possibile la risoluzione tramite solver SAT di ultima generazione. Dopo aver descritto la struttura modulare della libreria e le sue componenti principali, è stata sviluppata una pipeline di crittoanalisi che consente di modellare il comportamento di SIMECK a livello di round, chiavi e coppie plaintext–ciphertext. Gli esperimenti sono stati condotti su varianti a 32 bit, considerando due modalità operative: round-key indipendenti (analisi strutturale) e master-key vincolata (analisi crittanalitica). I risultati hanno evidenziato un’elevata efficienza dei solver CaDiCaL e Glucose nella risoluzione delle istanze più semplici, con tempi di solving dell’ordine dei millisecondi, mentre la complessità cresce significativamente nelle configurazioni con vincoli di key schedule. Ciò conferma la sensibilità della riduzione SAT alla densità dei vincoli e alla propagazione unitaria. La tesi dimostra come l’approccio SAT possa costituire uno strumento efficace e automatizzabile per la valutazione logica della sicurezza dei cifrari leggeri, offrendo al contempo una base metodologica per lo sviluppo futuro di tecniche di analisi combinatoria più avanzate e generalizzabili.