당신이 새로운 금고가 절대 깨지지 않는다는 것을 증명하려는 숙련된 자물쇠 기술자라고 상상해 보십시오. 당신은 단순히 "이것은 강력합니다!"라고 말하지 않을 것입니다. 대신 다음과 같은 일련의 단계를 보여주어야 합니다. "만약 당신이 이 작은 자물쇠를 부술 수 없다면, 당신은 문을 부술 수 없습니다. 만약 당신이 문을 부술 수 없다면, 당신은 금고를 부술 수 없습니다." 이것이 현대 암호학이 작동하는 방식입니다. 전문가들은 보안을 테스트하기 위해 '게임'을 사용하는데, 여기서 해커는 비밀을 추측하려고 노력하며, 시스템의 보안은 이를 알려진, 불가능한 퍼즐을 푸는 것만큼 어렵다는 것을 보여줌으로써 증명됩니다. 하지만 여기 함정이 있습니다. 이러한 증명을 수작업으로 하는 것은 마치 허리케인 속에서 카드 집을 균형 잡으려 노력하는 것과 같습니다. 아주 작은 실수를 하거나, 미세한 틈을 놓치거나, 복잡함 속에서 길을 잃기 쉽습니다. 그리고 만약 단 한 단계라도 놓친다면, 전체 증명이 무너집니다. 이것이 바로 과학자들이 컴퓨터가 모든 카드를 하나하나 확인하여 카드 집이 굳건히 서 있도록 만드는 방법을 찾아온 이유입니다.

여기에 논문이 등장합니다. 저자들은 강력한 컴퓨터 프로그램인 Lean 4 내부의 디지털 작업장인 HOPSCOTCH(도약하는 게임을 의미하는 유쾌한 이름)를 구축했습니다. HOPSCOTEC을 단순한 수학을 체크하는 것을 넘어, 보안 증명의 이야기를 이해하는 매우 똑똑한 로봇 교정가라고 생각하십시오. HOPSCOTCH는 암호학자들이 기이하고 제한된 언어로 증명을 쓰도록 강요하는 대신, 그들이 다른 모든 수학에서 사용하는 것과 동일한 도구를 사용하여 증명을 작성할 수 있게 해줍니다. 이는 '게임 호핑(game hopping)' 과정—즉, 하나의 보안 시나리오에서 다음 시나리오로 건너뛰는 과정—을 컴퓨터가 검사, 검증 및 자동화할 수 있는 명확한 단계별 객체로 변환합니다. 저자들은 단순히 도구를 만든 것이 아니라, 이를 사용하여 GGM이라는 복잡한 구조를 포함한 여러 유명한 암호화 방식의 보안을 성공적으로 증명함으로써, 이 "로봇 교정가"가 혼란 없이 실제 세계의 암호학적 과제를 처리할 수 있음을 보여주었습니다.

큰 그림: 왜 우리는 교정 로봇이 필요한가

디지털 보안의 세계에서 우리는 "증명 가능한 보안"에 의존합니다. 이는 우리가 단순히 코드가 안전하기를 바라는 것이 아니라, 그것을 증명하려고 노력한다는 것을 의미합니다. 이를 수행하는 표준적인 방법은 "게임 기반" 접근 방식입니다. 보안 요원(시스템)과 도둑(공격자)을 상상해 보십시오. 보안 요원은 비밀을 가지고 있고, 도둑은 그것을 맞추려고 노력합니다.

1. 실제 게임 (The Real Game): 도둑이 실제 시스템을 깨뜨리려고 시도합니다.
2. 도약 (The Hop): 우리는 실제와 거의 비슷하지만 분석하기 더 쉬운 약간 다른 게임을 상상합니다. 만약 도둑이 실제 게임에서 이길 수 있다면, 그들은 이 새로운, 약간 다른 게임에서도 이길 수 있다는 것을 증명합니다.
3. 연쇄 (The Chain): 우리는 규칙을 매번 아주 조금씩 바꾸면서 한 게임에서 다른 게임으로 계속 도약하며, 결국 누군가 연속으로 백만 번 동전 던지기를 맞히는 것처럼 명백히 이기기 불가능한 최종 게임에 도달합니다.

