Klasifikace metod pro formální analýzu autentizačních protokolů

Autor: T. Vaněk <vanekt1(at)fel.cvut.cz>, Pracoviště: České vysoké učení technické v Praze, FEL , Téma: Bezpečnost, Vydáno dne: 29. 12. 2008
Je představena klasifikace existujících dostupných metod pro vytváření formálních modelů protokolů se zaměřením na popis BAN logiky a Petriho sítí. V následujících článcích bude popsán protokol TESLA a modifikace BAN logiky k použít pro modelování všesměrových autentizačních protokolů.

Classification of the methods for the formal analysis of authnetication protocols - Abstract:

This article deals with classification of existing methods for formal analysis of the authentication protocols with focus on broadcast authentication protocols. The greatest attention is paid to the BAN logic and Coloured Petri Nets.

Úvod

Kryptografické protokoly jsou konstruovány za účelem zajištění bezpečné komunikace účastníků komunikace přes nezabezpečenou síť. Jedním ze základních cílů, kterých chceme dosáhnout je zajištění autentizace komunikujících stran a integrity přenášených zpráv. Naprostá většina protokolů předpokládá, že účastníky komunikace jsou pouze dvě strany. Existují situace, kdy má smysl uvažovat autentizaci více účastníků současně, resp. komunikaci, kdy se jeden aktivní účastník autentizuje vůči více příjemcům. Typickými aplikacemi, kde se toto schéma může uplatnit, je například distribuce směrovacích informací, které si mezi sebou vyměňují směrovače. Většina směrovacích protokolů (OSPF, EIGRP, IS-IS) využívá vícesměrové (multicastové) vysílání.

Klasifikace nástrojů pro formální analýzu protokolů

C.J. Meadows definuje čtyři základní přístupy, které je možné zaujmout k analýze kryptografických protokolů:
Typ I
Přístup typu I k analýze kryptografických protokolů spočívá v modelování a ověření protokolu pomocí popisných jazyků a ověřovacích nástrojů, které nejsou určeny výhradně pro analýzu takovýchto protokolů. Hlavní myšlenka spočívá v tom, že na kryptografický protokol hledíme jako na jakýkoliv jiný program a snažíme se dokázat jeho správnost. Hlavním nedostatkem tohoto přístupu skutečnost, že prokázáním správnosti protokolu není prokázána bezpečnost protokolu. Mezi nástroje patřící typu I patří jazyky InaJo a LOTOS. Obecnou slabinou přístupů typu I je, že používají metody, které nebyly zamýšleny k analýze bezpečnostních protokolů, takže důvtipnější typy útoků (jako např. útok přehráním zpráv) zde nejsou uvažovány. V praxi se tyto systémy příliš nepoužívají.
Typ II
Přístup Typu II k analýze kryptografických protokolů spočívá ve vývoji expertního systému, který může návrhář použít k vývoji a zkoumání různých scénářů. Tyto systémy začínají s nějakým (z hlediska bezpečnosti) nepřijatelným stavem a zkoumají, zda je tento stav dosažitelný z počátečního stavu protokolu. Tento typ analýzy dokáže identifikovat bezpečnostní chyby lépe než analýzy typu I, ale nedokáže zaručit (stejně jako u analýz Typu I) bezpečnost autentizačních protokolů. Analýzy pomocí nástrojů typu II mohou odhalit, zda daný protokol obsahuje konkrétní bezpečnostní slabiny, ale jsou neschopné odhalit neznámé typy „slabých míst“ v protokolech. Jediný existující expertní systém, který se dnes používá pro analýzu protokolů je Interrogator. Vstupem systému je specifikace protokolu a cílová data. Výstupem je zpráva ukazující postup, jak narušitel může získat tato data. V tomto systému se na protokol nahlíží jako na soubor komunikačních procesů, kde na každého účastníka připadá jeden proces. Interrogator generuje skrz protokol velké množství cest, které končí v konkrétním nebezpečném stavu. Pokud kterákoliv z těchto cest začíná v počátečním stavu, pak se povedlo odhalit slabé místo. Neprokázalo se, že tyto systémy jsou schopné odhalit nové typy útoků nebo útoky na protokoly, které jsou pokládány za bezpečné. Přístupy Typu II k analýze protokolů jsou pouze omezeně použitelné. Systémy využívající tento přístup jsou obvykle neefektivní, často se odvolávají na kompletní vyhledávání prostoru. Výsledky jsou často nepřesvědčivé a systém se ani nemusí nikdy zastavit (pokud je prohledávaný prostor nekonečný). Z tohoto důvodu je hlavní zájem v oblasti analýzy bezpečnostních protokolů věnován přístupu Typu III.
Typ III
Přístup Typu III používá k analýze protokolů formální logické modely vyvinuté pro analýzu znalostí nebo domněnek. Jako první představil Burrows model zvaný BAN logika, který měl za následek rozsáhlý výzkum využívající tento přístup. Základní model BAN logiky byl následně mnohokrát rozšiřován, ale i kritizován.

