1 Opdrachtomschrijving

Kan epistemische logica helpen bij het analyseren van de veiligheid van het SSH-Protocol? Eén van de problemen van internet is dat er derde partijen zijn waarvan je niet wilt dat zij gevoelige informatie kunnen bekijken wanneer je informatie verstuurt van jou computer naar een andere. Wanneer men gebruik maakt van het oude telnet zullen deze problemen zich voordoen. Om dit op te lossen zijn er authenticatie-protocollen ontworpen die met behulp van authenticatie en encryptie de informatie veilig stellen tegenover derde partijen. Het SSH-Protocol is hier een goed voorbeel van, dit protocol heeft het telnet systeem dan ook vervangen. Echter schuilt er altijd een addertje onder het gras, omdat de derde partijen de "veilige" informatie kunnen kraken en zo alsnog kunnen meegenieten van jouw informatie. Wij zullen gebruik maken van epistemische logica, of meer precies de BAN-Logica, om het SSH-Protocol te analyseren. Deze analyse richt zich op de werking van de authenticatie protocollen van SSH en de veiligheid hiervan. Hier zal een simulatie van worden gemaakt om het geheel visueel uit te leggen. Tevens zal er theoretische ondersteuning worden beschreven. Meer informatie over BAN-Logica is te vinden op N. Agray, W. van der Hoek and E.P. de Vink, On BAN logics for industrial security protocols, From Theory to Practice in Multi-Agent Systems, B. Dunin-Keplicz and E. Nawarecki (eds.) (dit artikel is toegespits op mobiel verkeer, maar de werking van BAN-logica wordt hierin duidelijk gemaakt).

2 Het SSH-Protocol [top]

SSH (secure shell) levert de mogelijkheid om eenvoudig toegang te krijgen tot een shell op een andere machine. SSH is tegenwoordig voornamelijk in gebruik omdat het protocol een hoge beveiliging kent. Een voordeel van SSH is dat het gebruik maakt van sterke encryptie, gebaseerd op encryptie algoritmes voor publieke sleutels (PKI), zowel voor systemen als voor gebruikers. En maakt het mogelijk om de TCP data stroom in een sessie te "tunnelen" en deze tunnel te versleutelen, en, indien gewenst, te comprimeren. Er zijn twee verschillende versies namelijk de 1.x versies (1.3 en 1.5) en de 2.0 versies. SSH versie 1 protocol is geïntegreerd, waar SSH versie 2 het vorige protocol heeft geherdefiniëerd in drie "lagen" (layers), 1) transport laag, 2) authenticatie laag en 3) de connectie laag.

De transport laag verzorgt integriteit, encryptie, compressie en de authenticatie van systemen, de authenticatie laag levert authenticatie en de connectie laag welke de tunnel beheert (shell, SSH-agent, port forwarding, flow control). Voor onze opdracht zullen we ons alleen richten op de authenticatie laag. Er zijn verschillende soorten methoden voor de authenticatie. De methoden kunnen onderverdeeld worden in public-key en uitdaging-antwoord protocollen. Bij de public-key methode is het authenticatie systeem gebaseerd op symmetrische of assymetrische encryptie. Een assymetrische encryptie wil niks anders zeggen dat de keys van elkaar verschillen, met andere woorden de client heeft een andere key dan de server. Met dit authenticatie schema reizen er geen geheimen over het Internet, en worden nooit naar de server verstuurd. Het omgekeerde geldt voor symmetrische encryptie, hierin hebben de client en de server dezelfde keys tot hun beschikking. Password is de "traditionele" wachtwoord methode en valt onder uitdaging-antwoord protocollen: als er verbinding wordt gemaakt wordt, na het vastellen van de identiteit, de gebruiker uitgenodigd het wachtwoord op te geven dat bij de desbetreffende gebruiker hoort, welke naar de server wordt verstuurd. De laatste soort methoden die wij gaan bespreken zijn de GSSAPI uitdaging-antwoord protocollen, deze zijn externe mechanisme om de authenticatie veilig te laten verlopen zoals kerberos of NTLM. Deze methoden zijn meestal geïmplementeerd door commerciele ondernemingen voor het gebruik binnen organisaties. De drie methoden (password, public-key en kerberos) voor authenticatie zullen wij gaan analyseren met behulp van de BAN-Logica.

3 Authenticatie methoden [top]

De drie authenticatie methoden, symmetrische asymmetrische en de kerberos authenticatie, zullen hier kort worden toegelicht. Om het geheel visueel uit te leggen hebben we een applet geïmplementeerd, deze kun je hier vinden.

Symmetrische Authenticatie: Alice stuurt een bericht M naar Bob, gecodeerd met de encryptiesleutel EK. Deze sleutel is van tevoren door Alice en Bob afgesproken om informatie mee te versleutelen.

Bob ontvangt het bericht M van Alice en decodeert dit bericht met de gedeelde decryptiesleutel DK.

Asymmetrische Authenticatie: Alice wil een bericht M naar Bob sturen, Alice stuurt daarom eerst een bericht naar Bob met de vraag op welke manier zij het bericht moet versleutelen.

Bob stuurt zijn encryptie sleutel naar Alice

Alice ontvangt de encryptie sleutel EK_B en gebruikt deze om het bericht M te versleutelen

Bob ontvangt het gecodeerde bericht M en gebruikt vervolgens zijn eigen decryptie sleutel DK_B om het bericht te ontcijferen.

Veiligheidsrisico’s:

