@TechReport{BeckertBrunsKuestersEtAl12, author = {Bernhard Beckert and Daniel Bruns and Ralf K\"{u}sters and Christoph Scheben and Peter H. Schmitt and Tomasz Truderung}, title = {The {\KeY} Approach for the Cryptographic Verification of {J}ava Programs: {A} Case Study}, institution = {Department of Informatics, Karlsruhe Institute of Technology}, number = {2012-8}, year = 2012, month = aug, series = {Karlsruhe Reports in Informatics}, language = {english}, url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000027497}, urn = {urn:nbn:de:swb:90-274973}, license = {http://creativecommons.org/licenses/by-nc-nd/3.0/}, abstract = {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{\"u}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.} }