Cryptol을 이용한 국내 표준 블록 암호 모듈의 자동 정형 검증

Vol. 28, No. 1, pp. 53-60, 2월. 2018
10.13089/JKIISC.2018.28.1.53, Full Text:
Keywords: formal, Verification, cryptography, cryptol, saw
Abstract

암호 알고리즘은 세계적으로 표준화가 진행되고 있으며, 암호 알고리즘의 안전성은 충분히 입증되어 왔다. 하지만, 기존 검증 방법으로는 구현상의 취약점이 존재하여 심각한 피해를 야기할 수 있기 때문에 표준에 따라 올바르게구현되었는지에 대한 개선된 검증 방법이 필요하다. 그러므로 본 논문에서는 국가정보원에서 수행하는 128비트 이상 블록 암호 모듈 중에서 검증 대상인 ARIA와 LEA를 선정하였고, 고신뢰 암호 모듈을 위해 Cryptol을 이용하여 올바르게 구현되었는지 검증하는 방법을 제시하고자 한다.

Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from December 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
W. Choi and S. Kim, "Automated Formal Verification of Korean Standard Block Cipher Using Cryptol," Journal of The Korea Institute of Information Security and Cryptology, vol. 28, no. 1, pp. 53-60, 2018. DOI: 10.13089/JKIISC.2018.28.1.53.

[ACM Style]
Won-bin Choi and Seung-joo Kim. 2018. Automated Formal Verification of Korean Standard Block Cipher Using Cryptol. Journal of The Korea Institute of Information Security and Cryptology, 28, 1, (2018), 53-60. DOI: 10.13089/JKIISC.2018.28.1.53.