We have presented a method for the formal development of secure smartcard applications. The method combines and integrates different techniques (with algebraic specifications at the core) to tackle the different problems: objects and distributed systems, attackers and cryptographic protocols, JavaCard programs and limited resources. The techniques include UML models enriched by algebraic specifications, and dynamic logic for JavaCard verification. The method is tailored to take advantage of the special features of smartcard scenarios, and to make proving securityand correctness as easy as possible. The method is illustrated with a small but surprisinglyco mplex example, a copy card. The approach is implemented in the KIV specification and verification system.