Abstrakt. Ett antal aktuella automatiserade protokollverifieringsverktyg baseras på abstrakta tolkningstekniker och andra över- approximationer av uppsättningen av nåbara tillstånd eller spår. De protokollmodeller som dessa verktyg använder formas av behovet av automatisk verifiering och kräver subtila antaganden. Dessutom kan ett komplext verifieringsverktyg lida av implementation buggar så att i värsta fall verktyget kan acceptera några felaktiga protokoll som är korrekt. Dessa risker för fel är också närvarande, men betydligt mindre, när man använder en LCF-teoretiker som Isabelle. Det interaktiva säkerhetsbeviset kräver dock mycket expertis och tid. Vi kombinerar fördelarna med båda världarna genom att använda representationen av det över approximerade sökområdet som beräknas av de automatiserade verktygen som en "säker idé" i Isabelle. Vi utformar alltså bevistaktik för Isabelle som genererar korrekturbeviset för protokollet från utmatningen av de automatiserade verktygen. I värsta fall misslyckas denna taktik med att konstruera ett bevis, nämligen när återgivningen av sökområdet av någon anledning är felaktig. Men när de lyckas förlitar sig korrektheten bara på grundmodellen och Isabelle-kärnan.
Det andra REF använde sig av Theorem-bevisaren Isabelle och beräknade en fast punkt för en abstraktion av övergångsförhållandet i protokollet av intresse - denna fast punkt över-uppskattar uppsättningen av nåbara tillstånd i protokollet.
Integrating Automated and Interactive Protocol Verification
{'venue': 'Formal Aspects in Security and Trust', 'journal': None, 'mag_field_of_study': ['Computer Science']}