The KeY Approach for the Cryptographic Verification of Java Programs: A Case Study Bernhard Beckert, Daniel Bruns, Ralf Küsters, Christoph Scheben, Peter H. Schmitt, and Tomasz Truderung In this paper, we report on an ongoing case study in which we use the KeY tool, a theorem prover for checking functional correctness and noninterference properties of Java programs, to establish computational indistinguishability for a simple Java program that involves clients sending encrypted messages over an untrusted network to a server. The analysis uses a general framework, recently proposed by Küsters et al., which enables program analysis tools, such as KeY, that can check (standard) noninterference properties for Java programs to establish computational indistinguishability properties.