만약 우리가 모든 "도약"이 안전하다는 것을 증명할 수 있다면, 전체 사슬은 안전한 것입니다. 이것을 "게임 호핑 증명"이라고 부릅니다.

문제는 인간이 이를 완벽하게 수행하는 데 서투르다는 점입니다. 이러한 증명은 길고, 지저분하며, 세부 사항이 가득합니다. 단 하나의 놓친 세부 사항이 전체 증명을 틀리게 만들 수 있으며, 시스템을 불안전하게 만들 수 있습니다. 수년 동안 연구자들은 이러한 증명을 확인하기 위한 특별한 컴퓨터 도구들을 구축하려고 노력해 왔지만, 이러한 도구들은 종종 수학자들과는 다른 언어를 사용합니다. 그들은 마치 "보안"은 알지만 "수학"은 모르는 번역가와 같아서, 전문가들이 자신의 아이디어를 앞뒤로 번환하게 만들어 느리고 오류가 발생하기 쉽게 만듭니다.

HOPSCOTCH의 등장: 만능 번역기

이 논문의 저자인 Stefan Dziembowski, Grzegorza Fabiańskiego, Daniele Micciancio, 그리고 Rafał Stefański는 다리를 놓기로 결정했습니다. 그들은 수학적 증명을 검증하는 데 사용되는 인기 있는 컴퓨터 프로그램인 Lean 4 내부의 프레임워크인 HOPSCOTCH를 만들었습니다.

HOPSCOTCH의 마법은 다음과 같습니다:

• 새로운 언어가 없음: 다른 도구들처럼 제한된 방식으로 코드를 작성하도록 강요하는 대신, HOPSCOTCH는 당신이 표준 Lean을 사용하여 증명을 작성할 수 있게 해줍니다. 이는 마치 요리사에게 플라스틱 칼을 사용하는 대신 자신이 좋아하는 칼로 요리하게 하는 것과 같습니다.
• 객체로서의 증명: HOPSCOTCH에서 증명은 단순한 텍스트 더미가 아닙니다. 그것은 레고 모델과 같은 구조화된 객체입니다. 게임의 각 "도약"은 특정한 레고 브릭입니다. 당신은 그것들을 서로 끼워 맞출 수 있으며, 컴퓨터는 그것들이 완벽하게 맞는지 확인합니다. 만약 당신이 서로 맞지 않는 두 브릭을 연결하려고 하면, 컴퓨터는 "아니오, 작동하지 않습니다"라고 말합니다.
• "추상화" 기법: 이러한 증명에서 가장 어려운 부분 중 하나는 서로 다르게 보이는 두 시스템이 정확히 동일하게 동작함을 보여주는 것입니다. HOPSCOTCH는 "상태 추상화(state abstraction)"라는 영리한 기법을 사용합니다. 두 대의 로봇이 있다고 상상해 보십시오. 하나는 내부 배선도가 복잡하고, 다른 하나는 깔끔합니다. HOPSCOTCH는 복잡한 배선이 깔끔한 배선과 어떻게 대응되는지를 보여주는 지도(추상화 함수)를 그릴 수 있게 해줍니다. 만약 그 지도가 정확하다면, 컴퓨터는 두 로봇의 외관이 다르더라도 행동은 동일하다는 것을 알게 됩니다.

그들이 실제로 수행하고 발견한 것

저자들은 단순히 도구를 만든 것이 아니라, 이를 시험대에 올렸습니다. 그들은 네 가지 주요 암호학적 개념의 보안을 공식적으로 검증하기 위해 HOPSCOTCH를 사용했습니다:

