Burroughs-Abadie-Needham Logik

Burrows -Abadi-Needham-logik eller BAN - logik er en formel logisk model for videns- og tillidsanalyse , der er meget brugt i analysen af godkendelsesprotokoller .

Hovedideen med BAN-logik er, at når man analyserer sådanne protokoller, først og fremmest skal man være opmærksom på, hvordan de involverede parter i autentificeringsprocessen opfatter information - hvad de tager for givet, og hvad de ved med sikkerhed eller kan være udledt af logiske gennem fakta, der er pålidelige for dem. [en]

Typisk er autentificeringsprotokoller beskrevet ved sekventiel opregning af meddelelser transmitteret mellem protokoldeltagere. Hvert trin beskriver indholdet af beskeden og specificerer afsender og modtager. BAN-logikken behandler ægtheden af en meddelelse som en funktion af dens integritet og nyhed ved at bruge logiske regler til at holde styr på tilstanden af disse attributter gennem hele protokollen. [2]

Der er tre typer objekter i BAN-logikken: medlemmer, krypteringsnøgler og formler, der forbinder dem. I den formelle analyse af protokollen konverteres hver besked til en logisk formel; så er de logiske formler forbundet med udsagn . Således ligner BAN-logik på mange måder Hoares logik . [3] Den eneste logiske operation, der bruges i denne logik, er konjunktion. Forskellige prædikater introduceres også , for eksempel etablering af relationer mellem deltagere og udsagn (tillidsforhold, jurisdiktion osv.) eller udtrykker nogle egenskaber ved udsagn (såsom friskhed , det vil sige udsagnet om, at udsagnet blev modtaget for nylig).

Som enhver formel logik er BAN-logik udstyret med aksiomer og slutningsregler. Formel protokolanalyse består i at bevise et bestemt sæt udsagn, udtrykt ved BAN-logiske formler, ved hjælp af slutningsregler. For eksempel er minimumskravet for enhver autentificeringsprotokol, at begge parter skal stole på, at de har fundet en hemmelig nøgle for at kunne udveksle oplysninger med hinanden.

Grundprædikater og deres betegnelser

$P|\equiv X$ betyder, at han tror på udtalelsen . Det betyder, at det vil virke, som om det er sand information. $P$ $x$ $P$ $x$
$P\vartriangleleft X$ indebærer, at han ser , det vil sige, at han modtog en besked, der indeholder . Det vil sige, at den kan læse og gengive (måske efter dekrypteringsproceduren) beskeden . $P$ $x$ $P$ $x$ $P$ $x$
$P|\sim X$ betyder, at han engang udtrykte , det vil sige, at han på et tidspunkt sendte en besked indeholdende . $P$ $x$ $P$ $x$
$P|\Rightarrow X$ betyder, at den har jurisdiktion over (eller har jurisdiktion over ), det vil sige, at den har myndighed i et spørgsmål vedr . $x$ $P$ $P$ $x$ $P$ $x$
$\#X$ betyder, at erklæringen er modtaget for nylig. Det vil sige, at beskeden ikke blev sendt engang i fortiden (før protokollen blev startet). $x$ $x$
$P{\stackrel {k}{\longleftrightarrow }}Q$ betyder, at og bruge en delt nøgle til kommunikation . $P$ $Q$ $k$
$\lbrace X\rbrace _{k}$ betyder, at dataene er krypteret med en nøgle . $x$ $k$

Andre betegnelser

Konjunktionsoperationen er angivet med et komma, og den logiske konsekvens er angivet med en vandret streg. Således skrives den logiske regel i notationen af BAN-logik som $A\wedge B\Rightarrow C$ ${\dfrac {A,B}{C))$

Aksiomer for BAN-logik

Tiden er opdelt i to epoker: fortid og nutid . Nutiden begynder fra det øjeblik, protokollen lanceres.
Den deltager , der taler , tror på sandheden . $P$ $x$ $x$
Kryptering betragtes som absolut sikker: en krypteret besked kan ikke dekrypteres af en deltager, der ikke kender nøglen.

Outputregler

Meddelelsesbetydningsregel :

