암호 프로토콜

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

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

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

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

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

고급 암호 프로토콜

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

형식 검증

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

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

이 목록은 아직 미완성입니다. 여러분이 편집하여 채워 주세요.

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

이 목록은 아직 미완성입니다. 여러분이 편집하여 채워 주세요.

Automated Validation of Internet Security Protocols and Applications (AVISPA) 및 후속 프로젝트 AVANTSSAR.^[5]^[6]
- Constraint Logic-based Attack Searcher (CL-AtSe)^[7]
- Open-Source Fixed-Point Model-Checker (OFMC)^[8]
- SAT-based Model-Checker (SATMC)^[9]
Casper^[10]
크립토베리프
Cryptographic Protocol Shapes Analyzer (CPSA)^[11]
Knowledge In Security protocolS (KISS)^[12]
Maude-NRL Protocol Analyzer (Maude-NPA)^[13]
프로베리프
Scyther^[14]
타마린 증명기^[15]
Squirrel^[16]

추상 프로토콜의 개념

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

A\rightarrow B:\{X\}_{K_{A,B}}

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

예시

같이 보기

각주

↑ “Cryptographic Protocol Overview” (PDF). 2015년 10월 23일. 2017년 8월 29일에 원본 문서 (PDF)에서 보존된 문서. 2015년 10월 23일에 확인함.
↑ Chen, Shan; Jero, Samuel; Jagielski, Matthew; Boldyreva, Alexandra; Nita-Rotaru, Cristina (2021년 7월 1일). 《Secure Communication Channel Establishment: TLS 1.3 (over TCP Fast Open) versus QUIC》 (영어). 《Journal of Cryptology》 34. 26쪽. doi:10.1007/s00145-021-09389-w. ISSN 0933-2790. S2CID 235174220.
↑ Berry Schoenmakers. “Lecture Notes Cryptographic Protocols” (PDF).
↑ Fábrega, F. Javier Thayer, Jonathan C. Herzog, and Joshua D. Guttman., 《Strand Spaces: Why is a Security Protocol Correct?》 CS1 관리 - 여러 이름 (링크)
↑ “Automated Validation of Internet Security Protocols and Applications (AVISPA)”. 2016년 9월 22일에 원본 문서에서 보존된 문서. 2024년 2월 14일에 확인함.
↑ Armando, A.; Arsac, W; Avanesov, T.; Barletta, M.; Calvi, A.; Cappai, A.; Carbone, R.; Chevalier, Y.; +12 more (2012). Flanagan, C.; König, B. (편집). 《The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures》 7214. LNTCS. 267–282쪽. doi:10.1007/978-3-642-28756-5_19. 2024년 2월 14일에 확인함.
↑ “Constraint Logic-based Attack Searcher (Cl-AtSe)”. 2017년 2월 8일에 원본 문서에서 보존된 문서. 2016년 10월 17일에 확인함.
↑ Open-Source Fixed-Point Model-Checker (OFMC)
↑ “SAT-based Model-Checker for Security Protocols and Security-sensitive Application (SATMC)”. 2015년 10월 3일에 원본 문서에서 보존된 문서. 2016년 10월 17일에 확인함.
↑ Casper: A Compiler for the Analysis of Security Protocols
↑ cpsa: Symbolic cryptographic protocol analyzer
↑ “Knowledge In Security protocolS (KISS)”. 2016년 10월 10일에 원본 문서에서 보존된 문서. 2016년 10월 7일에 확인함.
↑ Maude-NRL Protocol Analyzer (Maude-NPA)
↑ Scyther
↑ Tamarin Prover
↑ Squirrel Prover

추가 자료

Ermoshina, Ksenia; Musiani, Francesca; Halpin, Harry (September 2016). 〈End-to-End Encrypted Messaging Protocols: An Overview〉 (PDF). Bagnoli, Franco 외 (편집). 《Internet Science》. INSCI 2016. Florence, Italy: Springer. 244–254쪽. doi:10.1007/978-3-319-45982-0_22. ISBN 978-3-319-45982-0.

[1] “Cryptographic Protocol Overview” (PDF). 2015년 10월 23일. 2017년 8월 29일에 원본 문서 (PDF)에서 보존된 문서. 2015년 10월 23일에 확인함.

[2] Chen, Shan; Jero, Samuel; Jagielski, Matthew; Boldyreva, Alexandra; Nita-Rotaru, Cristina (2021년 7월 1일). 《Secure Communication Channel Establishment: TLS 1.3 (over TCP Fast Open) versus QUIC》 (영어). 《Journal of Cryptology》 34. 26쪽. doi:10.1007/s00145-021-09389-w. ISSN 0933-2790. S2CID 235174220.

[3] Berry Schoenmakers. “Lecture Notes Cryptographic Protocols” (PDF).

[4] Fábrega, F. Javier Thayer, Jonathan C. Herzog, and Joshua D. Guttman., 《Strand Spaces: Why is a Security Protocol Correct?》 CS1 관리 - 여러 이름 (링크)

[5] “Automated Validation of Internet Security Protocols and Applications (AVISPA)”. 2016년 9월 22일에 원본 문서에서 보존된 문서. 2024년 2월 14일에 확인함.

[TAP_1-6] Armando, A.; Arsac, W; Avanesov, T.; Barletta, M.; Calvi, A.; Cappai, A.; Carbone, R.; Chevalier, Y.; +12 more (2012). Flanagan, C.; König, B. (편집). 《The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures》 7214. LNTCS. 267–282쪽. doi:10.1007/978-3-642-28756-5_19. 2024년 2월 14일에 확인함.

[7] “Constraint Logic-based Attack Searcher (Cl-AtSe)”. 2017년 2월 8일에 원본 문서에서 보존된 문서. 2016년 10월 17일에 확인함.

[8] Open-Source Fixed-Point Model-Checker (OFMC)

[9] “SAT-based Model-Checker for Security Protocols and Security-sensitive Application (SATMC)”. 2015년 10월 3일에 원본 문서에서 보존된 문서. 2016년 10월 17일에 확인함.

[10] Casper: A Compiler for the Analysis of Security Protocols

[11] sa: Symbolic cryptographic protocol analyzer

[12] “Knowledge In Security protocolS (KISS)”. 2016년 10월 10일에 원본 문서에서 보존된 문서. 2016년 10월 7일에 확인함.

[13] Maude-NRL Protocol Analyzer (Maude-NPA)

[14] Scyther

[15] Tamarin Prover

[16] Squirrel Prover

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

v t e 암호학
일반	암호화 기계 고전 암호 난수 발생기 단대단 암호화 디지털 서명 랜섬웨어 복호화 암호 해독 암호화폐 암호문 암호바이러스학 암호화 암호화 프로토콜 인증 프로토콜 카뎀리아 크립토재킹 클렙토그래피 키 (암호) 키젠 트랩도어 함수 평문 해시 함수 암호화 해시 함수 키 유도 함수 SHA
수학	공개 키 암호 방식 대칭 키 암호 메시지 인증 코드 블록 암호 스테가노그래피 스트림 암호 암호화 해시 함수 양자 키 분배 양자 후 암호 인증된 암호 방식