Abstract-Block chiffer som AES är deterministiska, nyckelfärdiga funktioner som fungerar på små, fasta block. Block-chiffer driftlägen definierar en mekanism för probabilistisk kryptering av godtyckliga längdmeddelanden med hjälp av någon underliggande block chiffer. Ett driftsätt kan bevisas säkert (säg, mot valda-plaintext attacker) baserat på antagandet att den underliggande block chiffer är en pseudorandom funktion. Sådana bevis är dock komplexa och felbenägna och måste göras från grunden när ett nytt arbetssätt utvecklas. Vi föreslår ett automatiserat tillvägagångssätt för säkerhetsanalys av block-chiffer driftssätt baserat på en "lokal" analys av de steg som utförs av läget vid hantering av ett enda meddelandeblock. Vi modellerar dessa steg som en riktad, acyklisk graf, med noder som motsvarar instruktioner och kanter som motsvarar mellanvärden. Vi introducerar sedan en uppsättning etiketter och begränsningar på kanterna, och visar en meta-teori som visar att alla lägen för vilka det finns en märkning av kanterna som uppfyller dessa begränsningar är säkra (mot valda-plaintext attacker). Detta gör att vi kan minska säkerheten för ett givet läge till ett begränsningstillfredsställelse problem, som i sin tur kan hanteras med hjälp av en SMT lösare. Vi kopplar ihop vårt säkerhetsanalysverktyg med en rutin som automatiskt genererar livskraftiga lägen; tillsammans gör dessa det möjligt för oss att syntetisera hundratals säkra lägen.
En sådan automatiserad synthesizer för block chiffer driftsätt har publicerats REF, men deras metod för att bevisa säkerheten i systemet skiljer sig i grunden från vår.
Automated Analysis and Synthesis of Block-Cipher Modes of Operation
{'venue': '2014 IEEE 27th Computer Security Foundations Symposium', 'journal': '2014 IEEE 27th Computer Security Foundations Symposium', 'mag_field_of_study': ['Computer Science']}