암호 프로토콜

암호 프로토콜(cryptographic protocol)은 보안 관련 기능을 수행하고 암호학적 방법을 적용하는 추상적이거나 구체적인 프로토콜이며, 종종 암호 프리미티브의 시퀀스로 이루어진다. 프로토콜은 알고리즘이 어떻게 사용되어야 하는지 설명하고 데이터 구조 및 표현에 대한 세부 정보를 포함하여 여러 상호 운용 가능한 프로그램 버전을 구현하는 데 사용될 수 있다.

암호 프로토콜은 보안 응용 프로그램 수준 데이터 전송에 널리 사용된다. 암호 프로토콜은 일반적으로 다음 측면 중 적어도 일부를 포함한다.

 키 합의 또는 설정
 인증 프로토콜을 사용하여 개체 인증
 대칭 암호화 및 메시지 인증 키 자료 구성
 보안 응용 프로그램 수준 데이터 전송
 부인봉쇄 방법
 비밀 공유 방법
 다자간 보안 컴퓨팅

예를 들어, 전송 계층 보안(TLS)은 웹(HTTPS) 연결을 보호하는 데 사용되는 암호 프로토콜이다. X.509 시스템을 기반으로 하는 개체 인증 메커니즘, 공개 키 암호화를 사용하여 대칭 키 암호 키가 형성되는 키 설정 단계, 그리고 응용 프로그램 수준 데이터 전송 기능을 가지고 있다. 이 세 가지 측면은 중요한 상호 연결을 가진다. 표준 TLS는 부인봉쇄를 지원하지 않는다.

다른 유형의 암호 프로토콜도 있으며, 용어 자체도 다양한 의미를 가진다. 암호 응용 프로그램 프로토콜은 종종 하나 이상의 기본 키 합의 방법을 사용하며, 이들 역시 때때로 "암호 프로토콜"이라고 불린다. 예를 들어, TLS는 디피-헬먼 키 교환으로 알려진 것을 사용하는데, 이는 TLS 자체의 일부일 뿐이지만, 디피-헬먼은 다른 응용 프로그램에서는 그 자체로 완전한 암호 프로토콜로 간주될 수 있다.

 고급 암호 프로토콜 
다양한 암호 프로토콜은 데이터 기밀성, 무결성, 인증이라는 전통적인 목표를 넘어 컴퓨터 매개 협업의 다양한 다른 원하는 특성을 보호한다. 은닉 서명은 디지털 현금 및 디지털 자격 증명에 사용되어 개인의 신원이나 거래 당사자의 신원을 노출하지 않고 개인이 속성이나 권리를 가지고 있음을 증명할 수 있다. 보안 디지털 타임스탬프는 데이터(비밀이라 할지라도)가 특정 시간에 존재했음을 증명하는 데 사용될 수 있다. 다자간 보안 컴퓨팅은 비밀 데이터(예: 비공개 입찰)를 기반으로 답변(예: 경매에서 최고 입찰 결정)을 계산하는 데 사용될 수 있으므로 프로토콜이 완료되면 참가자는 자신의 입력과 답변만 알게 된다. 종단 간 감사 가능 투표 시스템은 전자 투표를 수행하기 위한 바람직한 개인 정보 보호 및 감사 가능성 속성 세트를 제공한다. 부인 불가능 서명은 서명자가 위조를 증명하고 서명을 확인할 수 있는 사람을 제한하는 대화형 프로토콜을 포함한다. 부인 가능한 암호화는 공격자가 일반 텍스트 메시지의 존재를 수학적으로 증명하는 것을 불가능하게 함으로써 표준 암호화를 강화한다. 디지털 믹스는 추적하기 어려운 통신을 생성한다.

 형식 검증 
암호 프로토콜은 추상적인 수준에서 때때로 형식 검증될 수 있다. 그렇게 할 때, 위협을 식별하기 위해 프로토콜이 작동하는 환경을 공식화할 필요가 있다. 이는 종종 돌레프-야오 모델을 통해 이루어진다.

보안 프로토콜의 형식 추론에 사용되는 논리, 개념 및 계산법:

 버로우스-아바디-니덤 논리 (BAN 논리)
 돌레프-야오 모델
 π-계산법
 프로토콜 구성 논리 (PCL)
 Strand space

보안 프로토콜의 형식 검증에 사용되는 연구 프로젝트 및 도구:

 Automated Validation of Internet Security Protocols and Applications (AVISPA) 및 후속 프로젝트 AVANTSSAR.
 Constraint Logic-based Attack Searcher (CL-AtSe)
 Open-Source Fixed-Point Model-Checker (OFMC)Open-Source Fixed-Point Model-Checker (OFMC)
 SAT-based Model-Checker (SATMC)
 CasperCasper: A Compiler for the Analysis of Security Protocols
 크립토베리프
 Cryptographic Protocol Shapes Analyzer (CPSA)cpsa: Symbolic cryptographic protocol analyzer
 Knowledge In Security protocolS (KISS)
 Maude-NRL Protocol Analyzer (Maude-NPA)Maude-NRL Protocol Analyzer (Maude-NPA)
 프로베리프
 ScytherScyther
 타마린 증명기Tamarin Prover
 SquirrelSquirrel Prover

 추상 프로토콜의 개념 

프로토콜을 형식적으로 검증하기 위해 종종 앨리스와 밥 표기법을 사용하여 추상화하고 모델링한다. 간단한 예시는 다음과 같다.

이는 앨리스 가 공유 키 로 암호화된 메시지 로 구성된 메시지를 밥 에게 보내려 함을 나타낸다.

 예시 
 인터넷 키 교환
 IPsec
 커버로스
 오프더레코드 메시징
 점대점 프로토콜
 시큐어 셸 (SSH)
 시그널 프로토콜
 전송 계층 보안
 ZRTP

 같이 보기 

 암호 시스템 목록
 보안 채널
 보안 프로토콜 오픈 저장소
 암호화 라이브러리 비교
 양자 암호 프로토콜

 각주 

 추가 자료