Tamarin, ProVerif 등 암호 프로토콜 검증 도구는 널리 쓰이지만 사용자 경험 측면은 상대적으로 연구가 부족했다. 연구진은 이들 도구를 실제로 사용해본 연구자·대학원생·실무자를 대상으로 탐색적 인간 중심 설문 연구를 진행해, 비종료 문제와 성능 문제 디버깅의 어려움, 형식 모델을 실제 프로토콜과 대조 검증할 체계적 방법의 부재 등 검증 워크플로 전반의 사용성 장벽을 밝혀냈다. 증명이 구체적 공격 없이 실패할 경우 사용자들은 모델을 단순화하거나 보조 引理를 추가하거나 모델링 추상화를 재검토하는 방식으로 대응하는 경향을 보였고, 실행 가능한 진단 정보와 결과에 대한 명확한 설명, 시각화, 반복 증명 작업의 자동화를 요구했다. 연구진은 프로토콜 수준 추론과 검증기의 형식 모델·증명 절차·진단 출력 사이의 간극에서 사용성 문제가 비롯된다고 결론짓고, 접근성·해석 가능성·사용성 개선을 위한 구체적 설계 우선순위를 도출했다.

• •Tamarin·ProVerif 경험자 대상 탐색적 인간 중심 사용성 설문 연구 수행
• •비종료·성능 문제 디버깅 어려움과 형식 모델-실제 프로토콜 검증 방법 부재 확인
• •증명 실패 시 모델 단순화·보조 인리에 추가·추상화 재검토로 대응하는 사용자 패턴 발견
• •실행 가능한 진단·결과 설명·시각화·자동화를 해결책으로 제안