Formální ověřování kryptografických protokolů je ověřování kryptografických protokolů pro zajištění požadovaných bezpečnostních vlastností. Jednou ze součástí takové kontroly je určení odolnosti protokolu vůči útokům za předpokladu spolehlivosti kryptografických primitiv , na kterých je založen. K vyřešení tohoto problému byla vyvinuta řada přístupů založených na různých formálních verifikačních metodách . Společným znakem formálních metod je použití systematického přístupu k problému, který umožňuje provádět rozumnější, přesnější a efektivnější kontrolu bezpečnostních vlastností protokolu.
Termín formální ověřování kryptografických protokolů poprvé zavedla Catherine Meadows [ 1] - hlavní výzkumnice Angličanů. Center for High Assurance Computer Systems (CHACS) [2] a Naval Research Laboratory (NRL).
Při ověřování kryptografických protokolů je vedle kontroly tradičních vlastností, které zaručují správné fungování distribuovaných systémů, věnována zvýšená pozornost také zdůvodnění speciálních vlastností informační bezpečnosti . Nejdůležitější z těchto vlastností jsou následující vlastnosti:
Přesná matematická definice těchto vlastností v podstatě závisí na formálním modelu , v jehož rámci je kryptografický protokol popsán. Při ověřování kryptografických protokolů se obvykle vycházejí z následujících předpokladů o schopnostech protivníka:
Proto, aby byla zajištěna důvěrnost a integrita informací, musí být protokol navržen tak, aby žádný protivník nemohl získat dostatek informací ze zachycených zpráv k provedení zamýšlené hrozby.
Stavové stroje lze použít k analýze kryptografických protokolů. V tomto případě se použije technika známá jako technika analýzy dosažitelnosti. Tato technika předpokládá popis systému v následující podobě. Pro každý přechod je sestaven globální stav systému, který je vyjádřen prostřednictvím stavů entit systému a stavů komunikačních kanálů mezi nimi. Každý globální stav je poté analyzován a jsou určeny jeho vlastnosti, jako je uváznutí a správnost. Pokud entita nemůže přijmout zprávu a ta měla být přijata v tomto stavu, pak je problém v protokolu.
Technika analýzy dosažitelnosti je účinná při určování správnosti protokolu vůči jeho specifikacím, ale nezaručuje bezpečnost proti aktivnímu útočníkovi.
Existuje automatická kompletní metoda pro ověření vlastností důvěrnosti kryptografických protokolů. Metoda je založena na robustní abstraktní interpretaci kryptografických protokolů, která využívá rozšíření stromových automatů , konkrétně V-parametrizované stromové automaty, které mísí autoteoretické techniky s rysy deduktivních technik. Na rozdíl od většiny přístupů kontroly modelů nabízí tato metoda de facto záruky bezpečnosti. Je popsána možnost analýzy protokolů za přítomnosti paralelních principů více relací.
Kryptografický protokol vystavený protivníkovi se nazývá označený hopping systém (LTS). Každý stav LTS je reprezentován dvojicí (S,K) , kde S je stav výpočtu protokolu a K jsou znalosti dostupné protivníkovi. Přechody na LTS se provádějí na základě specifikace protokolu a předpokladů o schopnostech protivníka (model protivníka). V důsledku přechodů se mohou změnit jak stavy výpočtu protokolu, tak znalosti o nepříteli. Některé přechody mohou být označeny akcemi, které se na přechodu provádějí. Vlastnost protokolu, která se má zkontrolovat, je určena logickým vzorcem. K tomuto účelu mohou být vhodné časové logiky , logiky znalostí atd . Verifikace kryptografických protokolů se tak redukuje na klasickou úlohu matematické logiky - kontrolu proveditelnosti vzorce na modelu. Kontrola mnoha vlastností spočívá v kontrole dosažitelnosti určitých stavů v LTS; K vyřešení tohoto problému bylo vyvinuto mnoho algoritmů. Výhodou tohoto přístupu je jednoduchost a univerzálnost a také možnost využití četných nástrojů pro řešení problému verifikace modelu. Největším problémem při testování skutečných protokolů je to, že LTS mohou mít neomezený počet stavů. K překonání této obtížnosti se používají symbolické metody pro reprezentaci modelů, metody pro stavbu modelu za běhu (on-the-fly), různé typy abstrakce dat.
Popis (specifikace) protokolu je reprezentován jako formule Spec nějakého formálního logického jazyka. Popis schopností protivníka a testované vlastnosti protokolu představují také vzorce Φ a Ψ . Verifikační problém se redukuje na kontrolu odvoditelnosti vzorce Ψ ze vzorců Spec a Φ . Hlavní výhodou tohoto přístupu je, že umožňuje kontrolovat potřebné vlastnosti pro iterativní protokoly bez ohledu na počet kol jejich provedení. Nevýhodou je, že konstrukce nátisku je většinou velmi pracná a nelze ji plně automatizovat. Konstrukce takového důkazu obvykle spočívá ve vytvoření speciálního systému omezení, ve kterém se spolu s protokolovým zařízením berou v úvahu znalosti a schopnosti protivníka, a kontrola řešitelnosti tohoto systému omezení. .
V případě, kdy je specifikační jazyk kryptografických protokolů vybaven formální operační sémantikou (jako je tomu v případě spi-kalkulu ), lze na množině protokolů zavést vztah ekvivalence stop nebo bisimulace ≈ . Pak pro kontrolu některých vlastností daného parametrizovaného protokolu P(M) stačí ověřit, že pro jakýkoli proces A vystupující jako protivník platí ekvivalence A|P(M)≈A|P(M ) . V tomto případě se říká, že procesy P(M) a P(M′) jsou ve vztahu ekvivalence testu. Bylo zjištěno, že úkoly kontroly důvěrnosti a integrity vlastností protokolů jsou redukovány na úkol kontroly testovací ekvivalence spi-procesů . Byl navržen algoritmus pro kontrolu testovací ekvivalence procesů spi bez replikace . Hlavním rysem tohoto problému je, že ekvivalenci A|P(M) ≈ A|P(M ) je třeba zkontrolovat pro libovolný proces A (protivník), což vede k potřebě analyzovat nekonečně velkou množinu výpočtů. konečné délky. Bylo poznamenáno, že pro efektivní kontrolu ekvivalence testů je nutné vyvinout metody pro symbolickou reprezentaci a analýzu nepřátelských znalostí. V této poznámce navrhujeme alternativní metodu pro reprezentaci a analýzu nepřátelských znalostí, kterou lze použít k testování testovací ekvivalence procesů spi-kalkulu .
Nejnovějším přístupem k analýze formálního protokolu je použití metody kontroly typu, kterou zavedl Abadi . Abadi zavedl typ nedůvěryhodný (Un) pro otevřené zprávy, které pocházejí od oponenta (jako oponenti vystupují všichni kromě ověřujících principálů). V metodě kontroly typu jsou zprávám a kanálům přiřazeny typy (například datová položka soukromého typu se objeví na veřejném kanálu). Metoda typové kontroly má podstatnou výhodu v tom, že je stejně jako metoda modelové kontroly plně automatická, ale na rozdíl od druhé je schopna pracovat s několika třídami nekonečných systémů. Má však potenciální nevýhodu v tom, že vzhledem k tomu, že narušení bezpečnosti jsou definována z hlediska typových nekonzistencí, musí být dokazované bezpečnostní požadavky uvedeny ve specifikaci tak, jak je napsána. To odlišuje metodu kontroly typu od metody kontroly modelu, pro kterou lze nezávisle specifikovat jakoukoli bezpečnostní vlastnost, kterou lze vyjádřit pomocí časové logiky, poté, co byl specifikován samotný protokol.
Existuje technika pro automatické ověřování kryptografických protokolů založená na přechodné reprezentaci protokolu pomocí sady Hornových frází (logický program). Tato technika umožňuje ověřit bezpečnostní vlastnosti protokolů, jako je důvěrnost a autentizace , plně automatickým způsobem. Důkazy získané s jeho pomocí jsou navíc správné pro neomezený počet protokolových relací.
Pro ověření programu je určena metoda zdůvodnění na základě nejslabšího předpokladu (Weakest Precondition usuzování). Tato technika bere v úvahu tři složky: stav před provedením programové instrukce, samotnou programovou instrukci a cíl, který musí být pravdivý po provedení instrukce. Nevýhodou této techniky je obtížnost dokazování složitých predikátů . U dlouhých programů s mnoha cíli nemusí být důkazy možné. V práci věnované integrovanému prostředí CPAL-ES (Cryptographic Protocol Analysis Language Evaluation System) je k ověření použita metoda „nejslabšího předpokladu“. Protože kryptografické protokoly bývají krátké, byla tato metoda úspěšně aplikována na tyto protokoly.
AVISPA Cryptographic Protocol Automatic Verifier, který obsahuje nástroj TA4SL, je schopen analyzovat omezený i neomezený počet protokolových relací pomocí OFMC , CL- ATSE a SATMC . AVISPA se dobře hodí pro analýzu vlastností zabezpečení v případě omezeného počtu relací. Pro neomezené relace poskytuje AVISPA pouze omezenou podporu. Například použití AVISPA je zvláště problematické, pokud nejsou žádné stopy po útoku.
Nástroj pro automatické ověřování kryptografických protokolů ProVerif, který implementuje metodu logického vyvozování, umožňuje analyzovat neomezený počet protokolových relací pomocí horní aproximace a protokolové reprezentace pomocí Hornových výrazů .
ProVerif vám umožňuje automaticky kontrolovat vlastnost soukromí , vlastnost autentizace , zpracovávat mnoho různých kryptografických primitiv, včetně kryptografie sdíleného a veřejného klíče (šifrování a podpis ), hashovacích funkcí a dohody o klíči Diffie-Hellman , specifikované jak v pravidlech přepisu, tak v tvar rovnic.
ProVerif dokáže zpracovat neomezený počet protokolových relací (dokonce i paralelně) a neomezený prostor zpráv, umožňuje specifikovat model protokolu v termínech blízkých modelované předmětové oblasti a ve většině případů poskytuje příležitost získat tu či onu odpověď o vlastnosti protokolu. Mezi nevýhody ProVerif patří skutečnost, že tento nástroj může indikovat falešné útoky a také vyžaduje úzkou interakci s uživatelem a hluboký vhled do podstaty problému při ověřování protokolů.
Automatický ověřovatel kryptografických protokolů společnosti Scyther využívá symbolickou analýzu kombinovanou s obousměrným vyhledáváním na základě částečně uspořádaných vzorů a ověřuje omezený a neomezený počet relací protokolu.
V přístupu Scyther je protokol definován jako sekvence událostí, kde události zahrnují jak přenos zpráv vyměňovaných účastníky relace, tak zprávy, které může vložit útočník. Zápis se používá k rozlišení mezi "vlákny" (oddělená provedení události).
Scyther nevyžaduje zadání útočného skriptu. Je pouze nutné nastavit parametry, které omezují buď maximální počet běhů, nebo prostor trajektorií, které mají být iterovány.
Nástroj FDR2, který je založen na metodě kontroly modelu, používá notaci CSP (Communicating sekvenční procesy) k popisu chování účastníků protokolu. Každý účastník protokolu je modelován jako proces CSP, který buď čeká na zprávu, nebo zprávu odesílá. Kanály se používají ke komunikaci mezi procesy a simulaci protivníků. Protivník je popsán jako paralelní složení několika procesů, jeden pro každou skutečnost nebo zprávu, ze kterých může získat nějaké informace o provedení protokolu. FDR2 používá přístup nazývaný kontrola modelu zpřesnění . Spočívá v potvrzení, že model, který popisuje chování systému, který implementuje testovaný protokol, je ekvivalentní modelu, který specifikuje bezpečnostní požadavky pro tento protokol.