{\dfrac {A|\equiv A{\stackrel {K}{\longleftrightarrow }}B,A\vartriangleleft \lbrace X\rbrace _{K}}{A|\equiv B|\sim X}}

Tilsvarende verbal formulering: Ud fra antagelserne om, at han tror på at dele nøglen med , og ser beskeden krypteret med nøglen , følger det, at han mener, at han på et tidspunkt sagde . $EN$ $K$ $B$ $EN$ $x$ $K$ $EN$ $B$ $x$

Bemærk, at det her implicit antages, at han aldrig selv har udtrykt . $EN$ $x$

Regel for kontrol af unikheden af numeriske indsættelser :

{\dfrac {A|\equiv \#X,A|\equiv B|\sim X}{A|\equiv B|\equiv X))

det vil sige, at hvis han tror på nyhed og på det , han engang udtrykte , så tror han på, at han stadig stoler på . $EN$ $x$ $B$ $x$ $EN$ $B$ $x$

Jurisdiktionsregel :

{\dfrac {A|\equiv B|\Rightarrow X,A|\equiv B|\equiv X}{A|\equiv X))

siger, at hvis han tror på kræfter om , og tror på det, han tror på , så skal han tro på . $EN$ $B$ $x$ $EN$ $B$ $x$ $EN$ $x$

Andre regler

Tillidsoperatøren og konjunktionen adlyder følgende relationer:

{\dfrac {A|\equiv X,A|\equiv Y}{A|\equiv (X,Y)))

{\dfrac {A|\equiv (X,Y)}{A|\equiv X))

{\dfrac {A|\equiv B|\equiv (X,Y)}{A|\equiv B|\equiv X))

Faktisk fastsætter disse regler følgende krav: stol på et sæt udsagn, hvis og kun hvis det stoler på hver udsagn separat. $EN$ $EN$

En lignende regel findes for operatøren : $|\sim$

{\dfrac {A|\equiv B|\sim (X,Y)}{A|\equiv B|\sim X))

Endelig, hvis en del af erklæringen er modtaget for nylig, så kan det samme siges om hele erklæringen:

{\dfrac {A|\equiv \#X}{A|\equiv \#(X,Y)))

En formel tilgang til analyse af autentificeringsprotokoller

Fra et praktisk synspunkt udføres protokolanalyse som følger: [4] [5]

Den originale protokol konverteres til en idealiseret protokol (det vil sige skrevet i form af BAN-logik).
Antagelser om den oprindelige tilstand af protokollen er tilføjet.
Hver sætning er forbundet med en logisk formel, det vil sige en logisk erklæring om protokollens tilstand efter hver sætning.
Inferensregler og aksiomer anvendes på protokollens antagelser og påstande for at bestemme parternes tillidstilstand ved afslutningen af protokollen.

Lad os forklare betydningen af denne procedure. Det første trin kaldes idealisering og består af følgende: hvert trin i protokollen, skrevet som , omdannes til et sæt logiske udsagn vedrørende de transmitterende og modtagende parter. Lad for eksempel et af protokoltrinene se sådan ud: $P\longrightarrow Q:besked$

A\longrightarrow B:\lbrace A,K_{ab}\rrace _{K_{bs}}

Denne meddelelse fortæller parten (som har nøglen ), at nøglen skal bruges til at kommunikere med . Den tilsvarende logiske formel for denne meddelelse er: $B$ ${\displaystyle K_{bs))$ ${\displaystyle K_{ab))$ $EN$

A\longrightarrow B:\lbrace A{\stackrel {K_{ab}}{\longleftrightarrow }}B\rbrace _{K_{bs}}

Når den givne besked er leveret , er udsagnet sandt: $B$

B\vartriangleleft \lbrace A{\stackrel {K_{ab}}{\longleftrightarrow }}B\rbrace _{K_{bs}}

det vil sige, at han ser dette budskab og vil fortsætte med at handle i overensstemmelse med det. $B$

Efter idealisering ser protokollen ud som en sekvens af udsagn og udsagn, der forbinder disse udsagn. Den indledende erklæring består af protokollens indledende antagelser, den endelige erklæring er resultatet af protokollen:

[assumptions]S_{1}[assertion1]\cdots [assertion(n-1)]S_{n}[konklusioner]

En protokol anses for at være korrekt, hvis sættet af endelige erklæringer omfatter sættet af (formaliserede) protokolmål.

Formål med godkendelsesprotokoller

Lad os skrive målene for godkendelsesprotokollen i form af BAN-logik (det vil sige, hvilke logiske påstande der skal udledes af protokollens antagelser, givet rækkefølgen af trin (påstande) udført i denne protokol): [6] [7]

A|\equiv A{\stackrel {K}{\longleftrightarrow }}B

B|\equiv A{\stackrel {K}{\longleftrightarrow }}B

det vil sige, at begge parter skal stole på, at de bruger den samme hemmelige nøgle til at udveksle beskeder. Du kan dog bede om mere, for eksempel:

A|\equiv B|\equiv A{\stackrel {K}{\longleftrightarrow }}B

B|\equiv A|\equiv A{\stackrel {K}{\longleftrightarrow }}B

det vil sige kvittering for modtagelse af nøglen . [6]

Analyse af den bredmundede frø-protokol ved hjælp af BAN-logik

Overvej en simpel godkendelsesprotokol , broadmouth frog-protokollen , som tillader to parter, og , at etablere en sikker forbindelse ved hjælp af en server, de både har tillid til og synkroniserede ure. [8] I standardnotation er protokollen skrevet som følger: $EN$ $B$ $S$

A\rightarrow S:A,\{T_{A},K_{ab},B\}_{K_{as))

S\rightarrow B:\{T_{S},K_{ab},A\}_{K_{bs}}

Efter idealisering tager protokoltrinnene formen:

A\rightarrow S:\{T_{A},A{\stackrel {K_{ab}}{\longleftrightarrow }}B\}_{K_{as}}

S\rightarrow B:\{T_{S},A|\equiv A{\stackrel {K_{ab}}{\longleftrightarrow }}B\}_{K_{bs}}

Lad os nedskrive de indledende antagelser af protokollen. Parterne og har henholdsvis nøgler og , til sikker kommunikation med serveren , som på BAN-logikkens sprog kan udtrykkes som: $EN$ $B$ ${\displaystyle K_{as))$ ${\displaystyle K_{bs))$ $S$

A|\equiv A{\stackrel {K_{as}}{\longleftrightarrow }}S

S|\equiv A{\stackrel {K_{as}}{\longleftrightarrow }}S

B|\equiv B{\stackrel {K_{bs}}{\longleftrightarrow }}S

S|\equiv B{\stackrel {K_{bs}}{\longleftrightarrow }}S

Der er også antagelser om midlertidige indsættelser:

S|\equiv \#T_{A}

B|\equiv \#T_{S}

Ud over det er der et par antagelser om krypteringsnøglen:

$B$ er afhængig af at vælge en god nøgle: $EN$

B|\equiv A|\Rightarrow (A{\stackrel {K_{ab)){\longleftrightarrow }}B)

$B$ stoler på at give nøglen fra : $S$ $EN$

B|\equiv S|\Rightarrow (A|\equiv A{\stackrel {K_{ab)){\longleftrightarrow }}B)

$EN$ stoler på, at sessionsnøglen er accepteret:

A|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)

Lad os gå videre til analysen af protokollen.

$S$ modtager den første besked, hvorfra følgende konklusioner kan drages:

$S$ , når du ser en besked krypteret med nøglen , konkluderer den, at den blev sendt (reglen om betydningen af beskeden). ${\displaystyle K_{as))$ $EN$
Tilstedeværelsen af en frisk midlertidig indsættelse giver os mulighed for at konkludere, at hele meddelelsen blev skrevet for nylig (reglen for operatøren ). $T_{A}$ $\#$
Fra friskheden af hele beskeden kan han konkludere, at han troede på det, han sendte (reglen for at kontrollere det unikke ved numeriske indsættelser). $S$ $EN$

Derfor ,. $S|\equiv A|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$

$B$ modtager den anden protokolmeddelelse, som resulterer i:

Når klienten ser en besked krypteret med nøglen , forstår klienten , at den er blevet sendt . ${\displaystyle K_{bs))$ $B$ $S$
Den midlertidige indsættelse beviser , at hele beskeden blev sendt for nylig. $T_{S}$ $B$
I lyset af beskedens friskhed konkluderer han, at han stoler på alt, der sendes. $B$ $S$
Især mener han, at han stoler på den anden del af budskabet. $B$ $S$
Men han mener også, at det er i jurisdiktionen at finde ud af, om hans partner kender den hemmelige nøgle, og overlader derfor myndigheden til at generere nøglen. $B$ $S$ $EN$ $B$ $EN$

Ud fra disse overvejelser kan følgende konklusioner drages:

B|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)

B|\equiv A|\equiv (A{\stackrel {K_{ab)){\longleftrightarrow }}B)

Under hensyntagen til den oprindelige antagelse om, at , opnår vi, at den analyserede protokol er berettiget. Det eneste der ikke kan siges er: $A|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$

A|\equiv B|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)

det vil sige, at han ikke opnåede bekræftelse på, at han modtog den ønskede nøgle. $EN$ $B$

Kritik

Idealiseringsprocessen er mest kritiseret, da den idealiserede protokol muligvis ikke korrekt afspejler dens reelle modstykke. [9] Dette skyldes, at beskrivelsen af protokollerne ikke er givet på en formel måde, hvilket nogle gange sår tvivl om selve muligheden for korrekt idealisering. [10] Desuden forsøger en række kritikere at vise, at BAN-logikken også kan få åbenlyst forkerte karakteristika af protokollerne. [10] Desuden kan resultatet af protokolanalyse ved brug af BAN-logik ikke betragtes som et bevis på dets sikkerhed, da denne formelle logik udelukkende beskæftiger sig med tillidsspørgsmål. [elleve]

Noter

↑ N. Smart, Kryptografi, s. 175.
↑ B. Schneier, "Applied Cryptography", s. 66.
↑ M. Burrows, M. Abadi, R. Needham, "A Logic of Authentication", s. 3.
↑ M. Burrows, M. Abadi, R. Needham, "A Logic of Authentication", s. elleve.
↑ B. Schneier, "Applied Cryptography", s. 67.
↑ 1 2 N. Smart, "Kryptografi", s. 177.
↑ M. Burrows, M. Abadi, R. Needham, "A Logic of Authentication", s. 13.
↑ N. Smart, Kryptografi, s. 169-170.
↑ DM Nessett, "A Critique of the Burrows, Abadi, and Needham Logic", s. 35-38.
↑ 1 2 Boyd, C. og Mao, W. "On a Limitation of BAN Logic"
↑ PF Syverson, "Brugen af logik i analysen af kryptografiske protokoller"

Litteratur

M. Burrows, M. Abadi, R. Needham. A Logic of Authentication (neopr.) // Systems Research Center of Digital Equipment Corporation i Palo Alto. - 1989. - December ( bind 426 ). - S. 44-54 .

Monniaux, D. Beslutningsprocedurer for analyse af kryptografiske protokoller ved troslogikker // Computer Security Foundations Workshop, 1999. Proceedings of the 12th IEEE: journal. - 1999. - S. 44-54 .

Boyd, Colin; Mao, Wenbo. On a Limitation of BAN Logic // Fremskridt inden for kryptologi - EUROCRYPT '93 (neopr.) / Helleseth, Tor. - Springer Berlin / Heidelberg, 1994. - S. 240-247. - ISBN 978-3-540-57600-6 .

N. Smart. Kryptografi . - Moskva: Technosfera, 2005. - S. 162 -179. — 528 s. - ISBN 5-94836-043-1 .

B. Schneier. Anvendt kryptografi (neopr.) . - John Wiley & Sons , 1995. - S. 66-69. — 662 s. - ISBN 0-47111-709-9 . Arkiveret 3. september 2012 på Wayback Machine

A. Alferov, A. Kuzmin, A. Zubov, A. Cheremushkin. Fundamentals of Cryptography . - Moskva: Helios ARV, 2002. - S. 378-385 , 404-406. - 480 s. — ISBN 5-85438-025-0 .