초록 ▼

연구개요
보안 프로토콜의 모듈화된 자동검증 과제는 부분검증 결과를 병합할 때 성질이 유지되는 조합성을 보이는 파이계산법에 대한 열린쌍방시뮬레이션을 기반으로
(1) 실제적인 보안 프로토콜을 모형화할 수 있도록 기반 이론을 더욱 일반화하여
(2) 검증 엔진의 핵심이 되는 등가성 알고리듬을 일반화된 이론에 맞게 확장하고
(3) 그를 기반으로 검증도구를 개발하고 접근성이 높은 웹기반 인터페이스 형태로 공개하는 연구이다.

연구 목표대비 연구결과
정량적 연구 성과 목표 달성
- 3편의 국제학회 학술

연구개요
보안 프로토콜의 모듈화된 자동검증 과제는 부분검증 결과를 병합할 때 성질이 유지되는 조합성을 보이는 파이계산법에 대한 열린쌍방시뮬레이션을 기반으로
(1) 실제적인 보안 프로토콜을 모형화할 수 있도록 기반 이론을 더욱 일반화하여
(2) 검증 엔진의 핵심이 되는 등가성 알고리듬을 일반화된 이론에 맞게 확장하고
(3) 그를 기반으로 검증도구를 개발하고 접근성이 높은 웹기반 인터페이스 형태로 공개하는 연구이다.

연구 목표대비 연구결과
정량적 연구 성과 목표 달성
- 3편의 국제학회 학술지: 66% 성과 달성
- CS분야 우수국제학술대회 논문(LICS 2018) 1편 게제 완료
- Logical Methocs in Computer Scinece 저널(SCI) 1편 게재 확정
(최종본 작업중 첨부자료 참고)
- 3편의 국내 논문 100% 성과 달성
- KCI우수등재지논문 1편, KCI등재지 논문2편
- 국내학회 학술분과 행사에 3회 이상 참여 100% 달성
- 2019.08 SIGPL Summer School 2019 평창 휘닉스파크
- 2019.02 SIGPL Winter School 2019 경성대학교
- 2018.08 SIGPL Summer School 2018 동국대학교
- 국제학술대회 및 국제교류는 최근 코로나 등으로 물리적 진행이 어려웠음
정성적 연구 성과 목표 달성
- 계획: 기초이론 개선/검증, 응용분야 적용, 웹기반 도구 개발
- 성과: 기초이론 개선/검증, 병렬 알고리즘으로 성능 개선, 웹기반 일부 구현

연구발성과의 활용 계획 및 기대효과 (연구개발결과의 중요성)
예상 효과는 다음과 같다.
(1) 부분검증 결과를 병합할 때 성질이 유지되는 조합성을 보장되기 때문에
(ㄴ) 모듈 변경 시 전체 시스템 검증 반복이 불필요하므로 검증시간도 단축
(ㄱ) 이미 인해 검증된 보안 모듈을 새로운 시스템에 재사용하기 용이
(2) 기존의 실행경로추적 알고리듬으로 자동검증이 어려운 보안 요구사항 자동검증 가능
(3) 웹기반 인터페이스를 제공하여 자동 보안 프로토콜 검증이 필요한 분야에서 첨단 보안 검증기술에 대한 접근성 향상

(출처 : 요약문 2p)

목차 Contents

• 표지 ... 1
• 연구결과 요약문 ... 2
• 목차 ... 3
• 1. 연구개발과제의 개요 ... 4
• 2. 연구개발과제의 수행 과정 및 수행 내용 ... 5
• 3. 연구개발과제의 수행 결과 및 목표 달성 수준 ... 6
• 1) 정성적 연구개발성과(연구개발결과) ... 6
• 3) 목표 달성 수준 ... 7
• 4) 목표 미달 시 원인 분석(해당 시) ... 9
• 4. 연구개발성과의 관련 분야에 대한 기여 정도(연구개발결과의 중요성) ... 9
• 5. 연구개발성과의 관리 및 활용 계획 ... 10
• 6. 참고문헌 ... 11
• 붙임1. 세부 정량적 연구개발성과 ... 13
• 붙임2. 연구책임자 대표적 연구실적 및 증빙(요약문 및 사본) ... 17
• 끝페이지 ... 19