Quantum Cryptography and Autoformalization in Lean

보안 통신의 세계에서 가장 신뢰받는 자물쇠는 강철이 아니라 물리학의 근본 법칙으로 만들어집니다. 이것이 바로 양자 키 분배의 영역이며, 이는 전통적으로 앨리스(Alice)와 밥(Bob)이라 불리는 두 사람이 메시지를 보호하기 위해 공유된 비밀 코드를 생성하는 방법입니다. 복잡한 수학 문제를 푸는 난이도에 의존하는 전통적인 암호화와 달리, 이 방식은 빛의 아주 작은 입자인 광자(photon)를 측정하면 필연적으로 그것이 변한다는 사실에 의존합니다. 만약 이브(Eve)라는 이름의 제삼자인 도청자가 엿들으려 한다면, 그녀는 자신의 간섭 흔적을 감지 가능한 형태로 남기게 됩니다. 수십 년 동안 과학자들은 이러한 키를 만들기 위한 프로토콜을 개발해 왔지만, 이 시스템들이 진정으로 안전하다는 것을 증명하는 과정은 매우 취약했습니다. 증명은 종종 서로 다른 논문들로부터 엮어낸 수학적 논증의 사슬에 의존했는데, 각 논문은 저마다의 가정을 가지고 있었습니다. 만약 그 사슬의 한 고리가 다른 고리와 약간 어긋나거나 숨겨진 가정이 간과된다면, 보안 보장 전체가 아무도 모르게 무너질 수 있었습니다.

매사추세츠 공과대학교(MIT)의 연구진은 수학적 논리를 검증하도록 설계된 컴퓨터 프로그램을 사용하여 기초부터 보안 증명을 구축함으로써 이러한 취약성을 해결했습니다. 그들은 얽힌 입자 쌍을 사용하여 키를 생성하는, 널리 사용되는 특정 방식인 BB84 프로토og에 집중했습니다. 모든 논리 단계가 제대로 결합되어 있는지 확인하기 위해 인간의 신뢰에 의존하는 대신, 그들은 전체 보안 논증을 컴퓨터가 읽고 절대적인 정밀도로 검증할 수 있는 형식 언어로 번зу했습니다. 그 결과는 숨겨진 빈틈이나 어긋난 가정이 끼어들 틈을 주지 않는 기계 검증된 증명입니다. 이는 교환되는 입자의 수가 제한적인 경우에도 프로토콜이 안전하게 유지됨을 확인해 주는데, 이는 보안 추정치를 약화시키는 흔한 실제 세계의 제약 조건입니다. 나아가, 증명을 검증하는 데 사용된 것과 동일한 컴퓨터 시스템을 통해 새로운 더 타이트한 수학적 경계(bound)를 발견하였으며, 이를 통해 유한 크기 패널티(finite-size penalty)에 의한 키율 감소를 줄였습니다.

연구진은 국소 연산 및 고전 통신(local operations and classical communication)의 규칙을 엄격히 집행하는 디지털 언어를 컴퓨터 시스템 내에 만드는 것으로 시작했습니다. 양자 암호학의 맥락에서 이는 컴퓨터가 앨리스와 밥이 각자의 입자에 대해서만 행동을 수행할 수 있고, 공공 채널을 통해서만 정보를 공유할 수 있으며, 서로의 개인 데이터에 마법처럼 접근할 수 없음을 보장한다는 것을 의미합니다. 이 언어는 인간 검토자가 놓칠 수 있는 종류의 논리적 오류를 방지하는 가드레일 역할을 합니다. 예를 들어, 이러한 증명을 형식화하려는 이전의 시도에서 한 인공지능 에이전트는 양측 모두가 실제로 소유하지 않은 문자열을 결합하여 최종 키를 만드는 방법을 제안한 적이 있습니다. 컴퓨터의 엄격한 규칙은 이를 즉시 불가능한 것으로 표시하여 연구진이 접근 방식을 개선하도록 강제했습니다. 이 제약된 환경 내에서 단계별로 프로토콜을 구축함으로써, 연구진은 최종 보안 정리가 의도한 물리적 과정을 정확하게 설명하도록 보장했습니다.

