Seite 1 von 1

Lab 2 - Verifikation Bonus Task

Verfasst: 3. Dez 2012 22:47
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

Re: Lab 2 - Verifikation Bonus Task

Verfasst: 4. Dez 2012 12:11
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.

Re: Lab 2 - Verifikation Bonus Task

Verfasst: 4. Dez 2012 17:22
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