실행 검사와 안전성 논증
몇 개의 입력에서 암호 코드가 동작한다는 결과와 공격자가 얻을 수 있는 이점을 논증하는 일은 다르다. EasyCrypt는 확률적 계산의 관계를 증명하고 게임 사이의 변환을 통해 보안 주장을 구성한다. 어떤 공격 능력과 확률 모델을 허용하는지가 논증의 의미를 결정한다.
명세와 구현의 관계
암호학적 논증 외에 저수준 구현이 고수준 명세와 일치하는지 확인하는 작업에도 활용된다. 특히 Jasmin과의 연동이 안내되어 있다. 특정 성질이 증명되었다고 구현의 모든 성능 특성이나 운영 환경의 보안까지 자동으로 보장되는 것은 아니다. 증명한 계약과 환경 가정을 명확히 구분한다.
증명 환경 구성
Why3와 외부 SMT solver를 연결하고 명령행이나 증명 편집 환경에서 작업한다. 각각 독립적으로 버전이 바뀌므로 지원되는 조합을 확인해야 한다. 증명기를 설치하거나 갱신한 뒤 연결 설정도 다시 확인한다. 자동 증명으로 해결되지 않은 조건은 증명 전략이나 명세 및 실제 문제를 구분해 조사하며 증명 스크립트와 실행 환경을 함께 유지한다.