프로토콜을 모델로 표현하기
참여자가 메시지를 보내고 상태를 바꾸는 과정을 규칙으로 작성한다. 공격자가 알고 있는 정보와 네트워크 메시지도 모델의 일부다. 암호 연산은 수학적 성질을 반영한 기호 표현으로 다루므로 실제 암호 라이브러리의 바이너리를 직접 검사하는 방식과는 다르다.
무엇을 증명하는가
명시한 모델에서 비밀 유지나 인증에 필요한 조건을 검토할 수 있다. 여러 프로토콜 실행이 병렬로 섞이는 상황도 분석 대상이다. 결과의 의미는 참여자의 규칙, 공격자 능력, 확인할 속성을 어떻게 정했는지에 따라 달라진다.
탐색이 끝나지 않는 경우
자동 탐색이 종료하면 증명이나 속성을 깨는 공격 경로를 얻을 수 있지만, 모든 입력에서 종료가 보장되는 것은 아니다. 복잡한 모델에서는 증명 상태와 공격 그래프를 확인하며 탐색을 유도한다. 시간이 오래 걸린다는 사실 자체는 안전성의 증거가 아니다.