计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2013年
2期
325-331
,共7页
王勇%方娟%任兴田%林莉
王勇%方娟%任興田%林莉
왕용%방연%임흥전%림리
可信计算%远程证明%协议验证%形式化%进程代数
可信計算%遠程證明%協議驗證%形式化%進程代數
가신계산%원정증명%협의험증%형식화%진정대수
可信计算组织(Trusted Computing Group,TCG)的远程证明协议是最早提出的远程证明的解决方案,其协议的形式化验证对于工程实施具有重要意义.分析了TCG远程证明协议的两种形式——直接证明协议和借助可信第三方的证明协议,对它们进行了抽象处理,得到了两种协议形式的抽象模型.在抽象模型的基础上,给出了基于进程代数的形式化描述,并分别进行了形式化验证,验证结果表明两种协议形式的并行系统均展示了期望的外部行为.
可信計算組織(Trusted Computing Group,TCG)的遠程證明協議是最早提齣的遠程證明的解決方案,其協議的形式化驗證對于工程實施具有重要意義.分析瞭TCG遠程證明協議的兩種形式——直接證明協議和藉助可信第三方的證明協議,對它們進行瞭抽象處理,得到瞭兩種協議形式的抽象模型.在抽象模型的基礎上,給齣瞭基于進程代數的形式化描述,併分彆進行瞭形式化驗證,驗證結果錶明兩種協議形式的併行繫統均展示瞭期望的外部行為.
가신계산조직(Trusted Computing Group,TCG)적원정증명협의시최조제출적원정증명적해결방안,기협의적형식화험증대우공정실시구유중요의의.분석료TCG원정증명협의적량충형식——직접증명협의화차조가신제삼방적증명협의,대타문진행료추상처리,득도료량충협의형식적추상모형.재추상모형적기출상,급출료기우진정대수적형식화묘술,병분별진행료형식화험증,험증결과표명량충협의형식적병행계통균전시료기망적외부행위.
