Source Code Verification of a Secure Payment Applet

Some files, links, and 'special features' related to the Java Card secure payment application studied in [1]. This paper discusses a case study in formal verification and development of secure smart card applications. An elementary Java Card electronic purse applet is presented whose specification can be simply formulated as "in normal operation, the applet's balance field can only be decreased, never increased". The applet features a challenge-response mechanism which allows legitimate terminals to increase the balance by putting the applet into a special operation mode. A systematic approach is used to guarantee a secure flow of control within the applet: appropriate transition properties are first formalized as a finite state machine, then incorporated in the specification, and finally formally verified using the Loop translation tool and the PVS theorem prover.

Download

	PayApplet.java	The pay applet. Java source code annotated with JML.
	PayApplet_user.prf	The user proof file. PVS proof file.
	setKeyProof.pdf	Proof tree for the setKey method.
	getValueProof.pdf	Proof tree for the getValue method.
	decValueProof.pdf	Proof tree for the decValue method.
	respondProof.pdf	Proof tree for the respond method.
	getChallengeProof.pdf	Proof tree for the getChallenge method.

Links

	Java Card	The Java Card Home Page.
	JML	The JML Home Page.
	PVS	The PVS Home Page.
	Verificard	The Verificard project Home Page.

References