공격자가 아는 정보
비밀값, 공개 채널, 암호 연산과 참여자의 메시지 교환을 모델로 정의한다. 이어 공격자가 특정 값을 알아낼 수 있는지 같은 질문을 작성한다. 분석은 명시한 연산 규칙과 공격자 능력 안에서 이루어진다.
프로토콜 설계의 점검
메시지가 암호화되어 있다는 사실만으로 상대방의 신원을 올바르게 확인한다고 볼 수 없다. ProVerif는 참여자의 행동을 조합해 보안 조건을 깨는 흐름을 분석하는 데 쓰인다. 어떤 메시지를 누가 만들고 누구의 키로 확인하는지가 모델에서 중요하다.
모델과 구현 구분하기
기호 모델의 보안 성질은 실제 프로그램의 메모리 안전성이나 난수 구현 품질과 다른 문제다. 라이브러리 바이너리를 실행하며 취약점을 찾는 도구로 해석하면 안 된다. 검증 대상은 작성한 프로토콜 모델과 질문이며, 구현의 추가 가정은 별도로 점검한다.