BAN logika

BAN logika patří mezi doxastické logiky tzn. logiky založené na domněnkách. Doxastická logika je oborem logiky, které zkoumá logickou strukturu víry a přesvědčení tj. pojmy, se kterými klasická výroková ani predikátová logika nedokáže plnohodnotně pracovat. Někdy bývá doxastická logika klasifikována jako podmnožina epistemické logiky (logika poznání) [2]. Doxastické a epistemické logiky se často používají v oborech jako je umělá inteligenci nebo multiagentní systémy tj. tam, kde dochází k interakci více komunikujících stran. Cílem BAN logiky je zodpovězení následujících otázek o zkoumaném protokolu:

Tento systém se zabývá autentizačními protokoly pouze na abstraktní úrovni, neřeší se takové detaily, jako je konkrétní implementace daného protokolu a problémy s tím souvisejícími (množnost uváznutí v mrtvém bodě, nesprávné použití kryptosystému).
Existuje mnoho rozšíření původní BAN logiky. Některá z následujících rozšíření se zaměřila na eliminaci určitých předpokladů původní BAN logiky, jiná se snaží zvětšit dokazovací schopnosti BAN logiky. Kromě zde uváděných rozšíření existují i další, v tomto článku nezmiňovaná.

Základní konstrukce BAN logiky

Jedinou použitou logickou spojkou je konjunkce, která se značí čárkou. Povolené vlastnosti jsou asociativnost a komutativnost.

P believes X   Účastník P je přesvědčen (věří), že tvrzení X je pravdivé. Konstrukce, kdy konkrétní entita něčemu věří, se označuje jako indexovaná doxastická modalita. Je možný i méně častý tvar zápisu ve tvaru „ believe X“ (věří se, že X), který se používá méně často.
P sees X    Někdo poslal účastníkovi P zprávu obsahující X, který ji může přečíst a zopakovat (pokud byla zpráva zašifrována, tak po případném dešifrování).
P said X    V určitém čase účastník P odeslal zprávu obsahující sdělení X. Není známo, kdy byla zpráva odeslána, nebo zda byla odeslána během tohoto běhu protokolu. Platí předpoklad, že P věří o tvrzení X, že je pravda.
P controls X    Účastník P má plnou moc nad X a z tohoto důvodu by měl býtdůvěryhodný. Tato konstrukce se hlavně používá tehdy, když účastník P předal pravomoc nad nějakým tvrzením.
#X   Výraz X je platný neboli čerstvý (fresh). To znamená, že výraz X nebyl odeslán v žádné předešlé zprávě tohoto běhu protokolu. Tento výraz nabývá pravdivé hodnoty pro tzv. nonce, které se generují právě za účelem „čerstvosti“.
(P↔Q)K   Účastníci P a Q mohou ke vzájemné komunikaci používat sdílený klíč K . Klíč K je „v pořádku“ tzn. nikdy ho nemůže zjistit žádný účastník komunikace kromě účastníků P a Q, nebo účastník R, jemuž jeden z účastníků P, nebo Q důvěřuje.
(→P)K   Účastník P vlastní veřejný klíč K. Odpovídající soukromý klíč K-1. nemůže zjistit nikdo jiný než účastník P nebo účastník R, kterému účastník P důvěřuje.
(P<=>Q)K   Zpráva X je tajemství známé pouze P a Q a těm účastníkům, kterým se P a Q rozhodli toto tajemství sdělit. P a Q mohou použít X k tomu, aby si navzájem prokázali svou identitu.
{X}K from P   Tento zápis vyjadřuje zprávu X zašifrovanou účastníkem P pomocí klíče K. Část výrazu „ from P“ se často vynechává, protože se předpokládá, že každý účastník je schopen poznat a ignorovat své vlastní zprávy.

