电子学报
電子學報
전자학보
ACTA ELECTRONICA SINICA
2014年
6期
1179-1185
,共7页
加密算法%安全性%形式逻辑%计算语义
加密算法%安全性%形式邏輯%計算語義
가밀산법%안전성%형식라집%계산어의
encryption algorithms%security properties%formal logics%computational semantics
提出了一个基于计算语义的安全协议验证逻辑,能准确描述安全协议中的各种计算行为和通信行为。设计了基于该逻辑的证明系统,能对密码学中常用加密算法的各类安全属性规范直接描述,具有密码学可靠性。发现了计算协议组合逻辑在加密算法安全性建模时存在的不可靠性,并提出了解决方法。通过对Needham-Schroeder-Lowe协议安全性的证明,验证了逻辑的证明能力。与大部分验证方法不同的是,本逻辑属于由密码学算法安全性到协议安全性的正向推理方法,兼具符号方法的易用性和计算方法的可靠性。
提齣瞭一箇基于計算語義的安全協議驗證邏輯,能準確描述安全協議中的各種計算行為和通信行為。設計瞭基于該邏輯的證明繫統,能對密碼學中常用加密算法的各類安全屬性規範直接描述,具有密碼學可靠性。髮現瞭計算協議組閤邏輯在加密算法安全性建模時存在的不可靠性,併提齣瞭解決方法。通過對Needham-Schroeder-Lowe協議安全性的證明,驗證瞭邏輯的證明能力。與大部分驗證方法不同的是,本邏輯屬于由密碼學算法安全性到協議安全性的正嚮推理方法,兼具符號方法的易用性和計算方法的可靠性。
제출료일개기우계산어의적안전협의험증라집,능준학묘술안전협의중적각충계산행위화통신행위。설계료기우해라집적증명계통,능대밀마학중상용가밀산법적각류안전속성규범직접묘술,구유밀마학가고성。발현료계산협의조합라집재가밀산법안전성건모시존재적불가고성,병제출료해결방법。통과대Needham-Schroeder-Lowe협의안전성적증명,험증료라집적증명능력。여대부분험증방법불동적시,본라집속우유밀마학산법안전성도협의안전성적정향추리방법,겸구부호방법적역용성화계산방법적가고성。
This paper proposes a logic for verifying security protocols in the computational model ,which can describe the computation and communication actions precisely .We present a cryptographically sound proof system on the logic and can formalize the various security properties for encryption algorithms directly .During the research ,several unsoundness of the formalization with the computational protocol compositional logic in prior work is discovered ,and corresponding solutions are proposed .By proving the security properties for the Needham-Schroeder-Lowe protocol ,the power of the logic is demonstrated .Being different from most of the current verification approaches ,this logic reasons about the security of protocols from the security of cryptographic algorithms forwardly ,and is both easy to use and cryptographically sound .