Abstrakt. SET (Secure Electronic Transaction) är en uppsättning protokoll som föreslås av ett konsortium av kreditkortsföretag och programvaruföretag för att säkra e-handelstransaktioner. Inköpsdelen av sviten är avsedd att garantera integriteten och äktheten av betalningstransaktionen samtidigt som kortinnehavarens kontouppgifter hålls hemliga från Merchant och hans val av varor hemlig från banken. I detta dokument beskrivs de första verifieringsresultaten för SET:s fullständiga inköpsprotokoll. Med hjälp av Isabelle och den induktiva metoden visar vi att deras primära mål verkligen uppfylls. Bristen på uttrycklighet i den dubbla signaturen gör dock att vissa avtalsegenskaper misslyckas: det är omöjligt att bevisa att Kortinnehavaren avsåg att skicka sina kreditkortsuppgifter till själva betalningsingången som tar emot dem. En stor insats i kontrollen gjordes för att smälta SET-dokumentationen för att ta fram en realistisk modell. Protokollets komplexitet och storlek gör det svårt att verifiera jämfört med andra protokoll. Men våra ansträngningar har gett betydande insikter.
Bella och Al. REF använder Isabelle för att analysera SET:s fullständiga inköpsprotokoll och finner att om man äger bristen på explicithet i den dubbla signaturen så misslyckas vissa avtalsegenskaper: det är omöjligt att bevisa att Kortinnehavaren menade att skicka sina kreditkortsuppgifter till själva betalningsingången som tar emot dem.
Verifying the SET Purchase Protocols
{'venue': 'Journal of Automated Reasoning', 'journal': 'Journal of Automated Reasoning', 'mag_field_of_study': ['Computer Science']}