I denna undersökning analyserades rörelsefunktionen i Marvel's Spider-Man 2. Bakgrundskapitlet beskriver de 31 olika element av spelkänsla samt vad begreppen system, funktion och mekanik betyder. Problemformuleringen presenterar metoden for formell analys. I problemformuleringen presenteras även frågeställningen, vilket lyder som följande: Hur använder Marvel's Spider-Man 2 olika element av spelkänsla inom spelets rörelsesystem och hur är detta rörelsesystem uppbyggt? Den formella analysen producerade kvalitativa data som användes for att besvara hur rörelsesystemet är uppbyggt, spelets primitiver och hur element av spelkänsla ar tillämpat i rörelsesystemet. Resultatet visade att spelet använder majoriteten av elementen av spelkänsla och att rörelsesystemet har en hög grad framväxande gameplay med mycket virtuell skicklighet. Ett potentiellt framtida arbete kan vara att undersöka fler spel genom samma metod for att se likheter och skillnader i spelens rörelsefunktioner.

Formal analysis of security protocols is becoming increasingly relevant. In formal analysis, a model is created of a protocol or system, and propositions about the security of the model are written. A program is then used to verify that the propositions hold, or find examples of where they do not. This report uses formal methods to analyse the authentication aspect of a protocol that allows private individuals, enterprises, and systems to securely and asynchronously share sensitive data. Unpublished, early drafts of the protocol were studied and algorithms described in it were verified with the help of the formal verification tool Tamarin Prover. The analysis revealed two replay attacks. Improvements to the protocol were suggested based on this analysis. In later versions of the protocol, the improvements have been implemented by the protocol developers. / Det blir alltmer relevant med formell analys av säkerhetsprotokoll. I formell analys så skapas en modell av ett protokoll eller ett system, och påståenden om modellens säkerhet skrivs. Ett program används sedan för att verifiera att påståendena gäller, eller för att hitta exempel där de inte gäller. Den här rapporten avänder formella metoder för att analysera autentiseringsaspekten av ett protokoll som tillåter privatpersoner, företag och system att asynkront dela känslig information på ett säkert sätt. Opublicerade och tidiga utkast av protokollet studerades och de algoritmer som beskrivs i protokollet verifierades med hjälp av Tamarin Prover. Analysen avslöjade två återspelningsattacker. Förbättringar till protokollet föreslogs baserat på denna analys. I senare versioner har protokollutvecklarna implementerat förslagen.