enigmaZ3

Descrizione del Progetto

Simulatore storicamente accurato della macchina Enigma della Wehrmacht e sistema di crittoanalisi automatica basato su SMT solving (Z3) con fallback numerico. Il progetto nasce con un duplice obiettivo: riprodurre fedelmente il funzionamento della macchina Enigma a 3 rotori — incluso il meccanismo di double-stepping, ring settings, plugboard e riflettore — e automatizzare la crittoanalisi dato un testo cifrato e un crib (frammento di testo in chiaro noto).

Il cracker trova automaticamente la configurazione della macchina (posizioni rotori, coppie plugboard, ordine rotori, ring settings) utilizzando un approccio ibrido: prima il solver simbolico Z3, poi un fallback brute-force deterministico con passo primo (7919) per evitare pattern e massimizzare la copertura con budget limitato.

Architettura

Il progetto è organizzato in due package indipendenti:

• enigma/ — Simulatore puro della macchina Enigma con classi Rotor, Reflector, Plugboard, SimpleEnigma (1 rotore, fase didattica) e EnigmaMachine (3 rotori, storicamente accurata)
• cracker/ — Sistema di crittoanalisi a 4 livelli incrementali di complessità:
  • crack_rotor_positions() — trova le posizioni dei rotori (plugboard noto)
  • crack_with_plugboard() — trova posizioni + coppie plugboard ignote via backtracking
  • rank_rotor_configurations() — ranking euristico con ordine rotori e ring settings ignoti
  • crack_full_configuration() — ricerca completa con raffinamento numerico

Il progetto include due interfacce utente: enigma_cli.py, una CLI unificata con comandi encrypt, decrypt, crack (output JSON) e benchmark (output CSV + PNG); e interactive_demo.py, una demo interattiva a terminale con colori ANSI e trace lettera-per-lettera del segnale attraverso la macchina, pensata per presentazioni orali.

Aspetti Tecnici Rilevanti

• Strategia ibrida di solving: Z3 tenta prima una risoluzione simbolica intelligente; se va in timeout, un fallback numerico deterministico esplora lo spazio con un cammino pseudo-random (passo primo 7919) per massimizzare la copertura con budget limitato
• Modellazione simbolica completa: l'intero percorso del segnale Enigma (plugboard → rotori → riflettore → rotori inversi → plugboard) è codificato come catena di espressioni Z3 con If-Then-Else per i lookup nelle tabelle di wiring
• Double-stepping: il simulatore implementa correttamente l'anomalia meccanica del doppio avanzamento del rotore centrale, fedele al comportamento della macchina storica

Approccio di Sviluppo

Il progetto è stato costruito in 6 fasi incrementali: simulatore base a 1 rotore, proof-of-concept Z3, Enigma completa a 3 rotori, cracker Z3 completo, benchmark con grafici, documentazione e CI.