버로우스-아바디-네덤 논리

Burrows–Abadi–Needham logic

버로우스-아바디-네덤 논리(BAN 로직이라고도 함)는 정보 교환 프로토콜을 정의하고 분석하기 위한 일련의 규칙이다.구체적으로, BAN 논리는 사용자들이 교환된 정보가 신뢰할 수 있는지, 도청으로부터 안전한지, 아니면 둘 다를 결정하는 데 도움을 준다.BAN의 논리는 모든 정보 교환이 변조 및 공개 모니터링에 취약한 미디어에서 일어난다는 가정으로부터 시작된다.이것은 "네트워크를 신뢰하지 말라"라는 인기 있는 보안 망토로 진화했다.

일반적인 BAN 논리 시퀀스에는 다음 세 단계가 포함된다.[1]

  1. 메시지 원본 확인
  2. 메시지 신선도 확인
  3. 출처의 신뢰도 검증.

BAN 로직은 인증 프로토콜을 분석하기 위해 (모든 자명 시스템과 마찬가지로) 가정과 정의를 사용한다.BAN 로직의 사용은 프로토콜의 보안 프로토콜 표기법 제정에 수반되는 경우가 많으며 때때로 서류에 제시되기도 한다.

언어유형

BAN 논리와 같은 계열의 로직은 결정가능하다: BAN 가설과 추정된 결론을 취하는 알고리즘이 존재하며, 그 결론이 가설에서 도출될 수 있는지 여부를 답하는 알고리즘이 존재한다.제안된 알고리즘은 다양한 종류의 마술 세트를 사용한다.[2]

대안 및 비판

BAN 로직은 GNY 로직과 같은 다른 많은 유사한 형식주의자들에게 영감을 주었다.이들 중 일부는 BAN 논리의 한 가지 약점을 보완하려고 노력한다: 지식과 가능한 보편적 측면에서 분명한 의미를 지닌 좋은 의미론의 결여.그러나 1990년대 중반부터 모델 체커를 이용한 운용 모델(완벽한 암호화를 가정)에서 암호 프로토콜이 분석되었고, BAN 로직과 관련 형식성으로 '검증'된 프로토콜에서는 수많은 버그가 발견되었다.[citation needed]어떤 경우에는 프로토콜이 BAN 분석에 의해 안전한 것으로 간주되었지만 실제로는 안전하지 않다.[3]이 때문에 BAN-family 로직은 표준침해성 추론에 근거한 증명방법에 찬성하는 로직들을 포기하게 되었다.[citation needed]

기본 규칙

