Burrows–Abadi–Needham logik

Burrows–Abadi–Needham-logik (även känd som BAN-logiken ) är en uppsättning regler för att definiera och analysera protokoll för informationsutbyte. Närmare bestämt hjälper BAN-logik sina användare att avgöra om utbytt information är tillförlitlig, säkrad mot avlyssning eller både och. BAN-logik börjar med antagandet att allt informationsutbyte sker på media som är sårbara för manipulering och offentlig övervakning. Detta har utvecklats till det populära säkerhetsmantrat, "Lita inte på nätverket."

En typisk BAN-logiksekvens inkluderar tre steg:

  1. Verifiering av meddelandets ursprung
  2. Verifiering av meddelandets färskhet
  3. Verifiering av ursprungets trovärdighet.

- logik använder postulat och definitioner – som alla axiomatiska system – för att analysera autentiseringsprotokoll . Användning av BAN-logiken åtföljer ofta en säkerhetsprotokollnotationsformulering av ett protokoll och ges ibland i papper.

Språktyp

BAN-logik och logik i samma familj kan avgöras : det finns en algoritm som tar BAN-hypoteser och en påstådd slutsats, och som svarar på huruvida slutsatsen kan härledas från hypoteserna eller inte. De föreslagna algoritmerna använder en variant av magiska uppsättningar .

Alternativ och kritik

BAN-logik inspirerade många andra liknande formalismer, såsom GNY-logik. Några av dessa försöker reparera en svaghet hos BAN-logiken: avsaknaden av en bra semantik med en tydlig innebörd i termer av kunskap och möjliga universum. Från och med mitten av 1990-talet analyserades dock kryptoprotokoll i operativa modeller (förutsatt perfekt kryptografi) med hjälp av modellkontroller, och många buggar hittades i protokoll som "verifierades" med BAN-logik och relaterade formalismer. [ citat behövs ] I vissa fall ansågs ett protokoll vara säkert av BAN-analysen men var i själva verket osäkert. Detta har lett till att BAN-familjens logik har övergetts till förmån för bevismetoder baserade på standardinvariansresonemang. [ citat behövs ]

Grundläggande regler

Definitionerna och deras implikationer är nedan ( P och Q är nätverksagenter, X är ett meddelande och K är en krypteringsnyckel ):

  • P tror att X : P agerar som om X är sant, och kan hävda X i andra meddelanden.
  • P har jurisdiktion över X : P : s övertygelser om X bör litas på.
  • P sa X : Vid ett tillfälle sände (och trodde) P meddelandet X , även om P kanske inte längre trodde X.
  • P ser X : P tar emot meddelande X och kan läsa och upprepa X.
  • { X } K : X är krypterad med nyckel K.
  • fresh( X ): X har inte tidigare skickats i något meddelande.
  • key( K , P ↔ Q ): P och Q kan kommunicera med delad nyckel K

Innebörden av dessa definitioner fångas i en serie postulat:

  • Om P tror nyckel( K , P ↔ Q ), och P ser { X } K , så tror P ( Q sa X )
  • Om P tror ( Q sa X ) och P tror fresh( X ), så tror P ( Q tror X ).

P måste tro att X är fräsch här. Om X inte är känt för att vara färskt, kan det vara ett föråldrat meddelande som spelas upp av en angripare.

  • Om P tror ( Q har jurisdiktion över X ) och P tror ( Q tror X ), så tror P X
  • Det finns flera andra tekniska postulat som har att göra med sammansättning av meddelanden. Till exempel, om P tror att Q sa < X , Y >, sammanlänkningen av X och Y , så tror P också att Q sa X , och P tror också att Q sa Y .

Med denna notation kan antagandena bakom ett autentiseringsprotokoll formaliseras. Med hjälp av postulaten kan man bevisa att vissa agenter tror att de kan kommunicera med hjälp av vissa nycklar. Om beviset misslyckas, tyder felpunkten vanligtvis på en attack som äventyrar protokollet.

BAN logikanalys av Wide Mouth Frog-protokollet

Ett mycket enkelt protokoll - Wide Mouth Frog-protokollet - tillåter två agenter, A och B, att upprätta säker kommunikation med hjälp av en pålitlig autentiseringsserver, S och synkroniserade klockor runt om. Med hjälp av standardnotation kan protokollet specificeras enligt följande:

Agenterna A och B är utrustade med nycklar K as respektive K bs , för att kommunicera säkert med S. Så vi har antaganden:

