선택한 단어 수는 입니다.
최소 단어 이상 선택하여야 합니다.
최소 단어 이상 선택하여야 합니다.
선택한 단어 수는 30입니다.
최대 10 단어까지만 선택 가능합니다.
최대 10 단어까지만 선택 가능합니다.
문제 정의
- 정형검증의 대표적인 도구로는 HDM, Gypsy Verification Environment, PVS, SMV, Spin 등이 있다. 본 논문에서는 보안운영체제 검증에 적합한 정형기법 에 대하여 조사해보고자 한다. 운영체제는 매우 규모가 큰 소프트웨어 시스템이므로 한번에 검증하는 것보다는 작은 부분으로 나누어 모듈별로 검증하는 것이 합리적이다.
- 본 연구에서는 정형검증 기법과 여러 도구들에 비교했 다. 정형기법은 명세기법과 검증기법오로 분류되고, 검증 기법은 다시 정리증명과 모델체킹오로 분류된匚卜.
가설 설정
- NRL 프로토콜 분석기는 P「이og로 작성되어 있고, 암 호 프로토콜, 인증 프로토콜, 키 분배 프로토콜 등을 위한 특수목적 검증 시스템이다. NPA 는 Dolev 와 Yao[16]2| term-rewriting 모델을 기초로 하고 있는데, 이 모델에서 공격자는 모든 메시지 트래픽을 읽을 수 았 고, 메시지를 변경하고 훼손시킬 수 있을 뿐만 아니라, 합법적인 사용자가 할 수 있는 모든 연산들을 수행할 수 있다고 가정하고 있다. 단, 암호 키나 암호문 등의 특정 한 단어를 알지는 못한다고 가정한다.
- NPA 는 Dolev 와 Yao[16]2| term-rewriting 모델을 기초로 하고 있는데, 이 모델에서 공격자는 모든 메시지 트래픽을 읽을 수 았 고, 메시지를 변경하고 훼손시킬 수 있을 뿐만 아니라, 합법적인 사용자가 할 수 있는 모든 연산들을 수행할 수 있다고 가정하고 있다. 단, 암호 키나 암호문 등의 특정 한 단어를 알지는 못한다고 가정한다. 공격자의 목표는 특정단어를 알아내는 것이다[1, 71.
※ AI-Helper는 부적절한 답변을 할 수 있습니다.