Abstrakt. Säkerhetsspecifikationer för webbtjänster uttrycks vanligtvis som en blandning av XML-scheman, exempelmeddelanden och berättande förklaringar. Vi föreslår ett nytt specifikationsspråk för att skriva kompletterande maskinkontrollerbara beskrivningar av SOAP-baserade säkerhetsprotokoll och deras egenskaper. Vårt TulaFale-språk är baserat på pi-kalkylen (för att skriva samlingar av SOAP-processorer som körs parallellt), plus XML-syntax (för att uttrycka SOAP-meddelanden), logiska predikat (för att konstruera och filtrera SOAP-meddelanden) och korrespondenspåståenden (för att ange autentiseringsmål för protokoll). Vår implementering sammanställer TulaFale till den tillämpade pi-kalkylen, och kör sedan Blanchet's upplösningsbaserade protokollkontrollant. Därför kan vi automatiskt verifiera autentisering egenskaper hos SOAP-protokoll. Webbtjänster är en omfattande distribuerad systemteknik, baserad på asynkront utbyte av XML-meddelanden som överensstämmer med SOAP-meddelandeformatet [BEK + 00,W3C03]. WS-Security-standarden [NKHBM04] beskriver hur man signerar och krypterar delar av SOAP-meddelanden, för att uppnå end-to-end-säkerhet. Detta dokument introducerar TulaFale, ett nytt språk för att definiera och automatiskt verifiera modeller av SOAP-baserade kryptografiska protokoll, och illustrerar dess användning för en typisk begäran / svar protokoll: vi skissar protokollet, beskriver potentiella attacker, och sedan ge en detaljerad beskrivning av hur man definierar och kontrollerar begäran och svar meddelanden i TulaFale. En grundläggande motivation för webbtjänster är att stödja programmatisk tillgång till webbdata. HTML returneras av en typisk webbplats är en blandning av data och presentationsmarkup, väl lämpad för mänsklig surfning, men förekomsten av markup gör HTML en rörig och skör format för databehandling. Däremot är XML som returneras av en webbtjänst bara data, med vissa tydligt särskiljande metadata, väl lämpad för programmatisk åtkomst. Till exempel, sökmotorer exportera webbtjänster för programmatisk webbsökning, och e-handel webbplatser exportera webbtjänster för att tillåta anslutna webbplatser direkt tillgång till sina databaser. I allmänhet växer ett brett spektrum av tillämpningar för webbtjänster fram, från en väletablerad användning av SOAP som plattform och leverantörsneutralt mellanprogram inom en enda organisation, till den föreslagna användningen av SOAP för interaktion mellan enheter [S + 04]. I början, "SOAP" stod för "Enkel Object Access Protocol", och var avsedd att genomföra "RPC med XML över HTTP" [Win98, Win99, Box01]. HTTP underlättar driftskompatibiliteten mellan geografiskt avlägsna maskiner och mellan dem inom skyddsområden åtskilda av företagets brandväggar som blockerar många andra transporter. XML underlättar interoperabilitet mellan olika leverantörers implementationer, till skillnad från olika binära format av tidigare RPC-teknik. Ändå bör webbtjänstteknik inte misstolkas som HTTP-specifik RPC för distribuerade objekt [Vog03]. HTTP är för närvarande det vanligaste transportprotokollet, men SOAP-formatet är oberoende av HTTP, och vissa webbtjänster använder andra transporter såsom TCP eller SMTP [SMWC03]. Designmålen för SOAP/1.1 [BEK + 00] utesluter uttryckligen objektorienterade funktioner såsom objektaktivering och distribuerad sophämtning; enligt version 1.2 [W3C03] är "SOAP" ett rent namn, inte en akronym. Det primitiva meddelandemönstret i SOAP är ett enda enkelriktat meddelande som kan behandlas av noll eller fler mellanhänder mellan två slutpunkter; RPC är ett härlett meddelandemönster byggt från en begäran och ett svar. I korthet är SOAP inte bunden till objekt, och webbtjänster är inte bundna till webben. Ändå är vårt körexempel en RPC över HTTP, vilket fortfarande verkar vara det vanliga fallet. Webbtjänster specifikationer stöder SOAP-nivå säkerhet via en syntax för att inbädda kryptografiska material i SOAP-meddelanden. För att uppfylla sina säkerhetsmål kan webbtjänster och deras kunder konstruera och kontrollera säkerhetsrubriker i meddelanden, enligt WS-säkerhetsformatet [IM02, NKHBM04]. WS-Security kan ge meddelandesekretess och autentisering oberoende av den underliggande transporten, t.ex. med hjälp av säkra hashfunktioner, kryptering med delad nyckel eller kryptering med öppen nyckel. WS-Security har flera fördelar jämfört med att använda en säker transport som SSL, inklusive skalbarhet, flexibilitet, transparens för mellanhänder som brandväggar och stöd för icke-avvisning. Väsentligt nog föreskriver dock inte själva WS-Security ett särskilt säkerhetsprotokoll: varje tillämpning måste fastställa sina säkerhetsmål och behandla säkerhetsrubriker i enlighet därmed. Webbtjänster kan vara sårbara för många av de väldokumenterade klasserna av angrepp på vanliga webbplatser [SS02,HL03]. Dessutom, till skillnad från typiska webbplatser, webbtjänster som förlitar sig på SOAP-baserade kryptografiska protokoll kan dessutom vara sårbara för en ny klass av XML omskrivning attacker: en rad attacker där en angripare kan spela in, ändra, spela om och omdirigera SOAP-meddelanden, men utan att bryta de underliggande kryptografiska algoritmer. Flexibilitet kommer till ett pris när det gäller säkerhet, och det är förvånansvärt lätt att misstolka de garantier som faktiskt erhålls från bearbetning av säkerhetsrubriker. XML är därför en ny inställning för ett gammalt problem går tillbaka till Needham och Schroeder banbrytande arbete om autentisering protokoll; SOAP säkerhetsprotokoll bör bedömas säkert, eller inte, med avseende på en angripare som kan "interpose en dator på 2 alla kommunikationsvägar, och därmed kan ändra eller kopiera delar av meddelanden, spela upp meddelanden, eller avge falskt material" [NS78]. XML-omskrivningsattacker ingår i WS-I-hotmodellen [DHK + 04]. Vi har hittat en mängd olika repris- och imiteringsattacker i praktiken. Användningen av formella metoder för att analysera kryptografiska protokoll och deras sårbarheter börjar med arbete av Dolev och Yao [DY83]. Under de senaste åren har det bedrivits intensiv forskning om modellen Dolev-Yao, vilket lett till att många formalismer och verktyg har utvecklats. TulaFale bygger på forskningslinjen med hjälp av pi-kalkylen. Pi-kalkylen [Mil99] är en allmän teori om interaktion mellan samtidiga processer. Flera varianter av pi-kalkylen, inklusive spi [AG99], och en generalisering, tillämpad pi [AF01], har använts för att formalisera och bevisa egenskaper kryptografiska protokoll. En rad komposition resonemang tekniker finns tillgängliga för att bevisa protokoll egenskaper, men bevis kräver vanligtvis mänsklig skicklighet och beslutsamhet. På senare tid har emellertid Blanchet [Bla01, Bla02] föreslagit en rad automatiska tekniker, som ingår i hans teoremprovare ProVerif, för att kontrollera vissa sekretess- och autentiseringsegenskaper hos den tillämpade pi-kalkylen. ProVerif arbetar genom att sammanställa pi kalkyl till Horn klausuler och sedan kör upplösningsbaserade algoritmer. TulaFale är ett nytt skriptspråk för att ange SOAP säkerhetsprotokoll, och verifiera frånvaron av XML omskrivning attacker: TulaFale = processer + XML + predicates + påståenden pi calculus är kärnan i TulaFale, och tillåter oss att beskriva SOAP processorer, såsom klienter och servrar, som kommunikationsprocesser. Vi utökar pi-kalkylen med en syntax för XML plus symboliska kryptografiska operationer; därför kan vi direkt uttrycka SOAP-meddelanden med WS-säkerhetshuvuden. Vi anger deklarativt konstruktion och kontroll av SOAP-meddelanden med Prolog-stil predikat; därför kan vi beskriva de operativa detaljerna i SOAP bearbetning. Självständigt anger vi säkerhetsmål med hjälp av olika påståenden, såsom korrespondens för meddelandeautentisering och korrelation. Det är viktigt att TulaFale kan uttrycka den detaljerade strukturen av XML-signaturer och kryptering för att fånga låga nivåer attacker på denna struktur, såsom kopiera en del av en XML-signaturer till en annan; mer abstrakta representationer av meddelandeformat, typiskt i studien av Dolev-Yao-modellen och används till exempel i tidigare arbete med SOAP-autentisering protokoll [GP03], är okänsliga för sådana attacker. Vår metodik vid utveckling av TulaFale har varit att studera specifika webbtjänster implementationer, och att utveckla TulaFale skript modellera sina, en särskild implementering av WS-Säkerhet och relaterade specifikationer. Vi har implementerat det löpande exempelprotokollet i detta dokument med hjälp av WSE, och kontrollerat att de SOAP-meddelanden som anges i vårt skript troget återspeglar de SOAP-meddelanden som observerats i detta genomförande. För en diskussion om genomförandet av relaterade protokoll, inklusive loggar av SOAP meddelanden, se den tekniska rapporten version av en tidigare dokument [BFG04a]. Bilda. 1 illustrerar vår metodik. Till vänster har vi den användarbaserade koden för att implementera ett protokoll för webbtjänster, t.ex. det här dokumentet, ovanpå WSE-biblioteket. Till höger har vi TulaFale-skriptet som modellerar den användarbaserade koden, tillsammans med en del bibliotek bygger på modelleringsåtgärder som utförs av WSE. Även till höger har vi TulaFale-verktyget, som sammanställer sina inmatningsskript i den rena tillämpade pi-kalkylen som ska analyseras via ProVerif. TulaFale är ett direkt genomförande av pi kalkyl beskrivs i en tidigare formell semantik av webbtjänster autentisering [BFG04a]. Det ursprungliga bidraget från detta dokument är att presentera en konkret språkdesign, att rapportera ett genomförande av automatisk verifiering av påståenden i TulaFale skript med Blanchet ProVerif, och att utveckla ett betydande exempel. Avsnitt 2 introducerar informellt en enkel begäran/svar protokoll och dess säkerhetsmål: autentisering och korrelation av de två meddelandena. Avsnitt 3 presenterar TulaFale syntax för XML med symbolisk kryptografi och för predikat, och som en källa till exempel, förklarar ett bibliotek av TulaFale predicates för att bygga och kontrollera SOAP-meddelanden. Avsnitt 4 beskriver predikat som är specifika för meddelandena i vår begäran/svar protokoll. I avsnitt 5 introduceras processer och säkerhetspåståenden i TulaFale och beskrivs deras genomförande via ProVerif. Avsnitt 6 beskriver processer och predikat specifika för vårt protokoll, och visar hur man verifierar sina säkerhetsmål. Slutligen avslutas avsnitt 7. Vi anser att en enkel SOAP-baserad begäran / svar protokoll, av det slag som lätt implementeras med hjälp av WSE för att göra en RPC till en webbtjänst. Våra säkerhetsmål är helt enkelt meddelandeautentisering och korrelation. För att uppnå dessa mål, innehåller begäran ett användarnamn token identifiera en viss användare och en signatur token signerad av en nyckel härledd från användarens lösenord; omvänt, svaret innehåller en signatur token signerad av serverns öppna nyckel. Dessutom, för att bevara sekretessen för användarens lösenord från ordlista attacker, användarnamnet token i begäran meddelandet krypteras med serverns öppna nyckel. (För enkelhetens skull är vi inte intresserade av några sekretessegenskaper, såsom sekretess för de faktiska meddelandeorganen, och vi modellerar inte någon behörighetspolicy.) I resten av detta avsnitt presenterar vi en detaljerad men informell specifikation av vårt avsedda protokoll, och överväga vissa variationer som är föremål för XML omskrivning attacker. Vårt protokoll omfattar följande huvudmän: -En enda certifieringsmyndighet (CA) utfärda X.509 offentliga nyckelcertifikat för tjänster, undertecknat med CA: s privata nyckel. -Två servrar, var och en utrustad med en offentlig nyckel som certifierats av CA och exporterar ett godtyckligt antal webbtjänster. -Multiple kunder, agerar på uppdrag av mänskliga användare. Förtroende mellan huvudansvariga modelleras som en databas som associerar lösenord till auktoriserade användarnamn, tillgängliga från kunder och servrar. Vår hotmodell har en aktiv angripare i kontroll av nätverket, i besittning av alla offentliga nycklar och användarnamn, men inte i besittning av något av följande: (1) Den privata nyckeln till CA. (2) Den privata nyckeln till en offentlig nyckel som godkänts av CA. (3) Lösenordet för alla användare i databasen. Den andra och tredje punkten utesluter i huvudsak "insiderattacker", vi antar att klienterna, servrarna och CA tillhör en enda sluten institution. Det är lätt att utvidga vår modell för att studera effekterna av insiderattacker, och faktiskt för att tillåta mer än två servrar, men vi utelämnar detaljerna i detta expositionsexempel. Bilda. 2 visar en avsedd körning av protokollet mellan en klient och servern. -Den huvudsakliga klienten (kr,U) agerar på uppdrag av en användare som identifierats av U (en XML-kodning av användarnamn och lösenord). Parametern kr är den öppna nyckeln till CA, som kunden behöver för att kontrollera giltigheten av allmänna nyckelcertifikat. -Den huvudsakliga servern (sx,cert,S) implementerar en tjänst som identifieras av S (en XML-kodning av en webbadress, en SOAP-åtgärd, och ämnesnamnet som visas på tjänstens certifikat). Parametern sx är serverns privata signeringsnyckel, medan cert är dess offentliga certifikat. -Kunden skickar en begäran meddelande som uppfyller ärMsg1(−,U,S,id1,t1,b1), som vi definierar senare att betyda att meddelandet har kropp b1, timestamp t1, och meddelande identifierare id1, är adresserad till en webbtjänst S, och har en <Security> rubrik som innehåller en token som identifierar U och krypteras med S: s öppna nyckel, och en signatur av S, id1, t1 och b1 av U. - Servern skickar ett svar meddelande som uppfyller ärMsg2(−,S,id1,id2,t2,b2), som vi definierar senare för att betyda att meddelandet har kropp b2, timestamp t2, och meddelandeidentifieraren id2, skickas från S, och har en <Security> rubrik som innehåller S certifikat cert och en signatur av id1, id2, t2 och b2 av S. -Kunden och servern antar start-och slut-händelser märkta C1(U,S,id1,t1,b1) för att registrera de data som överenskommits efter mottagandet av det första meddelandet. På samma sätt registrerar start- och sluthändelserna märkta C2(U,S,id1,t1,b1,id2,t2,b2) de data som överenskommits efter att båda meddelandena mottagits. Varje start-händelse markerar en avsikt att skicka data. Varje sluten händelse markerar tydligen framgångsrik överenskommelse om data. Start-och slut-event definierar våra autentiserings- och korrelationsmål: för varje slut-event med en viss etikett, det finns en föregående start-event med samma etikett i alla körningar av systemet, även i närvaro av en aktiv angripare. Sådana mål kallas engångskorrespondenser [WL93] eller icke-injektivavtal [Low97]. C1-händelserna anger autentisering av begäran, medan C2-händelserna anger autentisering av svaret. Genom att inkludera uppgifter från begäran anger C2-händelser också korrelationen mellan begäran och svar. Som de flesta meddelanden, bild. 2 illustrerar helt enkelt en typisk protokoll körs, och är i sig inte en lämplig specifikation. I avsnitten 4 och 6 presenterar vi en formell specifikation i TulaFale: vi definierar huvudpersonerna Client(kr,U) och Server(sx,cert,S) som parametriska processer, och vi definierar kontrollerna isMsg1 och isMsg2 som predikerar på vår XML-modell med symbolisk kryptografi. Den formella modellen förtydligar följande punkter, som lämnas implicita i figuren: -Kunden kan godtyckligt välja vilken tjänst S att ringa, och vilka data t1 och b1 att skicka. (I den formella modellen gör vi vanligtvis sådana godtyckliga val genom att mata in data från motståndaren.) Omvänt måste kunden generera en ny identifierare ID1 för varje begäran, annars är det omöjligt att korrelera svaren från två samtidiga förfrågningar till samma tjänst. -Liksom servern kan godtyckligt välja svarsdata id2, t2 och b2. Å andra sidan tar vår formella modell inte direkt upp reprisskydd. För att utesluta direkt replays av korrekt undertecknade meddelanden, skulle vi behöva specificera att för varje slut-event finns det en unik föregående start-event med samma etikett. Detta kallas en brevväxling eller ett injiceringsavtal. I praktiken kan vi skydda oss mot direktåterspel med hjälp av en cache av nyligen mottagna meddelandeidentifierare och tidsstämplar för att säkerställa att inga två meddelanden accepteras med samma identifierare och tidsstämpel. Därför, om vi kan bevisa att protokollet upprättar icke-injektiv överenskommelse om data, inklusive identifierare och tidsstämplar, då, med tanke på sådan replay skydd, protokollet genomförandet också fastställer injiceringsavtal. Vi avslutar detta avsnitt genom att diskutera några bristfälliga variationer av protokollet, motsvarande faktiska brister vi har stött på i användarkoden för webbtjänster. -Förutsätt att checken ärMsg1(−,U,S,id1,t1,b1) krävs bara att S, id1 och b1 är undertecknade av U, men inte tidsstämpeln t1. Återspelskydd baserat på tidsstämpeln är nu ineffektivt: motståndaren kan spela in ett meddelande med tidsstämpel t1, vänta tills en viss tid t2 när tidsstämpeln har gått ut, och meddelandeidentifieraren id1 inte längre är cachad, skriva om det ursprungliga meddelandet med tidsstämpel t2, och sedan spela upp meddelandet igen. Det resulterande meddelandet uppfyller isMsg1(−,U,S,id1,t2,b1), eftersom t2 inte behöver signeras och därmed accepteras av servern. Bilda. 3 visar attacken, och det resulterande misslyckandet av korrespondens C1. -Suppstå att en klient återanvänder samma meddelandeidentifierare i två olika samtal till en webbtjänst; motståndaren kan manipulera meddelanden så att kunden behandlar svaret på det första samtalet som om det vore svaret på det andra samtalet. Bilda. 4 visar attacken. Kunden skickar en första begäran med organ b1 och ID1. Motståndaren avlyssnar svaret med kropp b2, och skickar ett SOAP-fel tillbaka till klienten. Därefter skickar kunden en andra begäran med samma identifieringskod1 som den första, och kropp b1". Motståndaren kan ta bort denna begäran för att förhindra att den når tjänsten, och sedan spela upp det ursprungliga svaret. Kunden anser nu att b2 är svaret på b1', när det i själva verket är svaret på b1, kanske helt annorlunda. Formellt är detta ett misslyckande med korrespondensen C2. -Uppstå som att servern inte inkluderar begäran id1 i signaturen på svarsmeddelandet. Då kan motståndaren montera en liknande korrelation attack, bryta C2-vi utelämna detaljer. Vi kan enkelt anpassa vårt TulaFale-skript för att modellera dessa variationer i protokollet. Vårt verktyg upptäcker automatiskt och snabbt felen och returnerar beskrivningar av de meddelanden som skickas under attackerna. Dessa brister i webbtjänster kod är typiska för fel i kryptografiska protokoll historiskt. Den praktiska effekten av dessa brister är svår att bedöma, som de konstaterades i den preliminära koden, före införandet. Ändå är det klokt att eliminera dessa sårbarheter, och verktyg som TulaFale kan systematiskt utesluta dem. I detta avsnitt introduceras termen och det grundläggande språket i TulaFale, via en serie grundläggande konstruktioner som behövs för t.ex. protokollet i avsnitt 2. Hela 8 papperet, för utställningens skull, vi bort vissa detaljer i SOAP kuvert, såsom vissa rubriker och attribut, som inte är kopplade till säkerhet. Här är en TulaFale term för en SOAP begäran, som illustrerar formatet för det första meddelandet i vårt exempel protokoll: Varje SOAP meddelande består av en XML <Envelope> element, med två barn: en valfri <Header > och en obligatorisk <Body>. I detta exempel har rubriken fyra barn, och kroppen har en Id-attribute, den bokstavliga strängen "1". Vi baserar TulaFale på en sorterad (eller typad) term algebra, uppbyggd från en uppsättning funktionssymboler och variabler. De grundläggande typerna för XML-data inkluderar sträng (för bokstavssträngar), att (för namngivna attribut) och objekt (antingen ett element eller en sträng). Varje element eller attributtag (t.ex. Kuvert eller Id) motsvarar en sorterad funktionssymbol i den underliggande algebran. Även om TulaFale syntax är nära XML-trådformat, är det inte identiskt. Vi undertrycker all information om namnrymden. Som tidigare nämnts utelämnar vi att stänga elementtaggar; till exempel skriver vi </> istället för </Envelope>. Bokstavliga strängar citeras alltid, som i <Created>"2004-03-19T09:46:32Z" </>. I standardformatet för tråd, skulle dubbla citat utelämnas när en sträng är en elementkropp. Vi använder citat för att skilja strängar från termer variabler, såsom variablerna uri, ac, id, utok, sig, och begära i exemplet ovan. I TulaFale representerar vi kryptografiska algoritmer symboliskt, som funktionssymboler som agerar på en sorts bytes av byte arrayer. Varje funktion är antingen en data konstruktör, utan medföljande omskrivning regel, eller det är en destructor, utrustad med en omskrivning regel för att testa eller extrahera data från en tillämpning av en konstruktör. Krypteringsfunktioner är till exempel konstruktörer och dekrypteringsfunktioner är destructors. Detta tillvägagångssätt, grunden för Dolev-Yao-modellen [DY83], antar 9 att den underliggande kryptografin är perfekt, och kan troget återspeglas av abstrakta ekvationsegenskaper hos funktionerna. Den abstracterar också några detaljer, såsom längden på strängar och byte arrayer. Den TulaFale syntax för att införa konstruktörer och destructors är baserad på den syntax som används av ProVerif. Till exempel deklarerar vi funktionssymboler för RSA-nyckelgenerering, kryptering med öppen nyckel och avkryptering med hjälp av följande TulaFale-deklarationer: konstruktör pk(byte):bytes. konstruktör rsa(bytes, bytes):bytes. Destructor decrsa( bytes, byte): bytes med decrsa(s,rsa(pk(s),b) = b. Konstruktören pk representerar förhållandet mellan privata och offentliga nycklar (båda byte arrayer, av sort bytes); det tar en privat nyckel och returnerar motsvarande offentliga nyckel. Det finns ingen omvänd eller destructor, eftersom vi avser att representera en enkelriktad funktion: givet endast pk(s) det är omöjligt att extrahera s. konstruktören rsa(k,x) krypterar data x:bytes under den offentliga nyckeln k, vilket producerar en krypterad byte array. Destructor decrsa(s,e) använder motsvarande privata nyckel s för att dekryptera en byte array som genereras av rsa(s),x. Destructordefinitionen uttrycker dekrypteringsfunktionen som en omskrivningsregel: när en tillämpning av decrsa i en term matchar den vänstra sidan av regeln, kan den ersättas med motsvarande höger sida. För att deklarera RSA public-key signatures, introducerar vi en annan konstruktör rsasha1(s,x) som producerar en RSA signatur av en kryptografisk hash av data x under den privata nyckeln s: konstruktör rsasha1(bytes,bytes):bytes. Destructor checkrsasha1(bytes, bytes, byte):bytes med checkrsasha1(pk(s),x,rsasha1(s,x))=pk(s). För att kontrollera giltigheten av en signatur sig på x med hjälp av en offentlig nyckel k, kan man bilda termen checkrsasha1( k,x,sig) och jämföra den med k. Om k är en offentlig nyckel i formuläret pk(s) och sig är resultatet av signering x under motsvarande privata nyckel s, då skrivs denna term om till k. I detta papper binder ett X.509 certifikat en nyckel till ett ämnesnamn genom att inbädda en digital signatur som genereras från den privata nyckeln hos någon attesterande myndighet (CA). Vi deklarerar X.509 certifikat enligt följande: konstruktör x509(bytes, sträng, sträng, bytes):bytes. Destructor x509key(byte):bytes med x509key(x509(s,u,a,k))=k. Destructor x509user(byte):sträng med x509user(x509(s,u,a,k))=u. Destructor x509alg(byte):sträng med x509alg(x509(s,u,a,k))=a. Destructor checkx509(bytes, byte):bytes med checkx509(x509(sr,u,a,k),pk(sr)=pk(sr). Termen x509 (sr,u,a,k) representerar ett certifikat som binder ämnesnamnet u till den öppna nyckeln k, för användning med signaturalgoritmen a (vanligtvis rsasha1). Detta certifikat är signerat av CA med privat nyckel sr. Med ett sådant certifikat, destructors x509key, x509user, och x509alg extrahera de tre offentliga fälten av certifikatet. Ungefär som checkrsasha1 för vanliga digitala signaturer, kan en ytterligare destructor checkx509 användas för att kontrollera äktheten av den inbyggda signaturen. Därefter skriver vi logiska predikat för att konstruera och tolka XML krypterad under någon känd RSA offentlig nyckel. Ett predikat skrivs med hjälp av en Prolog-liknande syntax; det tar en tuple av termer och kontrollerar logiska egenskaper, såsom om två termer är lika eller om en term har ett specifikt format. Det är bra att tänka på några av de termer som ges till predikatet som ingångar och de andra som utgångar. Enligt denna tolkning beräknar predikatet utdatatermer som uppfyller de logiska egenskaperna genom mönstermatchning. Predikatet mkEncryptedData tar en vanlig text:item och en RSA offentlig krypteringsnyckel ek:bytes, och det genererar ett XML-element krypterat som innehåller XML-kodning av vanlig krypterad under ek. predicate mkEncryptedData (krypterad:item,plain:item,ek:bytes) :– chiffer = rsa(ek,c14n(plain)), krypterad = <EncryptedData> <CiferData> <CiferValue>base64(chiffer) </> </> </> Den första bindningen i predikatdefinitionen beräknar den krypterade bytesmatrisen, chiffer, med hjälp av den rsa-krypteringsfunktion som tillämpas på nyckeleket och klartextsslätten. Eftersom rsa endast definieras över byte arrays, är vanlig:item först konverteras till bytes med hjälp av (reversibel) c14n konstruktör. Den andra bindningen genererar ett XML- element (<EncryptedData>) som innehåller de krypterade bytena. Eftersom endast strängar eller element kan inbäddas i XML-element, konverteras den krypterade byte-matrisen, chiffer, först till en sträng med hjälp av (reversibel) base64-konstruktören. I detta papper använder vi tre transformationsfunktioner mellan olika typer: c14n (med invers ic14n) transformerar ett objekt till en bytes, bas64 (med invers ibase64) transformerar en bytes till en sträng, och utf8 (med invers iutf8) transformerar en sträng till en bytes. Alla tre funktionerna har specifika betydelser i samband med XML-omvandlingar, men vi behandlar dem helt enkelt som tvångsfunktioner mellan olika typer. För att bearbeta ett givet element, låt oss säga att vi ibland skriver tydliga predikat på sändarsidan respektive på mottagningssidan av protokollet. Enligt överenskommelse, för att konstruera ett <Foo> element, skriver vi en predikat som heter mkFoo vars första parameter är det element som konstrueras; för att tolka och kontrollera det, skriver vi en predikat som heter isFoo. För <EncryptedData>, till exempel, är det logiska predikatetEncryptedData tolkar element som konstruerats av mkEncryptedData; det tar ett element krypterat 11 och en dekrypteringsnyckel dk:bytes och, om krypterat är ett <EncryptedData> element med någon vanlig text krypterad under motsvarande krypteringsnyckel pk(dk), returnerar det den enkla texten som vanlig. predicate isEncryptedData (krypterad:item,plain:item,dk:bytes) :— krypterad = <CryptedData> <CipherData> <CipherValue>base64(chiffer) </> </>, c14n(plain) = decrsa(dk, chiffer). Abstractly, detta predicate reverserar de beräkningar som utförs av mkEncryptedData. En skillnad, naturligtvis, är att medan mkEncryptedData passerar den offentliga krypteringsnyckeln ek, är isEncryptedData predicate istället passerade den privata nyckeln, DK. Den första raden matchar krypterad mot ett mönster som representerar elementet <EncryptedData> och extraherar det krypterade bytesystemet, chiffer. konstruktören bygger på mönstermatchning och är implicit inverterad med hjälp av sin destructor ibase64. Den andra raden dekrypterar chiffer med hjälp av dekrypteringsnyckeln dk, och implicit inverterar c14n med hjälp av dess destructor ic14n för att beräkna vanlig. Tjänster och X509 Security Tokens
I REF har ett verktyg för säkerhetsverifiering av WS skapats som möjliggör översättning av säkerhetskonfigurationer i WS-SecurityPolicy till TulaFale språk som sedan verifieras för korrekthet med hjälp av formella logik-baserat resonemang.
TulaFale: A Security Tool for Web Services
{'venue': 'ArXiv', 'journal': 'ArXiv', 'mag_field_of_study': ['Computer Science']}