Logika GNY pro analýzu autentizačních protokolů

GNY Logic Used to Analyse of Authentication Protocols. Tento článek pojednává o jedné z autentizačních logik, a to GNY logice. Jsou zde uvedeny jedny z nejdůležitějších zpráv používaných touto logikou a její porovnání s další často využívanou logikou - BAN.

---

GNY Logic Used to Analyse of Authentication Protocols

Abstract

This article discourses about one type of authentication logics - GNY Logic. There are some of the most important messages used by the logic and comparison of them with other frequently used logic - BAN.

Keywords: logic; GNY; authentication; protocols

---

Úvod

Pro analýzu bezpečnosti autentizačních protokolů vytvořili Michael Burrows, Martín Abadi a Roger Needham autentizační logiku, tzv. BAN-logiku. V této logice jsou přesně uvedeny předpoklady protokolu, typy jednotlivých podniknutých kroků v dané oblasti znalostí a konečný stav každého účastníka. Přestože je protokol nejčastěji popisován pomocí zasílání zpráv, je obvykle velmi užitečné k použití jeho popisu využít formální logiky. Pro BAN logiku je typické používání zpráv, které účastník mohl obdržet. Nicméně BAN logika má své meze. Například samotný text zprávy lze považovat za irelevantní, neboť si jej může kdokoliv přečíst. Další nevýhodou je, že v BAN logice nelze zobrazit hash funkce. K detailnějšímu pochopení pravidel BAN logiky doporučuji článek „Klasifikace metod pro formální analýzu autentizačních protokolů“ - viz odkaz http://access.fel.cvut.cz/view.php?cisloclanku=2008120012.
Nevýhody a nedostatky se snaží odstranit GNY logika [1]. Tato logika byla navržena Gangem, Needhamem a Yahalomem zejména kvůli zvýšení použitelnosti BAN logiky. GNY zamýšlí stupňovitou analýzu protokolů, klade silný důraz na odloučení mezi obsahem a významem zpráv.
Nevýhodou GNY logiky je její větší komplikovanost, než je tomu u ostatních metod, a proto je zde použito mnoho pravidel, která se musí v každém stupni kontrolovat.

Logika GNY

Popis protokolu pomocí GNY logiky je výraznější nežli je tomu v případě již zmíněné BAN logiky. GNY logika je tvořena jasnějšími předpoklady než jsou ty, které jsou implicitně používané v BAN logice. Například v BAN logice se předpokládá, že je pro šifrované zprávy redundance poskytnuta dostatečně, což ovšem v reálném případě nemusí být splněno za všech okolností a v některých případech je též výhodou specifikovat redundanci explicitně. Velký počet protokolových chyb je způsoben právě nekorektními předpoklady. Například v Needham-Schroederově protokolu je využit předpoklad, že vytvořené zprávy obsahují jen relace vytvořené pomocí čerstvě vygenerovaného klíče, což ovšem nemusí být vždy pravda. Dalším neméně důležitou podmínkou je vytvoření jednoznačných předpokladů, které poté slouží k přesnějšímu a korektnějšímu fungování protokolů. V GNY logice jsou předpoklady vytvářeny přesně podle tohoto uvedeného popisu. Nově definované pojmy jsou zde proto, aby bylo možné definovat i jiné funkce nežli šifrování, dešifrování jednosměrnou hash funkcí a definice soukromého a veřejného klíče. Velký počet nových pravidel v této logice je vytvořen proto, aby mohlo být využito nových kryptografických technik, a ty pak mohly být využity ke konstrukci nových bezpečnějších protokolů [7].

Jednotlivé druhy zpráv používaných v GNY logice

Obr. 1 Jednotlivé druhy zpráv používaných v GNY logice

Nejzřetelnější rozdíl GNY logiky oproti BAN logice

Zprávy použité podle pravidel BAN logiky přepokládají, že pro redundanci existuje ve zprávě dostatečný prostor, a proto po použití korektního dešifrovacího klíče na šifrovaný text dostane účastník správně dešifrovanou zprávu. GNY logika ovšem toto nepředpokládá. Zavádí nové prohlášení:

