Varför informella bevis inte räcker

Protokolldesigners formulerar regelbundet informella säkerhetsargument – resonemang i löptext om varför en angripare inte kan lyckas. Historien visar att dessa argument ofta är felaktiga, även för protokoll som utformats av experter.

Needham-Schroeder (1978) utformades för ömsesidig autentisering. År 1995 upptäckte Gavin Lowe en man-in-the-middle-attack med hjälp av automatiserad verifiering – 17 år efter publiceringen. Det informella beviset missade en subtil replay-attack.

WEP godkändes av IEEE 1997 med informella säkerhetspåståenden. År 2001 upptäckte forskare återanvändning av RC4-nyckelströmmen, IV-kollisioner och bristande integritet – vilket gjorde det möjligt att knäcka systemet på minuter. Det informella resonemanget missade allt detta.

Protokollsäkerhet beror på samspel mellan många samtidiga sessioner, aktiva angripare och kryptografiska antaganden. Mänskligt resonemang har svårt att hantera tillståndsexplosioner och interfolierade samtidiga körningar.

Formella metoder modellerar protokollet matematiskt och bevisar – eller motbevisar – säkerhetsegenskaper (sekretess, autentisering och forward secrecy) för alla möjliga angriparstrategier, inte bara de som designern övervägde.

Symbolisk (Dolev-Yao): kryptografi är en perfekt svart låda; fokus ligger på protokollogik. Beräkningsbaserad: faktiska probabilistiska säkerhetsspel, närmare garantier i verkligheten. Båda upptäcker verkliga buggar.

POODLE (2014) utnyttjade ett padding-orakel i SSL 3.0 CBC. Sårbarheten var ett designfel på protokollnivå, inte ett implementeringsfel. En formell analys av SSL 3.0-specifikationen skulle ha upptäckt oraklet före driftsättningen.

TLS 1.3 (RFC 8446) utformades parallellt med formella analyser med ProVerif och miTLS. Specifikationen omarbetades utifrån resultaten av den formella analysen – en milstolpe i standardiseringsorganens införande av formella metoder.

Formella verktyg verifierar protokollmodellen, inte implementationen. Ett formellt verifierat protokoll kan fortfarande ha en osäker implementation. F* / HACL* utvidgar verifieringen till själva den kryptografiska koden.

Formell verifiering är kostsam: modellering av protokoll tar veckor och kräver specialistkompetens. Men för mål med högt skyddsvärde (TLS, SSH, Signal) är kostnaden motiverad – ett enda protokollfel kan påverka miljarder användare.

Informella bevis brister eftersom mänskligt resonemang missar samspel mellan samtidiga sessioner och angriparstrategier. Needham-Schroeder, WEP och POODLE hade alla informella säkerhetsargument. TLS 1.3 integrerade formell analys under designfasen. Formella verktyg upptäcker protokollfel innan driftsättning.