Na základě těchto základních konstrukcí lze vytvářet logické postuláty, kterými lze popisovat komunikační protokoly.

Pravidla odvozování BAN logiky

Pravidlo významu zprávy
Toto pravidlo vyjadřuje, jakým způsobem odvodit důvěru v původ zprávy. Pro symetrické kryptosystémy má tvar:

vanek11
 (1)

kde {X}K má význam zprávy od účastníka Q≠P. Toto pravidlo lze interpretovat větou: Jestliže P věří, že Q a P sdílí tajný klíč K a zároveň P vidí zprávu X, zašifrovanou pomocí klíče K a současně ji účastník P nezašifroval pomocí klíče K, pak účastník P věří, že účastník Q někdy poslal zprávu X.
 
V případě asymetrických kryptosystémů je vzorec možné rozepsat do tvaru

vanek12
 (2)

což znamená: Jestliže P věří, že K je veřejný klíč účastníků P a Q a současně vidí P vidí zprávu X, zašifrovanou pomocí klíče soukromého klíče účastníka Q, pak účastník P věří, že účastník Q někdy v minulosti poslal zprávu X.
 
Pravidlo ověření aktuálnosti zprávy
Toto pravidlo vysvětluje skutečnost, že pokud byla zpráva odeslána v nedávné době, pak příjemce může předpokládat, že odesílatel věří jejímu obsahu a může mu také věřit. Toto jediný postulát, ve kterém se přechází od said k believes a tedy v abstraktní rovině odráží způsob používání výzvy a odpovědi v procesu autentizace. Výsledek aplikace tohoto pravidla ukazuje, že výzvy k autentizaci často nejsou zašifrované, ale odpovědi vždy musejí být zašifrované.
 

vanek13
 (3)

což znamená: Jestliže účastník P věří, že zpráva X je čerstvá a že účastník Q někdy v minulosti poslal zprávu X, pak účastník P věří, že také účastník Q věří zprávě X. Z důvodu zjednodušení autoři BAN předpokládají, že X musí být v otevřeném tvaru, takže nemusí zahrnovat rovnice ve tvaru {Y}k . Toto pravidlo je důležité, protože mnoho protokolů se vyhýbá možnosti útoku přehráním staré zprávy (replay attack) tím, že používají nonce.
 
Rozhodovací pravidlo
Toto pravidlo vysvětluje skutečnost, že účastník P důvěřuje účastníku Q v otázce zprávy X, protože účastník Q vytvořil zprávu X a zaručuje tak její bezpečnost.

vanek14
(4)

což znamená: Jestliže účastník P věří, že účastník Q má v držení zprávu X, a současně účastník P věří, že účastník Q věří zprávě X, pak účastník P také věří zprávě X.
 
Skládací pravidlo
Toto pravidlo říká, že účastník vlastnící správný klíč je schopný dešifrovat přijatou zprávu.

vanek15
 (5)

což znamená: Jestliže účastník P věří, že K je veřejný klíč účastníků P a Q a P vidí zprávu X zašifrovanou pomocí klíč soukromého klíče uživatele Q, pak P je schopný získat otevřený text X.
Pravidlo aktuálnosti zprávy
Toto pravidlo lze aplikovat na jakoukoliv část zprávy:

vanek16
 (6)

což znamená: Jestliže P věří,že část X zprávy je aktuální, pak ostatní části zprávy jsou také aktuální.

Analýza protokolu pomocí BAN logiky

Analýza protokolu, tak jak ji presentují autoři má následující kroky:
vanek17

Obr. 1 Analýza protokolu pomocí BAN logiky