Bij het authenticeren met publieke sleutels zijn er in de BAN-logica twee regels die de ’beliefs’ van de agenten bepalen:

Het voornaamste veiligheidsrisico bij het gebruik van publieke sleutels is het ’lekken’ van een van de sleutels. Dit kan bijvoorbeeld gebeuren tijdens de uitwisseling waar Alice en Bob de gemeenschappelijke sleutels afspreken. Wanneer iemand een sleutel in zijn bezit krijgt zal die in staat zijn om gebruik te maken van de ’naieviteit’ van de agenten weergeven in regels (1) en (2). Hoewel symmetrische authenticatie niet de meest veilige manier is om informatie te versturen wordt dit systeem toch veel gebruikt. Symmetrische authenticatie vereist namelijk weinig rekenkracht van zowel Alice als Bob om informatie te versleutelen en versturen.

Bij asymmetrische authenticatie wordt een deel van dit risico weggenomen; de decryptie sleutels worden niet meer uitgewisseld en zo wordt een eventueel lek voorkomen. Toch kan iemand de berichten afluisteren: Eve kan bij het uitwisselen van de encryptie sleutels deze opvangen en zich dus voor Bob als Alice voordoen en vice versa. Doordat Eve deze sleutels bezit kan ze namelijk elk bericht ontvangen, decoderen, weer met haar eigen sleutel encoderen en weer verder sturen net alsof zij Bob of Alice is. Een ander probleem met encryptie is natuurlijk dat elke encryptie gekraakt kan worden, de mogelijkheid tot afluisteren zal dus altijd blijven bestaan.

Uitdaging-Antwoord protocollen: De meest eenvoudige vorm van een uitdaging-antwoord protocol is paswoord bescherming. De uitdaging die door de server aan de client wordt opgelegd, is ‘Wat is het paswoord?’, wanneer de client dit paswoord weet zal hij deze uitdaging dus met het paswoord beantwoorden. Het Kerberos protocol is een ander uitdaging-antwoord protocol maar gebruikt verschillende servers om een gebruiker in staat te stellen een bepaalde dienst te verkrijgen. Dit zijn de authenticatie server AS, de ticket granting server TGS en de server die een dienst aanbiedt, in ons geval de printer server PS.

Authenticatie met Kerberos: Alice wil graag een document printen, hiervoor moet zij toestemming krijgen om gebruik te maken van de printer server. Maar voordat zij toestemming kan vragen moet ze eerst een digitale sleutel krijgen K_A. Deze sleutel wordt bepaald met behulp van de hash-code.

Vervolgens zal Alice haar verzoek om toegang naar de authenticatie server AS sturen. Deze server zal vervolgens antwoorden met twee berichten: een bericht geencodeerd met de gemeenschappelijke sleutel K_A, het andere bericht is met de sleutel van de ticket granting server K_TGS geencodeerd. In beide berichten wordt de SK_A→TGS meegestuurd, dit is de sessie sleutel die Alice nodig heeft om op de ticket granting server in te loggen.

Alice zal met de sleutel K_A bericht A decoderen en haar sessie sleutel voor de ticket granting server te weten komen.

Met deze sleutel zal Alice twee berichten naar de ticket granting server sturen. Een van deze berichten bevat een tijdscode T_TGS, deze tijdscode dient om de ’freshness’ van het bericht te controleren.

De ticket granting server zal met behulp van zijn eigen sleutel K_TGS bericht C decoderen en de sleutel voor de sessie met Alice te weten komen, bovendien komt de TGS nu de gegevens van Alice te weten. Daarnaast is het bericht D de zogenoemde authenticator die de identiteit van Alice nogmaals bevestigd.

Wanneer de ticket granting server Alice haar identiteit heeft bevestigd zullen er twee berichten naar haar gestuurd worden:

Uit bericht F kan Alice haar sessie sleutel voor de printer server PS, SK_A→PS berekenen.

Nu heeft Alice voldoende informatie om in te kunnen loggen op de printerserver. Daarnaast stuurt ze nog een challenge mee aan de printerserver, de tijdscode TA als het protocol goed is verlopen krijgt Alice het bericht T_{A + 1} terug en kan de gevraagde dienst verleend worden.

De printer server zal beide berichten decoderen en vervolgens antwoord geven op de door Alice geplaatste uitdaging.

Veiligheidsrisico’s:

De uitwisseling van informatie door de verschillende servers wordt in het kerberos protocol beschermd doordat elke server zijn eigen sleutel heeft met het protocol, deze sleutels zijn vooraf bekend. Alice krijgt alleen de sessie sleutels van de verschillende servers door, hierdoor blijft de gevoelig informatie verborgen voor Alice. Het grootste veiligheidsrisico voor dit protocol ligt daarom niet bij deze sleutel maar in de periode waarvoor de tickets, die Alice krijgt uitgereikt, gelden en de tijdscodes die in de authenticators worden doorgestuurd. Een te lange ticketperiode geeft eventueele aanvallers de kans om gebruik te maken van een ticket terwijl de daadwerkelijke sessie allang is afgelopen. De gevoelgheid voor de tijdscodes komt in de analyse met BAN-logica naar voren uit de regel:

Wanneer een aanvaller nu een oude sleutel heeft bemachtigd en daarnaast de server kan doen geloven dat fresh(M), dan kan de aanvaller gebruik maken van deze oude sleutel. Dit kan bijvoorbeeld door het niet synchroon lopen van de verschillende systeemtijden.