2019년 도입된 대칭 프로토콜 검증기 '베리프팔(Verifpal)'이 엔진을 완전히 새로 교체했다는 사실을 이 논문이 처음으로 정식 기술한다. 기존 엔진은 전방 탐색으로 값 조합을 변형해 나갔지만, 새 엔진은 반증하려는 질의에서 출발해 이를 하위 목표로 분해하고 유일하게 해소 가능한 하위 목표마다 바인딩을 강제하는 목표 지향 방식으로 바뀌었다. 건전성은 솔버에 의존하지 않도록 설계돼, 솔버 버그가 공격을 놓칠 수는 있어도 거짓 공격을 만들어내지는 못한다. 언어도 단순해지고 표현력은 강화돼 공개키 암호에 특수 값이 필요 없어졌고, 각 주체가 여러 동시 세션을 갖도록 분석해 한 역할의 두 인스턴스가 필요한 공격도 탐지 범위에 들어왔다. 저자들은 베리프팔이 더 작아진 것이 아니라 완전히 다른 도구가 되었으며, 기존 두 경쟁 도구를 대체하기보다 나란히 사용할 가치가 있다고 결론짓는다.

• •전방 탐색 방식에서 질의를 하위 목표로 분해하는 목표 지향 방식으로 엔진을 완전 교체
• •건전성이 솔버에 의존하지 않도록 설계돼 솔버 버그가 거짓 공격을 만들 수는 없음
• •공개키 암호에 특수 값이 불필요해지는 등 언어 표현력 강화
• •동시 세션 다중 분석으로 한 역할의 두 인스턴스가 필요한 공격도 탐지 가능해짐
• •관찰적 동치·고정된 방정식 이론 등 한계는 여전하며 세션 수는 유한 범위로 제한