비공식 증명만으로는 충분하지 않은 이유

프로토콜 설계자는 공격자가 성공할 수 없는 이유를 설명하는 비공식적인 보안 논증을 작성하는 경우가 많습니다. 그러나 역사적으로 이러한 논증은 전문가가 설계한 프로토콜에서도 자주 틀린 것으로 드러났습니다.

Needham-Schroeder(1978)는 상호 인증을 위해 설계되었습니다. 1995년에 Gavin Lowe는 자동화된 검증을 사용해 중간자 공격을 발견했습니다. 프로토콜이 발표된 지 17년이 지난 시점이었습니다. 비공식 증명은 미묘한 재전송 공격을 놓쳤습니다.

WEP는 비공식적인 보안 주장을 바탕으로 1997년 IEEE의 승인을 받았습니다. 2001년까지 연구자들은 RC4 키 스트림 재사용, IV 충돌 및 무결성 부재를 발견했고, 이로 인해 WEP는 몇 분 만에 무너졌습니다. 비공식적인 추론은 이 모든 문제를 놓쳤습니다.

프로토콜 보안은 동시에 실행되는 여러 세션, 능동적 공격자 및 암호학적 가정 사이의 상호 작용에 좌우됩니다. 사람의 추론만으로는 상태 폭발과 서로 뒤섞인 동시 실행을 다루기 어렵습니다.

형식 기법은 프로토콜을 수학적으로 모델링하고, 설계자가 고려한 공격 전략뿐 아니라 가능한 모든 공격자 전략에 대해 보안 속성(기밀성, 인증, 순방향 비밀성)을 증명하거나 반증합니다.

기호 모델(Dolev-Yao): 암호를 완벽한 블랙박스로 보고 프로토콜 논리에 집중합니다. 계산 모델: 실제 확률적 보안 게임을 사용하므로 현실의 보장에 더 가깝습니다. 두 모델 모두 실제 버그를 발견할 수 있습니다.

POODLE(2014)은 SSL 3.0 CBC의 패딩 오라클을 악용했습니다. 이 취약점은 구현 버그가 아니라 프로토콜 수준의 설계 결함이었습니다. SSL 3.0 사양을 형식적으로 분석했다면 배포 전에 이 오라클을 발견했을 것입니다.

TLS 1.3(RFC 8446)은 ProVerif와 miTLS를 사용한 형식 분석과 함께 설계되었습니다. 형식 분석 결과를 바탕으로 사양을 반복적으로 개선했으며, 이는 표준화 기구가 형식 기법을 도입한 중요한 이정표입니다.

형식 도구는 구현이 아니라 프로토콜 모델을 검증합니다. 따라서 형식 검증을 거친 프로토콜도 안전하지 않게 구현될 수 있습니다. F* / HACL*은 암호화 코드 자체까지 검증 범위를 확장합니다.

형식 검증에는 많은 비용이 듭니다. 프로토콜 모델링에는 몇 주가 걸리고 전문 지식이 필요합니다. 그러나 TLS, SSH, Signal과 같은 고가치 대상에는 그 비용이 정당화됩니다. 프로토콜 결함 하나가 수십억 명의 사용자에게 영향을 줄 수 있기 때문입니다.

비공식 증명은 사람이 동시 세션 간의 상호 작용과 공격자 전략을 놓치기 때문에 실패합니다. Needham-Schroeder, WEP 및 POODLE에는 모두 비공식적인 보안 논증이 있었습니다. TLS 1.3은 설계 과정에 형식 분석을 도입했습니다. 형식 도구는 배포 전에 프로토콜 수준의 버그를 발견합니다.