EduCrypt: an educational tool for learning game-based cryptographic proofs

This thesis presents EduCrypt, an interactive educational tool designed to make game-based cryptographic proofs more accessible to students. Motivated by the difficulty learners face when confronting formal cryptographic arguments, EduCrypt adopts the game-playing technique that conveys proofs as sequences of probabilistic programs. A simple, student-oriented language called EduCrypt Games (ECG) is introduced to express these games. The language is integrated into an interface that allows users to write and inspect games, visualize transformations between games, and input proof steps, emphasizing immediate feedback and exploratory learning. The work describes the design goals, the ECG language, and the implementation of the multiplatform application targeting desktop and web environments using Kotlin. It discusses the internal representation and tool architecture, and demonstrates usage by presenting multiple examples. The thesis concludes by identifying the limitations of the current implementation, and outlining possible future directions and a roadmap for future developments.