정의와 그 함의는 다음과 같다(P와 Q는 네트워크 에이전트, X는 메시지, K는 암호화 키).

  • P는 X:P가 X가 사실인 것처럼 행동하고, 다른 메시지에서 X를 주장할 수도 있다고 믿는다.
  • P는 X에 대한 관할권을 가지고 있다: X에 대한 P의 신념은 신뢰되어야 한다.
  • P는 X: 한때는 P가 더 이상 X를 믿지 않을 수도 있지만 (믿고) 메시지 X를 전송했다.
  • P는 X:P가 메시지 X를 수신하며 X를 읽고 반복할 수 있다.
  • {X:K X는 키 K로 암호화된다.
  • fresh(X): X는 이전에 어떤 메시지도 보내지 않았다.
  • 키(K, P£Q): P와 Q는 공유 키 K와 통신할 수 있다.

이러한 정의의 의미는 일련의 가정들에서 포착된다.

  • 만약 P가 키(K, PrpgQ)를 믿고 P가 {X}K을(를) 본다면 P는 (Q가 X를) 믿는다.
  • 만약 P가 (X가) 믿고 (Q가 X라고 말했고) P가 (X가) 신선하다고 믿는다면, P는 (Q가 X를 믿는다)고 믿는 것이다.

P는 여기서 X가 신선하다고 믿어야 한다.만약 X가 신선한 것으로 알려져 있지 않다면, 그것은 공격자에 의해 재생된 구식 메시지일 수 있다.

  • P가 (Q가 X를 관할한다)고 믿고 P가 (Q가 X를 믿는다)고 믿는다면 P는 X를 믿는다.
  • 메시지 구성과 관련된 몇 가지 다른 기술적 견본이 있다.예를 들어, P가 Q가 X와 Y의 결합인 <X, Y>라고 말했다고 믿는다면, P도 X라고 했고, P도 Q가 Y라고 말한 것으로 본다.

이 표기법을 사용하여, 인증 프로토콜 뒤의 가정은 공식화될 수 있다.견본을 사용하면 특정 에이전트가 특정 키를 사용하여 통신할 수 있다고 믿는다는 것을 증명할 수 있다.증명이 실패하면 실패 지점은 대개 프로토콜을 위태롭게 하는 공격을 암시한다.

BAN ROI(입구개구리) 프로토콜 논리 분석

매우 간단한 프로토콜인 와이드 마우스 프로그 프로토콜은 A와 B라는 두 에이전트가 신뢰할 수 있는 인증 서버인 S와 동기화된 클럭을 사방에 사용하여 보안 통신을 설정할 수 있도록 한다.표준 표기법을 사용하여 프로토콜은 다음과 같이 지정할 수 있다.

에이전트 A와 B는 각각 키 K와as K를bs 탑재해 S와 안전하게 통신한다.그래서 우리는 다음과 같은 가정을 가지고 있다.

A가 믿는 열쇠(Kas, A파스)
S는 키를 믿는다(Kas, A파스)
B는 키를 믿는다(Kbs, B파스)
S는 키를 믿는다(Kbs, B파스)

에이전트 A는 B와 보안 대화를 시작하기를 원한다.따라서 그것은 B와ab 통신하기 위해 사용할 K라는 키를 발생시킨다.A씨는 이 열쇠가 스스로 키를 구성했기 때문에 안전하다고 생각한다.

A가 믿는 열쇠(Kab, A파운트B)

이 키가 A:에서 온 것이 확실하다면 B는 기꺼이 수락할 것이다.

B는 (A가 키를 관할한다(K, A파운드의 B)

더욱이 B는 S가 A의 키를 정확하게 중계할 것을 신뢰한다.

B는 (A가 (A가 (K, A £B)를) 관할한다)고 믿는다.

즉, B가 S가 A가 B와 통신하기 위해 특정 키를 사용하기를 원한다고 믿는다면, B는 S를 신뢰하고 또한 그것을 믿을 것이다.

을 갖는 것이 목표다.

B는 키를 믿는다(Kab, A파운트B)

A는 시계를 읽고 현재 시간 t를 얻어 다음과 같은 메시지를 보낸다.

1 A→S: {t, 키(Kab, A £B)}Kas

즉, 선택한 세션 키와 현재 시간을 개인 인증 서버 키 K로as 암호화된 S로 전송한다.

S는 키(Kas, A £)를, S는 {t, key(Kab, A £B)Kas를 본다고 믿기 때문에, S는 실제로 A가 {t, key(Kab, A £B)라고 말했다고 결론짓는다.(특히 S는 이 메시지가 일부 공격자에 의해 완전히 천으로 제조된 것은 아니라고 본다)

시계가 동기화되어 있기 때문에, 우리는 추측할 수 있다.

S는 신선하다고 믿는다.

S는 신선하다고 믿고 S는 A가 {t, 키(K, A파운드의ab B)라고 말한 것으로 믿고 있기 때문에, S는 A가 실제로 그 키ab(K, A파운드의 B)를 믿고 있다고 믿고 있다.(특히 S는 이 메시지가 과거 어느 시기에 포획한 일부 공격자에 의해 재생되지 않았다고 보고 있다.)

그런 다음 S가 키를 B:

2 S→B: {t, A, A believe key(Kab, A £B)}Kbs

메시지 2는 K로bs 암호화되어 있고, B는 K(Kbs, B)를 믿고 있기 때문에, B는 이제 S가 {t, A, A(Aab)를 믿는다고 말한 것으로 믿고 있다.시계가 동기화되어 있기 때문에 B는 신선하고, 매우 신선하다고 믿는다(A는 키를 믿는다(Kab, A £B).B는 S의 진술이 신선하다고 믿기 때문에, B는 S가 (A가 키(Kab, A £B)를 믿는다고 믿는다.B는 S가 A의 신념에 대해 권위적이라고 믿기 때문에, B는 (A가 키(Kab, A £B)를 믿는다.B는 A와 B 사이의 세션키에 대해 A가 권위적이라고 생각하기 때문에, B는 키(Kab, A £B)를 믿는다.이제 B는 비밀 세션 키로 K를ab 이용하여 A에게 직접 연락할 수 있다.

이제 시계가 동기화되어 있다는 가정을 버렸다고 가정해 봅시다.그럴 경우 S는 A로부터 메시지 1을 {t, 키ab(K, A파운트B)}로 받지만 더 이상 t가 신선하다고 단정할 수 없다.과거에 A가 이 메시지를 보낸 것은 알고 있지만(K로as 암호화되어 있기 때문에) 이것이 최근의 메시지라는 것은 아니기 때문에 S는 반드시 A가 키 K를ab 계속 사용하고 싶어한다고 생각하지 않는다.이는 프로토콜에 대한 공격을 직접 가리킨다.메시지를 캡처할 수 있는 공격자는 이전 세션 키 중ab K를 추측할 수 있다(이 작업은 시간이 오래 걸릴 수 있음).그런 다음 공격자는 이전의 {t, 키(Kab, A £B) 메시지를 재생하여 S로 전송한다.만약 시계가 동기화되지 않는다면(아마도 같은 공격의 일부로서), S는 이 오래된 메시지를 믿고 B에게 손상된 오래된 키를 다시 사용할 것을 요청할 수 있다.

원본 인증 논리 문서(아래 링크)에는 이 예와 Kerberos 핸드셰이크 프로토콜의 분석, 그리고 Andrew Project RPC 핸드셰이크의 두 가지 버전(이 중 하나가 결함)을 포함한 많은 예가 수록되어 있다.

참조

  1. ^ "Course material on BAN logic" (PDF). UT Austin CS.
  2. ^ Monniaux, David (1999). "Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief". Proceedings of the 12th Computer Security Foundations Workshop.
  3. ^ Boyd, Colin; Mao, Wenbo (1994). "On a Limitation of BAN Logic". EUROCRYPT '93 Workshop on the Theory and Application of Cryptographic Techniques on Advances in Cryptology. Retrieved 2016-10-12.

추가 읽기