Industrial Use of Formal Methods for a High-Level Security Evaluation

摘要: This paper presents an effective use of formal methods for the development and security certification smart card software. The approach is based on Common Criteria's methodology that requires to prove a product implements claimed level. work led world-first commercial Java CardTMproduct involving all assurances needed reach highest For this certification, have been used design implementation functions Card system embedded in product. We describe refinement scheme meet requirements models proofs. In particular, we show how build proof ensures objectives specification. also provide some lessons learned from important application cards industry.