En tråd är en sekvens av händelser; den representerar antingen verkställandet av legitim part i ett säkerhetsprotokoll eller en sekvens av åtgärder av en penetrator. Ett strandutrymme är en samling av trådar, utrustade med en grafstruktur som genereras av kausal interaktion. Inom denna ram kan påståenden om protokollets korrekthet uttryckas i termer av sambanden mellan trådar av olika slag. I detta dokument utvecklar vi begreppet strandutrymme. Vi bevisar sedan en allmänt användbar lemma, som ett prov resulterar i att en allmän bunden på förmågan hos penetratorn i något protokoll. Vi tillämpar rymdformalismen för att bevisa riktigheten i Needham-Schroeder-Lowe-protokollet. Vårt tillvägagångssätt ger en detaljerad bild av de förhållanden under vilka protokollet uppnår autentisering och skyddar sekretessen för de värden som utbyts. Vi använder också våra bevismetoder för att förklara varför det ursprungliga Needham-Schroeder-protokollet misslyckas. Vi anser att vårt tillvägagångssätt skiljer sig från annat arbete om protokollverifiering genom enkelheten i modellen och lättheten att producera begripliga och tillförlitliga bevis för protokoll korrekthet även utan automatiskt stöd.
Athena [43] bygger på en ändring av strandrymdmodellen REF.
Strand spaces: why is a security protocol correct?
{'venue': 'Proceedings. 1998 IEEE Symposium on Security and Privacy (Cat. No.98CB36186)', 'journal': 'Proceedings. 1998 IEEE Symposium on Security and Privacy (Cat. No.98CB36186)', 'mag_field_of_study': ['Computer Science']}