滁州学院学报
滁州學院學報
저주학원학보
JOURNAL OF CHUZHOU UNIVERSITY
2012年
2期
21-23,49
,共4页
迹语义%Petri网%信息流安全模型%非演绎模型
跡語義%Petri網%信息流安全模型%非縯繹模型
적어의%Petri망%신식류안전모형%비연역모형
Trace Semantics%Petri net%Information Flow Security Model%Non-- deducibility Model
就刻画安全的本质而言,基于非演绎信息流安全模型较之与基于访问控制的安全模型更为确切。文章在基于迹语义对非演绎信息流安全模型进行分析的基础上,给出了基于扩展Petri网的非演绎模型的形式化描述,进一步基于Petri网的形式化描述给出非演绎模型的验证算法且开发相应的验证工具,最后通过实例说明该算法的正确性和验证工具的方便适用性。
就刻畫安全的本質而言,基于非縯繹信息流安全模型較之與基于訪問控製的安全模型更為確切。文章在基于跡語義對非縯繹信息流安全模型進行分析的基礎上,給齣瞭基于擴展Petri網的非縯繹模型的形式化描述,進一步基于Petri網的形式化描述給齣非縯繹模型的驗證算法且開髮相應的驗證工具,最後通過實例說明該算法的正確性和驗證工具的方便適用性。
취각화안전적본질이언,기우비연역신식류안전모형교지여기우방문공제적안전모형경위학절。문장재기우적어의대비연역신식류안전모형진행분석적기출상,급출료기우확전Petri망적비연역모형적형식화묘술,진일보기우Petri망적형식화묘술급출비연역모형적험증산법차개발상응적험증공구,최후통과실례설명해산법적정학성화험증공구적방편괄용성。
In characterizing security, non--deducibility security model captures more essence than access control security models. This paper describes and formally defines non--dedueibility model based on trace semantics and Petri net. Furthermore, this paper provides the verification algorithm for non--de- ducibility security model based on Petri net and offers the verification tools with several examr~les.