Vstupem systému je specifikace protokolu a počáteční předpoklady. V každém kroku jsou ke zprávám protokolu připojeny předpoklady a poté je buď aplikováno pravidlo, nebo pokud to nelze běh protokolu končí. Pokud je to možné, je dosaženo požadovaného závěru.
Přesněji je protokol v BAN logice vyjádřen jako očíslovaný sled „odeslaných“ příkazů S1...Sn. Každý příkaz má tvar P→Q>X s tím, že P≠Q . Vysvětlení protokolu se skládá z řady tvrzení vložených před první příkaz a po každém příkaze. Tvrzení získám kombinací výrokových formulí P believes Q a P sees Q .
První výrok obsahuje předpoklady, zatímco poslední obsahuje závěry. Celkový zápis má tuto podobu:

vanek18

Analýza protokolu pomocí BAN logiky je shrnuta na obr. 1. Nepoužívá se žádný zápis času. Místo toho je čas rozdělen na minulost a současnost v závislosti na tom, zda bylo v minulém běhu protokolu něco řečeno.

Nevýhody BAN logiky
BAN logika nedokáže vyjádřit žádné matematické operace, proto také nedokáže prokázat ani jejich bezpečnost. Nicméně matematické operace nejsou v reálných protokolech to, co je obvykle špatné, takže neschopnost BAN logiky simulovat samotné matematické operace není příliš na škodu. Navíc jsou v praxi kryptografické (matematické) operace prováděny v bezpečí na straně odesílatele a příjemce, a tím pádem jejich zabezpečení nijak nesouvisí se zabezpečením samotné komunikace. BAN logika není deterministická – stejná zpráva použitá v různých komunikačních protokolech může vést k různým vyjádřením v BAN logice, protože záleží na významu, který zpráva může nabývat s ohledem na použitý protokol. Při modelování protokolu mohou mít také pravidla různý význam v závislosti na kontextu.

Mezi nejznámější modifikace BAN logiky patří:
 
GNY logika - GNY logika nepředpokládá existenci redundance ve zprávách. Místo toho představuje zápis rozpoznatelnosti k vyjádření faktu, že účastník očekává určité informace v obdržených zprávách. Gong a kol. dále jednoznačně vyjadřují stav, kdy účastník generuje zprávu sám pro sebe. Dále GNY logika zavedla rozlišení pojmů důvěra a vlastnictví. V této rozšířené logice každý účastník udržuje množinu důvěry a množinu vlastnictví zpráv.
 
Logika Mao a Boyda - Mao a Boyd popsali čtyři slabá místa (idealizace protokolu, důvěra, předpoklady protokolu a utajení) v BAN logice a předložili návrh nové logiky založené na BAN logice obsahující četná vylepšení. Logika představená Mayem a Boydem vyžaduje striktně psané vzorce a zprávy. Dále je definován nový idealizační postup. Tento postup je zvětší části mechanický a takřka nevyžaduje lidské zásahy.
 
Rozšíření BAN k použití v PKCS - Aby bylo možné analyzovat kryptosystémy veřejného klíče (PKCS), autentizační protokoly využívající certifikáty X.509, přišel Gaarder a Snekkenes s rozšířením BAN logiky. Byly přidány konstrukce k reprezentaci veřejného klíče a času (klasická BAN logika, pojem času vůbec nezavádí). Rozšířená BAN logika je pak použita k dokázání, že protokol plní svůj účel.
 
Typ IV
Přístupy typu IV k analýze protokolů spočívají ve vývoji formálního modelu založeného na algebraických výrazech popisujících kryptografický systém. Přístup typu IV obecně obsahuje analýzu dosažitelnosti určitých stavů systému. Z tohoto pohledu je tento přístup podobný Typu II. Nicméně přístup Typu IV se pokouší ukázat, že nelze dosáhnout nebezpečného stavu, zatímco přístup Typu II začíná v nebezpečném stavu a snaží se dokázat, že neexistuje cesta z nebezpečného stavu do výchozího bezpečného stavu. Do této patří logiky Dolev-Yao, KPL, CKT-5, NLR a Petriho sítě.
 
Petriho sítě
Petriho síť (obr. 2) je nástroj pro modelování a analýzu systémů diskrétních událostí. Můžeme si ji představit jako ohodnocený graf se dvěma typy uzlů (tzv. místa a přechody) a násobnými hranami. Orientované hrany jsou vždy pouze mezi uzly různých typů. Hrany určují logické vazby mezi místy a přechody. Mezi místy se přes přechody předávají značky neboli tokeny. Tokeny představují dynamickou část systému a reprezentují jeho aktuální stav. Tokeny mohou při splnění určitých podmínek mezi jednotlivými stavy přecházet. Pokud je přechod uskutečněn, token se přemístí do každého místa, které je s uskutečněným přechodem spojeno orientovanou hranou.