(1)

Toto prohlášení definuje tvrzení, že účastník P je přesvědčen, že zpráva X je rozpoznatelná. Neboli P očekává rozpoznatelnost zprávy již před tím, nežli samotnou zprávu přijme. BAN logika dále předpokládá důvěryhodné provedení principů protokolů. V GNY logice, pokud chceme použít pojem explicitní důvěry, zavádíme prohlášení:

(2)

Toto prohlášení znamená, že účastník P věří, že účastník Q je čestný.

Analýza protokolu pomocí GNY logiky

Prvním krokem, stejně jako při použití BAN logiky, je vytvoření logického popisu protokolu namísto předchozího konvenčního vyjádření funkce daného protokolu. Narozdíl od BAN logiky jsou v případě GNY logiky zachovány zprávy v podobě prostého textu. To poté umožňuje nadále uvažovat obsahový princip protokolu. Implicitní informace předávané během protokolu jsou zastoupeny logickou formulí reprezentující se jako určitý typ zprávy. Navíc při zaslání každé hlavní zprávy, je použito i označení * (not-originated-here), který značí že tato část zprávy ještě nebyla v dřívější době zaslána. [1]
V případě BAN logiky je předpokládáno, že vlastní vygenerované zprávy mohou být ignorovány. Tato podmínka je patrná především z pravidel týkajících se pravidel pro použití sdíleného klíče. GNY atribut * udává možnost logicky vyjádřit tento požadavek pro zprávy generované při současném spouštění protokolů. Toto vyjádření může být například takovéto:

(3)

Rozšíření

(4)

označuje tvrzení, které je vyvoláno implicitně danou zprávou.
V dalších krocích je GNY logika podobná BAN logice. Oproti BAN logice je ovšem GNY logika často rozšířena o funkci dvou konzistentních kontrol protokolu. Obsahová konzistence protokolu a ověřovací konzistenci protokolu. Obsahová konzistence protokolu slouží pouze ke kontrole zpráv, které jsou vytvořeny před odesláním. Naopak ověřovací konzistence vyžaduje, aby zprávy obsahovaly i rozšíření týkající se očekávání účastníka ještě před odesláním samotné zprávy. Kontroly konzistence ovšem nemohou být prováděny samotnou GNY logikou, ale mohou být provedeny pouze pomocí znalostí o kontrolách. Z toho důvodu zatím nebyly tyto konzistentní kontroly zahrnuty do automatizované logiky [5] [6] [8].

Modifikace pravidel BAN logiky pro GNY logiku

V tomto odstavci jsou uvedeny modifikace některých zpráv BAN logiky. Zmíněná modifikace se provádí především proto, aby byly odstraněny nedostatky BAN logiky a využito výhod GNY logiky. Nejprve si tedy rozebereme následující zprávu z BAN logiky značící, že účastník P věří v obsah a čerstvost zprávy X:

(5)

V GNY logice je tato zpráva nahrazena dvěmi zprávami:

(6)

Zde tedy první zpráva uvádí, že účastník P věří v čerstvost zprávy X druhá zpráva GNY logiky značí, že účastník P věří obsahu zprávy X [4]. Na tomto příkladu je uveden princip modifikací zpráv BAN logiky použitých v GNY logice. Základním účelem použití GNY logiky je získání obsahu zpráv a důvěra v ostatní účastníky komunikace, kterou je možné získat z obsahu předchozích zpráv. Vzhledem k tomu, že obsah zprávy není závislý na důvěře mezi účastníky, nemá na úsudek účastníka přijímacího zprávu pravidlo týkající se čerstvosti zprávy žádný vliv, důležitý je zde tedy fakt důvěry mezi účastníky [3]. Pravidlo, které umožňuje získání účastníkovi P důvěry z obsahu zprávy, lze popsat následujícím vztahem:

(7)

Tento zápis tedy značí, že účastník P získá ze zprávy důvěru k účastníkovi Q. Proto tedy označení

(8)

