Needham-Schroeder 프로토콜과 공격

Needham-Schroeder 프로토콜(1978)은 신뢰할 수 있는 제3자(TTP)를 사용하여 암호화 인증 프로토콜을 설계하려고 한 최초의 형식적 시도 중 하나였습니다. 목표는 두 당사자인 Alice와 Bob이 각 주체와 장기 키를 공유하는 신뢰할 수 있는 인증 서버(AS)를 사용하여 서로를 인증하고 공유 세션 키를 설정할 수 있게 하는 것이었습니다. 이 프로토콜은 공개 키 기반 구조보다 먼저 등장했지만, 최신성 확인을 위한 논스와 신뢰할 수 있는 서버를 통한 키 분배라는 개념을 도입했으며, 이러한 개념은 Kerberos와 같은 현대 프로토콜에서도 여전히 중심적인 역할을 합니다. NS와 그 실패를 이해하는 과정은 프로토콜 분석 분야 전체를 형성하는 데 영향을 주었습니다.

NS 대칭 키 프로토콜은 다섯 단계로 진행됩니다. (1) Alice는 Bob과 통신할 세션 키를 요청하기 위해 {A, B, Na}를 AS로 보냅니다. (2) AS는 {Na, B, Kab, {Kab, A}_Kb}_Ka를 Alice에게 응답으로 보냅니다. 여기에는 세션 키 Kab, Bob을 위한 티켓, 그리고 Alice의 장기 키 Ka로 모두 암호화된 정보가 포함됩니다. (3) Alice는 티켓 {Kab, A}_Kb를 Bob에게 전달합니다. (4) Bob은 티켓을 복호화하여 Kab를 추출하고, 도전 값인 {Nb}_Kab를 Alice에게 보냅니다. (5) Alice는 {Nb-1}_Kab로 응답하여 Kab를 보유하고 있음을 증명합니다. 논스 Nb는 4단계의 재생을 방지합니다. 이 프로토콜에는 Denning과 Sacco(1981)가 악용한 알려진 재생 공격이 존재합니다.

Denning과 Sacco(1981)는 다음과 같은 결함을 발견했습니다. 2단계의 AS 응답은 새로 생성된 것이 아니며, 서버가 제공하는 타임스탬프나 논스를 포함하지 않습니다. 과거 세션을 손상시켜 이전 세션 키 Kab를 가로챈 공격자 Mallory는 오래된 티켓 {Kab, A}_Kb를 이후 언제든지 Bob에게 재생할 수 있습니다. Bob은 Alice가 보낸 합법적인 티켓으로 보이는 것을 받아 손상된 키 Kab를 세션에 사용합니다. Denning과 Sacco의 해결책은 AS 응답과 티켓에 타임스탬프를 추가하는 것이었습니다. 이 방식은 Kerberos에 도입되어 티켓의 유효 기간을 제한하기 위해 타임스탬프가 티켓에 포함됩니다.

NS 공개 키 프로토콜(또한 1978년에 제안됨)은 공개 키 암호화를 사용하여 두 당사자를 상호 인증하도록 설계되었습니다. (1) Alice는 {Na, A}_PKb를 Bob에게 보냅니다. 이는 Bob의 공개 키로 암호화한 논스 Na입니다. (2) Bob은 {Na, Nb}_PKa로 응답합니다. 두 논스를 모두 Alice의 공개 키로 암호화한 값입니다. (3) Alice는 Bob의 논스를 그의 공개 키로 암호화한 {Nb}_PKb를 응답으로 보냅니다. 이 교환이 끝나면 두 당사자는 두 논스(Na, Nb)를 모두 보유하게 되고 세션 키를 파생할 수 있습니다. 이 프로토콜은 17년 동안 안전한 것으로 보였지만, Lowe가 1995년에 공격을 발견했습니다.

Gavin Lowe(1995)는 FDR 모델 검사기를 사용하여 중대한 결함을 발견했습니다. Mallory는 정직한 Bob에게 메시지를 전달하면서 Alice에게 Bob인 것처럼 가장할 수 있습니다. 1단계에서 Alice는 Bob과 통신한다고 생각하고 {Na, A}_PKm을 Mallory에게 보냅니다. Mallory는 이를 {Na, A}_PKb로 Bob에게 전달합니다. 2단계에서 Bob은 {Na, Nb}_PKa로 응답하고, Mallory는 이를 복호화한 다음 Alice를 위해 다시 암호화하여 {Na, Nb}_PKa로 보냅니다. Alice는 이를 복호화하여 Nb를 추출합니다. 3단계에서 Alice는 이것이 Bob에게 전달된다고 생각하고 {Nb}_PKm을 보냅니다. Mallory는 이를 복호화한 다음 {Nb}_PKb로 Bob에게 전달합니다. Bob은 Alice와의 상호 인증을 완료했다고 믿지만, 실제로 Alice가 인증하고 있는 상대는 Mallory입니다. 해결책은 2단계에서 Bob이 자신의 신원을 포함하여 {Na, Nb, B}_PKa로 보내도록 하는 것입니다.

Lowe가 NSPK 프로토콜에 제시한 수정은 단순하지만 매우 중요합니다. 2단계에서 Bob의 응답에는 Bob의 신원 B가 포함되어야 하므로, {Na, Nb, B}_PKa가 됩니다. 이제 Alice가 응답을 받으면, 포함된 신원 B가 자신이 연락하려던 상대와 일치하는지 확인합니다. Mallory는 자신의 응답으로 바꿔치기할 수 없습니다. Alice의 확인을 통과하는 유효한 {Na, Nb, M}_PKa를 만들려면 Mallory에게 Alice의 개인 키가 필요하기 때문입니다. 이 교훈은 Needham-Abadi 원칙으로 일반화됩니다. 인증 메시지는 식별을 위해 문맥에만 의존하지 말고 발신자의 신원을 명시적으로 결합해야 합니다.

