Resumen
This article discusses methods for establishing confidence that implementations meet their specifications and security requirements. Designing and building secure systems is must to build up the confidence among its users. Having confidence in the implementation of security mechanisms requires knowledge that the implementations are correct. Besides the normal testing and simulation to check correctness for specific test cases, formal verification using mathematical logic is possible and becoming more practical. The article concludes by suggesting that having confidence that a system is secure requires confidence in the cryptographic algorithms, confidence that the security mechanisms are implemented properly, and that the mechanisms themselves sup- port a security model. While the mathematical analysis necessary to reason about the cryptographic strength of algorithms may be beyond most system engineers, the type of mathematical logic used to analyze the correctness of implementations and trust relationships is not.