značí, že uživatel P získá důvěru od ostatních účastníků, ovšem pouze pokud budou platit následující pravidla:

Pravidlo číslo 1:

(9)

Neboli:

Účastník P přijímá zprávu X šifrovanou klíčem K, které po ověření důvěryhodnosti předává účastníkovi C. Účastník P vlastní šifrovací klíč a věří zabezpečení komunikace mezi ním a účastníkem Q. [1]

Pravidlo číslo 2:

(10)

Neboli:

Účastník P přijímá klíč S, dále ještě šifrovaný pomocí veřejného klíče K a následně jej zasílá účastníkovi C. Účastník P je vlastníkem klíčů šifrovacího klíče S a dešifrovacího klíče K. P důvěřuje šifrování pomocí veřejného klíče. [1]

Pravidlo číslo 3:

(11)

Neboli:

Účastník P přijímá od účastníka H zprávu X zašifrovanou klíčem S, této zprávě důvěřuje. Účastník P vlastní šifrovací klíč S a zprávu X a důvěřuje komunikaci s účastníkem Q šifrované klíčem S. [1]
Jako předpoklad těchto pravidel je nutnost předpokladu čerstvosti jednotlivých formulí.

Nově přidaná pravidla do GNY logiky

Do GNY logiky jsou oproti BAN logice přidána tři nová pravidla, která umožňují rozšíření možností zpráv popisující komunikaci v určitém typu kryptografických protokolů. Tato přidaná pravidla popisují triviální závěry, které jsou obvykle správné, ale nikdy nejsou v případě BAN logiky popisovány během komunikace protokolu. Následující dvě pravidla pouze rozšiřují vlastnosti GNY logiky [2].

(12)

Poslední, třetí, pravidlo je následující:

(13)

Toto pravidlo umožňuje další šíření zpráv, toto šíření je umožněno konjunkcí jedné nebo více zpráv [1].

Závěr

K autentizaci kryptografických protokolů se v současné době využívá nepřeberné množství logik. Jako jedna z prvních, velmi často vyžívaných autentizačních logik, byla BAN logika. Časem byly ale zjištěny některé nedostatky této logiky, čímž poté nedocházelo ke správné autentizaci některých druhů kryptografických protokolů. Byly proto vyvinuty další logiky, které odstraňovaly nedostatky dříve používaných logik. Jednou z nich je i GNY logika, kterou jsem se v tomto článku snažil popsat a uvést některé její nejdůležitější v ní užívané zprávy. V některém z dalších článků bude ukázána aplikace GNY logiky na některý z kryptografických protokolů.

Literatura

[1] MATHURIA, A.M., SAFAVI-NAIVI, R., NICKOLAS, P.R.. Eprints.kfupm.edu.sa/54733/1/54733.pdf [online]. 1995 [cit. 2010-02-24]. Dostupný z WWW:
[2] L.Gong, R. Needham, R. Yahalom, „Reasoning about Belief in Cryptographic Protocols“ in Proc. 1990 Symposium on Security and Privacy, pp. 234-248.
[3] L. Gong, Cryptographic Protocols for Distributed Systems. PhD thesis, Cambribge University, U.K., 1990.
[4] L.Gong, „Handling Infeasible Specifications of Cryptographic Protocols“, in Proc. 1991 IEEE Syposium on Security and Privacy, pp. 99-102
[5] A. Mathuria, R. Safavi-Naivi, P.Nickolas, „Some Remarks on the Logic of Gong, Need-ham and Yahalom“. in Proc. 1994 Iternational Computer Symposium (ICS´94), Dec. 1994
[6] L. Gong, “Using One-Way Functions for Authentication”, ACM Computer Communication Review, vol.19, pp. 8-11, Oct.1989
[7] D.E.Denning and G.M. Sacco, “Timestamps in Key Distribution Protocols”, Communications of the ACM, vol.24, pp. 533-536, Aug. 1981
[8] E.A. Campbell and R.Safavi-Naini, “On Automating The BAN Logic of Authentication:, in Proc. Fifteenth Australian Computer Science Conference (ACSC ´15), 1992