프로토콜이 구축되자, 연구진은 컴퓨터에 도청자가 입자를 하나씩이 아니라 동시에 모두와 상호작용하는 강력한 유형의 공격인 결맞음 공격(coherent attack)에 대해 보안성을 검증하도록 요청했습니다. 컴퓨터는 입자의 초기 측정부터 오류 수정 및 개인정보 증폭의 최종 단계에 이르기까지 모든 논리적 단계를 점검했습니다. 컴퓨터는 프로토콜이 안전함을 확인했는데, 이는 시스템이 중단되지 않는다면 생성된 키가 무제한의 계산 능력을 가진 도청자에게조차 완벽하고 무작위적인 비밀 키와 구별 불가능함을 의미합니다. 결정적으로, 이 증명은 실제 시스템이 무한한 흐름이 아닌 유한한 수의 입자로 작동한다는 사실을 고려했습니다. 이러한 유한 크기 효과는 보통 과학자들이 안전을 보장하기 위해 더 많은 잠재적 키 재료를 버리도록 하여 지나치게 보수적이 되게 만듭니다. 그러나 새로운 증명은 얼마나 많은 키 재료를 안전하게 유지할 수 있는지에 대한 정밀한 계산을 제공하여, 이러한 유한한 한계로 인해 부과되는 패널티를 줄였습니다.

놀랍게도 연구진은 동일한 컴퓨터 파이프라인을 자신들의 작업을 검증할 뿐만 아니라 개선하는 데에도 사용했습니다. 시스템이 논리를 점검하는 동안, 연구진은 이러한 시스템의 보안을 추정하는 데 사용되는 조건부 엔트로피 분산에 대한 더 타이트한 경계를 식별하는 데 도움을 받았습니다. 기존 공식은 너무 느슨하여 비밀 키의 길이를 불필요하게 줄이고 있었습니다. 컴퓨터의 다양한 수학적 경계를 테스트하고 비교하는 능력에 따라, 연구진은 더 날카로운 부등식을 도출했습니다. 이 새로운 경계는 더 타이트하며, 보안을 희생하지 않으면서도 기존 공식이 허용했던 것보다 유한 크기 패널티를 줄여 키를 생성할 수 있게 해줍니다. 이 발견은 추측이 아니라 컴퓨터가 참이라고 검증한 엄격한 수학적 결과였으며, 이는 형식 증명 엔진이 단순히 작업 내용을 확인하는 것을 넘어, 오래된 문제에 대한 더 나은 해결책을 찾아냄으로써 과학적 발견을 능동적으로 가속화할 수 있음을 보여주었습니다.

이 연구는 또한 미래의 암호 시스템이 어떻게 검증되어야 하는지에 대한 템플릿 역할도 합니다. 연구진은 기초적인 정의와 정리 라이브러리를 오픈 소스로 공개함으로써 커뮤니티를 위한 재사용 가능한 도구 모음을 제공했습니다. 이 라이브러리에는 양자 상태, 채널에 대한 형식적 정의와 프로토콜을 기술하기 위한 특정 언어가 포함되어 있어, 다른 과학자들이 이 토대 위에 구축할 수 있도록 합니다. 이는 미래의 다른 양자 프로토콜이나 다른 양자 정보 과학 분야에 대한 증명들도 동일한 수준의 엄격함으로 구축될 수 있음을 의미합니다. 연구진은 인간의 통찰력과 기계 검증 논리의 끊임없는 정밀함을 결합함으로써, 오랫동안 이 분야를 괴롭혀온 숨겨진 불확실성을 제거할 수 있음을 보여주었습니다. 그 결과, 양자 키의 신뢰성이 단순히 연구자의 주장이 아니라 기계에 의해 검증된 사실이 되는 새로운 보안 논증의 표준이 탄생했습니다.