A tror nyckel( K som , A ↔ S )
S tror nyckel( K som , A ↔ S )
B tror nyckel( K bs , B ↔ S )
S tror nyckel( K bs , B ↔ S )

Agent A vill inleda en säker konversation med B . Den uppfinner därför en nyckel, Kab , som den kommer att använda för att kommunicera med B . A anser att denna nyckel är säker, eftersom den utgjorde själva nyckeln:

A tror nyckel ( Kab , A ↔ B )

B är villig att acceptera denna nyckel, så länge den är säker på att den kom från A :

B tror ( A har jurisdiktion över nyckel( K , A ↔ B ))

Dessutom är B villig att lita på att S korrekt vidarebefordrar nycklar från A :

B tror ( S har jurisdiktion över ( A tror nyckel( K , A ↔ B )))

Det vill säga, om B tror att S tror att A vill använda en viss nyckel för att kommunicera med B , då kommer B att lita på S och också tro det.

Målet är att ha

B tror nyckel ( Kab , A ↔ B )

A läser klockan, erhåller den aktuella tiden t , och skickar följande meddelande:

1 A → S : { t , nyckel( Kab , A ↔ B ) } K som

Det vill säga, den skickar sin valda sessionsnyckel och den aktuella tiden till S , krypterad med sin privata autentiseringsservernyckel K as .

Eftersom S tror att nyckel( K as , A ↔ S ) , och S ser { t , key( Kab , A ↔ B ) } K som , drar S slutsatsen att A faktiskt sa { t , nyckel( Kab , A ↔ B )}. (Särskilt S att meddelandet inte tillverkades av helt tyg av någon angripare.)

Eftersom klockorna är synkroniserade kan vi anta

S tror fräsch( t )

Eftersom S tror fresh( t ) och S tror A sa { t , key( K ab , A ↔ B )}, tror S att A faktiskt tror på den nyckeln( Kab , A ↔ B ). (Särskilt S att meddelandet inte spelades upp igen av någon angripare som fångade det någon gång i det förflutna.)

S skickar sedan nyckeln vidare till B :

2 S → B : { t , A , A tror nyckel( Kab , A ↔ B ) } K bs

Eftersom meddelande 2 är krypterat med Kbs , och B tror på nyckel( Kbs , B ↔ S ) , tror B nu att S sa { t , A , A believes key( Kab , A ↔ B ) } . Eftersom klockorna är synkroniserade, tror B fresh( t ), och så fresh( A believes key( Kab , A ↔ B ) ) . Eftersom B tror att S :s uttalande är färskt, tror B att S tror att ( A tror nyckel( Kab , A ↔ B ) ) . Eftersom B tror att S är auktoritativ om vad A tror, ​​tror B att ( A tror nyckel( Kab , A ↔ B ) ) . Eftersom B tror att A är auktoritativ när det gäller sessionsnycklar mellan A och B , tror B key( Kab , A ↔ B ) . B kan nu kontakta A direkt genom att använda Kab som en hemlig sessionsnyckel.

Låt oss nu anta att vi överger antagandet att klockorna är synkroniserade. I så fall S meddelande 1 från A med { t , key( Kab , A ↔ B )}, men den kan inte längre dra slutsatsen att t är färskt. Den vet att A skickade detta meddelande någon gång i det förflutna (eftersom det är krypterat med K som ) men inte att detta är ett nyligen meddelande, så S tror inte att A nödvändigtvis vill fortsätta använda nyckeln Kab . Detta pekar direkt på en attack mot protokollet: En angripare som kan fånga meddelanden kan gissa en av de gamla sessionsnycklarna Kab . (Detta kan ta lång tid.) Angriparen spelar sedan upp det gamla { t , key( Kab , A ↔ B )}-meddelandet igen och skickar det till S . Om klockorna inte är synkroniserade (kanske som en del av samma attack), S tro på detta gamla meddelande och begära att B använder den gamla, komprometterade nyckeln igen.

Det ursprungliga dokumentet Logic of Authentication (länkat nedan) innehåller detta exempel och många andra, inklusive analyser av Kerberos handskakningsprotokoll och två versioner av Andrew Project RPC-handskakning (varav en är defekt).

Vidare läsning

Hämtad från " https://en.wikipedia.org/w/index.php?title=Burrows–Abadi–Needham_logic&oldid=1101723255 "