Lab 2 - Verifikation Bonus Task

florian.k
Neuling
Neuling
Beiträge: 5
Registriert: 3. Dez 2012 22:34

Lab 2 - Verifikation Bonus Task

Beitrag von florian.k »

Wir haben ein kleines Problem bei der Verifikation des Bonus Tasks. Der Angreifer handelt ja nicht deterministisch, und durch unsere Änderungen am Protokoll um die Probleme zu beheben, haben wir eine um ein vielfaches größere Zustandsmenge, sodass für jede der 3 LTLs jeweils ein Rechner, nach über 2Stunden Laufzeit immer noch kein Ergebniss lieferte. Ist es denn Ziel der Aufgabe, den Handlungsspielraum des Angreifers "sinvoll" einzuschränken um die Zustandsmenge kleiner zu halten. Das erscheint uns nicht so ganz logisch, da das Ziel ja eigentlich ist, jede noch so abstruse Kombination zu Überprüfen um die Sicherheit des Protokolls zu gewährleisten, oder sehen wir das falsch?

Haben andere ähnliche Probleme?

Viele Dank im Vorraus.

Gruß,
Florian

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

Re: Lab 2 - Verifikation Bonus Task

Beitrag von Nathan Wasser »

Wurde der Hinweis bei Aufgabe 5 berücksichtigt um Nichtdeterminismus einzuschränken?

Oder ist euer Protokoll jetzt vielleicht einfach viel zu kompliziert?

Was zählt alles zu "jede noch so abstruse Kombination"? Das Modell ist eh schon dadurch eingeschränkt, dass wir dem Intruder nur Werte aus mtype zulassen und auch nur die, die er kennt. Es kann ja ein richtiger Angreifer jede beliebige Bitfolge schicken.

Wir wissen doch, dass bei bestimmten Nachrichten einige Felder komplett ignoriert werden. Natürlich darf man dieses Wissen auch benutzen um die Zustandsmenge etwas zu reduzieren. Das wurde ja nicht ohne Grund bei Aufgabe 5 erwähnt.

errt
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 18. Okt 2012 19:12

Re: Lab 2 - Verifikation Bonus Task

Beitrag von errt »

Nathan Wasser hat geschrieben:Wurde der Hinweis bei Aufgabe 5 berücksichtigt um Nichtdeterminismus einzuschränken?
Ja, aber wir haben trotzdem > 80 Mio. States.
Nathan Wasser hat geschrieben:Oder ist euer Protokoll jetzt vielleicht einfach viel zu kompliziert?
Wir haben nicht mehr getan, als im Praktikum stand: Die Nachrichten um einen Eintrag erweitert, damit in msg2 eben eine Information mehr mitgeschickt werden kann.
Nathan Wasser hat geschrieben:Was zählt alles zu "jede noch so abstruse Kombination"? Das Modell ist eh schon dadurch eingeschränkt, dass wir dem Intruder nur Werte aus mtype zulassen und auch nur die, die er kennt. Es kann ja ein richtiger Angreifer jede beliebige Bitfolge schicken.
Wir wissen doch, dass bei bestimmten Nachrichten einige Felder komplett ignoriert werden. Natürlich darf man dieses Wissen auch benutzen um die Zustandsmenge etwas zu reduzieren. Das wurde ja nicht ohne Grund bei Aufgabe 5 erwähnt.
Wir haben aktuell nicht nicht nur die komplett zu ignorierenden Felder ignoriert, sondern auch andere Einschränkungen, da ja z.B. in msg1 das erste Datum immer ein Agent, nie ein Nonce ist, bei msg2 umgekehrt. Das reduzierte unsere Zustandsanzahl auf ~700.000. Die Frage ist nur, ob wir so große Änderungen am Intruder machen dürfen (die eigentlich sich nicht auswirken sollten, weil z.B. eine msg1 mit einer Nonce als erstem Datum ja von keinem Agenten akzeptiert wird) oder nicht.

Grüße,
Dominik

Antworten

Zurück zu „Archiv“