vanek19

Obr. 2 Petriho síť – základní pojmy

Barvené Petriho sítě

Barvené Petriho sítě (Colored Petri Nets - CPN) jsou graficky orientovaný jazyk pro návrh, specifikaci, design a prověření systému. Jsou užitečné pro systémy s velkým počtem procesů, které spolu komunikují a jsou na sobě závislé. Typickým příkladem využití CPN je modelování komunikačních protokolů, distribuovaných systémů a automatických produkčních systémů. CPN vznikly kombinací klasických Petriho sítí a vyšších programovacích jazyků. Petriho síť poskytuje možnosti pro interakci s procesem, zatímco programovací jazyk poskytuje možnost pro definici proměnných a manipulaci s jejich hodnotami. Klasické Petriho sítě nedokáží rozlišit jednotlivé tokeny od sebe. V barvených Petriho sítích lze jednotlivé tokeny rozlišit „barvou“, díky čemuž je možné v jednom stavu uchovávat více různých tokenů. Barva tokenu pak představuje další parametr, který ovlivní, zda-li dojde k přechodu. CPN mají dvě prostředí pro práci s vytvořeným modelem. Grafické rozhraní realizované grafem Petriho sítě slouží k modelování samotné struktury sítě. Pomocí tohoto modelu můžeme lehce pochopit a znázornit, jak spolu jednotlivé procesy komunikují a uvědomit si návaznosti jednotlivých částí systému na jiné části. Tato reprezentace je mnohem jednoduší na pochopení a demonstraci systému. Druhý model se označuje jako inskripční (popisný). Tato reprezentace má přesně danou strukturu a syntaxi. Pomocí matematických definic můžeme přesně definovat chování jednotlivých proměnných a pomocí tohoto jazyka jsou popsány i metody pro analýzu modelu. Popis realizovaný inskripčním jazykem (např. CPN ML language) obsahuje:

CPN model může být analyzován ve dvou stavech vzhledem k času jako časově závislý nebo časově nezávislý. Časově nezávislý model se používá hlavně pro ověření logické správnosti a funkčnosti modelu. Tím si ověříme, že části systému spolu komunikují tak, jak jsme předpokládali, a nedochází nikde třeba k zacyklení zpráv. Časově závislý model slouží k ověření výkonnosti systému. Díky tomuto dělení můžeme náš systém velmi dobře analyzovat a odstranit případné problémy, či zvýšit jeho výkonnost a optimalizovat ho pro požadované funkce. Mezi hlavní přednosti systémů na bázi CPN patří:

V CPN je možné použít tentýž model pro více činností:

Podle výzkumu, který provedl Rubin & Honeyman [1], je nejméně oblíbený přístup Typu I a nejčastěji používaný je Typ III. Tyto dva přístupy mají několik společných vlastností. Ve všech případech jsou použité metody nezávislé na podložním kryptografickém mechanismu. Na základě srovnání existujících a dostupných metod jsem dospěl k závěru, že žádná z popisovaných metod nich není přímo vhodná k modelování všesměrových autentizacích protokolů. Proto jsem se zaměřil na BAN logiku, a vhodnou modifikací jejích základních postulátů jsem ji pozměnil tak, aby jí bylo možné vyžít pro modelování všesměrových autentizačních protokolů.

Tento příspěvek vznikl v rámci výzkumného záměru MSM6840770038

Literatura

[1] Rubin, A. – Honeyman,P.: Formal Methods for the Analysis of Authentication Protocols, CITI Technical Report 93-7, 1997
[2] John-Jules Ch. Meyer: Modal epistemic and Doxastic Logic. pp. 1-38, "Handbook of Philosophical Logic", Springer 2004, ISBN 1402016441
[3] E. Snekkenes. Formal Specification and Analysis of Cryptographic Protocols. PhD thesis, University of Oslo, Norway, 2005.
[4] Bolignano D., An approach to the formal verification of cryptographic protocols, Proceedings of the Third ACM Conference on Computer and Communications Security, 1996, 106-118, ACM Press.