Lowe가 NSPK 결함을 발견하는 데에는 FDR (실패-발산 정제) 모델 검사기의 도움이 컸습니다. FDR은 공격자의 개입을 포함한 모든 가능한 프로토콜 실행을 빠짐없이 탐색합니다. 이로 인해 형식 프로토콜 분석 도구가 개발되었습니다. Proverif(응용 파이 계산에 기반)는 무한 세션에서 인증 및 기밀성 속성을 증명하거나 반증할 수 있습니다. Tamarin 증명기는 다중집합 재작성을 사용하며 TLS 1.3 및 Signal과 같은 복잡한 프로토콜을 지원합니다. AVISPA와 Scyther도 다른 도구입니다. 현대의 프로토콜 설계(TLS 1.3, Signal, Noise)는 배포 전에 형식 검증을 거칩니다. 이는 NS/Lowe 사건이 남긴 직접적인 유산입니다.

NS 공격은 인증 목표 사이의 차이를 명확히 했습니다. 개체 인증: 어떤 주체가 현재 살아 있으며 프로토콜에 참여하고 있음을 증명하는 것(신선성이 중요합니다). 데이터 출처 인증: 특정 메시지가 특정 주체에 의해 생성되었음을 증명하는 것(주체의 활성 상태를 의미하지 않을 수 있습니다). Lowe의 공격은 개체 인증을 손상시킵니다. Alice는 Bob과 인증하고 있다고 믿지만, 실제로는 Bob에게 중계하고 있는 Mallory와 인증하고 있습니다. 현대의 프로토콜 명세는 목표를 정확하게 기술합니다. "Alice는 이 세션의 시작자로서 Bob에게 인증됩니다." 모호한 목표는 비공식 검토는 통과하지만 형식 분석에서는 실패하는 불명확한 명세로 이어집니다.

NS와 관련된 또 다른 공격 유형은 반사 공격입니다. Mallory가 Alice의 메시지를 Alice에게 되돌려 재생하는 방식입니다. 프로토콜이 대칭적이라면(두 당사자가 동일한 키와 메시지 형식을 사용하는 경우), Alice는 자신의 도전 메시지를 Bob이 보낸 유효한 응답으로 받아들일 수 있습니다. 방어 방법은 키 방향을 다르게 사용하거나(각 방향에 대해 암호화 키와 복호화 키를 별도로 사용) 메시지에 역할 표시자를 포함하는 것입니다(암호화 주체가 메시지에 "I am initiator"를 포함합니다). TLS와 같은 현대 프로토콜은 반사를 방지하기 위해 HKDF에서 파생한 키에 역할별 레이블 문자열을 포함합니다(클라이언트에는 "c e traffic", 서버에는 "s hs traffic" 사용).

인터리빙 공격은 동시에 진행되는 여러 프로토콜 세션의 메시지를 결합해 인증을 위조합니다. Alice가 두 세션을 동시에 실행하면 Mallory는 두 세션의 메시지를 섞어 일관되지만 유효하지 않은 결합 세션을 만들고, Mallory가 인증되도록 할 수 있습니다. 방어 방법은 세션 바인딩입니다. 각 메시지를 세션 문맥에 암호학적으로 결합해야 합니다(예: 세션 ID를 포함하거나 세션마다 고유한 키를 사용합니다). TLS는 현재 세션의 전체 트랜스크립트에 대한 MAC인 완료 메시지를 통해 인터리빙을 방지합니다. 인터리빙된 메시지는 트랜스크립트를 변경하므로 완료 값이 무효화됩니다.

Needham-Schroeder 프로토콜은 Kerberos의 설계(재생을 방지하기 위한 타임스탬프는 Denning-Sacco의 수정에서 차용), TLS(완료 메시지의 트랜스크립트 MAC으로 인터리빙과 반사를 방지), Signal 프로토콜(래칫 상태를 통한 세션 바인딩), Noise 프로토콜 프레임워크(핸드셰이크 패턴에서의 신원 바인딩)에 직접적인 영향을 주었습니다. NS 공격은 비공식적인 보안 논증만으로는 충분하지 않다는 사실을 확립했습니다. 모든 프로토콜은 네트워크를 제어하고 메시지를 재생, 재정렬, 수정할 수 있는 능동적 공격자를 상정하여 분석해야 합니다. 이 공격자 모델(Dolev-Yao)은 이제 형식 프로토콜 검증에서 표준으로 사용됩니다.

Lowe가 NS 공개 키 프로토콜의 취약점을 수정하기 위해 제안한 간단한 변경은 무엇입니까?

Needham-Schroeder 대칭 프로토콜(1978)은 TTP 기반 세션 키 배포를 도입했습니다. Denning-Sacco 공격(1981)은 재생 취약점을 발견했고, 이는 Kerberos에서 타임스탬프를 사용하여 해결되었습니다. NSPK 공개 키 프로토콜은 Lowe가 모델 검사를 통해 발견한 MITM 공격(1995)에 취약했으며, 메시지에 발신자 신원을 포함하여 해결되었습니다. 이러한 공격은 형식 검증(Proverif, Tamarin)이 프로토콜 설계에 필수적임을 확립했습니다. 핵심 교훈은 다음과 같습니다. 메시지는 발신자 신원을 결합해야 하고, 세션은 서로 격리되어야 하며, 반사 공격은 방향별 키 파생으로 방지하고, 인터리빙 공격은 트랜스크립트 MAC으로 방지해야 합니다.