1. Encrypt-then-MAC: 메시지를 비밀스럽게 유지하면서 동시에 조작 불가능하게 만드는 방법입니다. 그들은 기초가 되는 암호화와 "태깅"(MAC)이 안전하다면, 전체 시스템이 가장 똑똑한 해커로부터도 안전하다는 것을 증명했습니다.
2. ElGamal 암호화: 공개 키를 사용하여 비밀 메시지를 보내는 유명한 방식입니다. 그들은 결정적 디피-헬먼(Decisional Diffie-Hellman, DDH) 가정이라는 어려운 수학 문제를 바탕으로 그 보안을 증명하는 방법을 보여주었습니다.
3. One-Time Secrecy에서 IND-CPA로: 시스템이 단일 메시지에 대해 안전하다면, 이를 여러 메시지에 대해서도 안전하게 만들 수 있음을 증명했습니다. 이는 견고한 암호화를 구축하는 데 중요한 단계입니다.
4. GGM 구조: 이것이 핵심입니다. GGM 방식은 단순한 난수 생성기를 복잡한 "의사 난수 함수"(진짜처럼 보이는 가짜 난수 생성기)로 변환합니다. 이전의 컴퓨터 증명들은 매우 얕은 버전(예: 3단계 트리)만을 다룰 수 있었습니다. 저자들은 HOPSCOTCH를 사용하여 **비정적 깊이(non-constant depth)**에 대한 GGM의 보안을 증명했습니다. 즉, 어떤 크기의 트리에도 작동한다는 것을 의미합니다. 그들이 아는 바로는, 이것이 범용 컴퓨터 증명 보조 도구가 이 특정하고 복잡한 구조를 성공적으로 검증한 첫 번째 사례입니다.

어떻게 수행했는가 (게임 메커니즘)

논문은 HOPSCOTCH가 증명을 특정 단계, 즉 "생성자(constructors)"로 분해하여 작동한다고 설명합니다:

• 관찰적 동등성 (Observational Equivalence): 두 게임이 외부 관찰자에게 어떻게 똑같이 보이는지 증명합니다.
• 축약 (Reductions): 게임 A를 깰 수 있다면 게임 B도 깰 수 있음을 보여줍니다.
• 하이브리드 시퀀스 (Hybrid Sequences): 많은 작은 단계들을 사슬처럼 연결합니다.

이 프레임워크에는 이러한 단계들을 대신 해결해 주는 "택틱스(tactics, 자동화된 도우미)"가 포함되어 있습니다. 예를 들어, 두 오라클(게임 시스템)이 동일함을 증명해야 할 때, 컴퓨터는 자동으로 "상태 추상화" 지도를 찾으려고 시도할 수 있습니다. 만약 찾지 못한다면, 컴퓨터는 해당 단계를 인간이 해결하도록 남겨두되, 인간이 어디에 있는지 알 수 있도록 구조를 유지합니다.

저자들은 또한 "계산적 건전성 정리(computational soundness theorem)"를 증명했습니다. 이것은 "컴퓨터가 이 증명이 유효하다고 말한다면, 그것은 실제로 현실 세계에서도 유효하다"는 것을 의미하는 멋진 표현입니다. 그들은 HOPS-COTCH가 생성하는 모든 증명 객체에 대해, 증명에 사용된 가정들을 바탕으로 해커가 가질 수 있는 "이점(advantage)"을 수학적으로 정확하게 계산할 수 있음을 보여주었습니다. 이는 컴퓨터가 단순히 자기 자신과 게임을 하고 있는 것이 아니라, 실제적이고 구체적인 보안 보장을 제공하고 있음을 보장합니다.

결론

이 논문은 HOPSCOTCH가 특화된 보안 도구의 편의성과 범용 수학 보조 도구의 강력함 사이의 간극을 성공적으로 메웠다고 결론짓습니다. 이를 통해 암호학자들은 읽기 쉽고, 검사하기 쉬우며, 인간의 실수에 덜 취약한 증명을 작성할 수 있습니다. 저자들은 컴퓨터가 아직 "해커"가 충분히 빠르게 실행되는지(polynomial time이라는 기술적 세부 사항)까지는 체크하지 못한다고 인정하지만, 완전히 자동화되고 신뢰할 수 있는 보안 증명을 위한 토대를 마련했습니다.

그들은 또한 미래를 암시합니다: 이러한 구조화된 증명 객체를 사용하면, 곧 AI를 사용하여 이러한 증명을 자동으로 작성하도록 돕거나, "나쁜 사건(bad events)"과 확률을 포함하는 더욱 복잡한 시나리오로 시스템을 확장하는 것이 가능해질 수 있습니다. 하지만 현재로서는 주요 성과가 명확합니다. 그들은 컴퓨터가 우리의 디지털 비밀이 안전하다는 것을 증명하도록 돕는 신뢰할 수 있고 유연하며 강력한 방법을 구축했다는 점입니다.