Lab 2 - Task 6 PROP_AB

Boddlnagg
Mausschubser
Mausschubser
Beiträge: 54
Registriert: 10. Dez 2012 12:07

Lab 2 - Task 6 PROP_AB

Beitrag von Boddlnagg »

Moin,

Wir sind mit unserem Model soweit fertig, allerdings können wir am Ende in Task 6 die Eigenschaft (1) PROP_AB nicht verifizieren. Im Gegenbeispiel passiert folgendes:
Der Intruder startet das Protokoll mit Bob und es läuft vollständig durch. Danach ist Bob's Status auf "OK".
Dann startet Alice das Protokoll und wählt (wie in Task 4 vorgesehen) den Intruder als partnerA. Auch dieses Protokoll läuft komplett durch, sodass auch Alice's Status am Ende auf "OK" ist. Allerdings ist nun
partnerA = agentI und partnerB = agentI.
Von meiner Intuition her würde ich jetzt mal sagen, dass das ein legaler Fall ist, denn sowohl Alice als auch Bob reden tatsächlich mit dem, mit dem sie meinen zu reden. Allerdings ist dieser Fall in der zu verifizierenden Eigenschaft nicht vorgesehen.

Haben wir was übersehen oder wie sollen wir damit umgehen?

LG,
Patrick

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab 2 - Task 6 PROP_AB

Beitrag von Nathan Wasser »

Alice und Bob sollten beim initialisieren ihren gewählten Partner für die Kommunikation aussuchen. Bei Alice darf das dann ab Task 4 nichtdeterministisch erfolgen, bei Bob sollte es nachwie vor immer Alice sein.

Boddlnagg
Mausschubser
Mausschubser
Beiträge: 54
Registriert: 10. Dez 2012 12:07

Re: Lab 2 - Task 6 PROP_AB

Beitrag von Boddlnagg »

D.h. auch wenn der Intruder das Protokoll mit Bob beginnt (und Bob mitteilt, dass er der Intruder ist) soll Bob davon ausgehen, dass er mit Alice redet, verstehe ich das richtig? Das würde das Problem vermutlich lösen.

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab 2 - Task 6 PROP_AB

Beitrag von Nathan Wasser »

Naja, er soll von Anfang an nur mit Alice reden wollen. Er geht aber nicht davon aus, sondern überprüft die Mitteilung um dies zu überprüfen.

Boddlnagg
Mausschubser
Mausschubser
Beiträge: 54
Registriert: 10. Dez 2012 12:07

Re: Lab 2 - Task 6 PROP_AB

Beitrag von Boddlnagg »

Vielen Dank, hat jetzt geklappt!

Antworten

Zurück zu „Archiv“