Verzweigungen aussagenlogisch erfassen?

[*Markus]

Hallo,

durch eine komplizierte Abfolgelogik einer Seite, die ich gerade mit Java und Tomcat erstelle, stoße ich immer wieder auf logisch widersprüchliche Verzweigungen, zB

Wenn d. User zum allerersten Mal auf die Seite kommt, soll die "Willkommen"-Seite geladen werden.

Hat der User sich aber bereits registriert, soll er sich gleich einloggen, aber auch nur dann, wenn er es beim Anmelden oder letzten Einloggen explizit angab.

Schaltet der User aus welchen Gründen auch immer Cookies plötzlich aus, soll er ausgeloggt werden und auf der "Willkommen"-Seite landen.

Bricht der User den Registrierungsvorgang ab zB mit den Back-Buttons, darf er trotzdem nicht in interne Seiten gelangen (zB durch einen Folgefehler von gesetzten Cookies oder initialisierten Sessions). Er darf sich wiederum nur auf der Willkommen-Seite bewegen.

usw usw ....

Eigentlich geht das noch ein paar Mal so weiter, wodurch es anfängt, richtig kompliziert zu werden, da man jetzt noch Tomcateigenheiten beachten muss, zB

Eine Session gibt es erst, nachdem die 1. Seite geladen wurde. Somit würde auf ein if (session == null) ab dem 2. Mal anders reagiert werden. Hinzu kommt das Logincookie, das einem die Möglichkeit geben soll, automatisch einzuloggen, wenn man bereits Mitglied ist. Jetzt muss man schon auf zwei Cookies je nach Seite und Reihenfolge der Seitenaufrufe unterschiedlich reagieren.

Wäre es ev. möglich, jedes Verhalten aussagenlogisch so zu erfassen und auf das Ergebnis herunterzubrechen, sodass man im Endeffekt weiß, wie man wann welche Cookies erstellen oder abfragen muss?
Wie könnte ich da vorgehen?

Markus