Protokollverifisering

Protokollverifisering er studiet og evalueringen av sikkerhetsprotokoller for å bekrefte at de oppfyller ønskede egenskaper, som konfidensialitet, autentisering og integritet, også i møte med angrep og feil i kommunikasjonen. Hovedmålet er å avdekke potensielle svakheter og å verifisere at protokollen gir ønskede sikkerhetsgarantier under et definert trussel- og angrepsmodell.

Metodisk bygger protokollverifisering ofte på formelle modeller som bruker symbolsk analyse fremfor direkte beregningsbasert simulering. Den vanligste modellen antar en Dolev–Yao-intrusjon, der angriperen kan avlytte, endre, sette inn og videresende meldinger men ikke bryte kryptografiske innpakninger uten nøklene. Resultatet er ofte angitt som bevis på egenskapene som autentisering eller konfidensialitet, eller mot ekvivalente motsetninger og moteksempler (counterexamples).

Vanlige metoder inkluderer symbolsk analyse, modellkontroll og bevisbaserte tilnærminger. Verktøy som ProVerif og AVISPA utfører automatisert symbolsk analyse for å verifisere sikkerhetsmål, mens Tamarin prover kombinerer innføring av tids- og multiset-regnskapsregler med bevis for samtidige egenskaper. Andre tilnærminger inkluderer BAN-logikk og strandromanalyse, som gir prosedyrer for å reasonere om agenters tro og forventninger.

Begrensninger inkluderer forenkling av beregningsmessige kalkulasjoner og behovet for realistiske antagelser om angriperens kapasitet. Resultatene av protokollverifisering gir ofte konklusjoner om sikkerhetsegenskaper under spesifiserte modeller, men gir ikke alltid endelig garanti i alle operative forhold. Til tross for dette utgjør protokollverifisering et viktig trekk i utvikling og sertifisering av kryptografiske protokoller.