论文研究-基于Petri网的混合安全策略建模与验证.pdf

所需积分/C币:5 2019-07-22 21:44:45 435KB .PDF
收藏 收藏
举报

提出了一种基于有色Petri网的建模方法,在系统的Petri网模型中可以对中国墙策略进行分析和验证。给出了基于有色Petri网的混合安全策略的形式化定义;并通过一个系统实例阐述了如何利用该方法对系统的混合安全性进行分析和验证。无论是在系统的设计阶段还是实现阶段,该方法都能够有效地提升系统的混合安全性。
第2期 张昭想,等:基于Pemi网的混合安全策略建模与验证 ·511 2 读取任意颜色的托肯。一旦李四读取了一个客体,一个具有与 李四的控制库所 该客体相同颜色的托肯将被创建到他的搾制库所p中。因此 准备报告 按照第2章中所定义的那些公理,P所有可能的情况为:, 草稿 {a,e}或{s,b 合成张 通过形式化分析,可以确定各个托肯的颜色,并且可以发 现潜在的利益冲突。 修改意见 张三的控制库所 ○最终稿 对于这个简单的实例,各个托肯的颜色是比较容易确定 图3实例进程的网 的。但是对于复杂的系统或进程来说,则会非常困难。对于在 第一个变迁(主体)t,张三根据他从ifob2中读取的信这些复杂情况下的自动分析,覆盖图将会是一个有力的工具。 息创建了一份投资报告的草稿p。然后经理李四(2)审阋了3.3覆盖图 这份投资报告的草稿并提出了修改意见p。最后,张三(3)根 对应于图3中CPN模型的覆盖图显示在图5中。各个托 据草稿p和修改意见p完成了投资报告的最终稿。并且,肯都进行了颜色标注 。是张二的控制库所,而p是李四的控制库所。 Inol1由李四所提供咨询的公司资料组成;inod2由张 三所提供咨询的公司资料组成。图4显示了 innodb和inl2 中的内容,以及CO类。每个CO类中只有两个元素,是为了 减少问题的复杂性。李四所使用的ib包括汇丰银行(颜 色“b”)和沃尔沃公司(颜色“e”)的资料。张三所使用的in fod2包括花旗银行(颜色“a”)和福特公司(颜色“s”)的资料。 )( 恨行COI类 汽车公司COI类 图夏盖图 〔花银行了[干你行特[次尔次 图5中,这个覆盖图由19个节点构成,表示了CN模型 的叮能标志。由于篇幅的限制,图5并不是一个完整的覆盖 图。节点的条目表示由数据库所p3、P1和p5中的对应托肯 图4CO类和数据库 颜色构成的标志。节点中括号内的条目表示了控制库所和 3.2形式化分析 P的标志。例如,节点11表示,一个颜色为a的托肯在p3中; 现在,中国墙策略将作为这个系统的基本安全策略。 一个颜色为e的托肯在p中;一个颜色为a的托肯在p中;两 李四为汇丰银行和沃尔沃公司(分别具有颜色“b”和“e”)提个托肯在p中,颜色分别为a和e。箭头表示变迁的发生。例 供咨询,对于他来说没有利益冲突,因为这两个公司属于不同的如变迁t2的发生将标志2改变到标志4(也将标志2改变到 COI类。同样,张三也没有利益冲突(图4)。形式化的分析如下:标志5,…,1)。由于篇幅限制,并不是所有的箭头都有标 银行CO类={a,b 注。有两种类型的箭头,即实线的和虚线的。实线箭头表示 汽车公司COI类={s,已 有效的”标志改变,即,变迁的发生不违反第2章中定义的那 infodb1={b,b,…,e,e, 些公理;相反,虚线箭头表示对公理的违反,例如: nfodb2 a)从节点2指向节点4的箭头违反了公理2,因为李四读 乃3:张三(t1)能够写入p。根据公理6,如果张三曾经从 取了颜色为a和b的托肯,而这两种颜色在同一个COI类中。 innodb2屮读取过一个颜色为a的托肯(客体),那么一个颜色 为a的客体将被创建在p3中;如果张三曾经从 infor2中读取 b)从节点2指向节点7的箭头违反了公理6,囚为创建 过一个颜色为s的托肯(客体),那么一个颜色为s的客体将被个颜色为b的托肯需要李四的控制库所中有一个颜色为b的 托肯。 创建在p3中。因此,在P3中被创建的托肯只能具有颜色a或s。 P1:李四(t2)能够从 infodb1中读取颜色为b或e的托肯; c)从节点2指向节点10的箭头既违反了公理2也违反了 他出能够从/中读取颜色为a或s的托肯。因此,根据公理公理6 对图5的分析可以发现,从起始标志(节点1)到可能的结 6,在p中被创建的托肯可以具有颜色n、b、5或e。但是,如果 李四已经从 infodbl中读取过颜色为b(或e)的托肯,按照公理 束标志(节点12~19)可以找到一条有效路径。这条路径是 2,他将不能从p2中读取颜色为a(或s)的托肯 1-2—5-13这条路径要求各托肯的颜色为:p3={a P2:张三(t2)可以从P3中读取颜色为a或s的托肯,也可 P={a,P3={a},B={a,a,a},p={a,e}当然,还可以找 以从p中读取颜色为a、b、s或e的托肯。因此,根据公理6, 到其他有效路径。 在p3中被创建的托肯可以具有颜色a、b、s或e 结束语 P:最初p6是空的,按照公理3、4,张三可以从 innodb2中 读取任意颜色的托肯。一旦张三读取了一个客体,一个具有与 本文提出了一种利用有色rei劂为中国墙策略建模和验 该客体相同濒色的托肯将被创建到他的控制库所p中。因此证的方法。通过引人控制库所的概念,给出了基于有色Pri 按照第2章中所定义的那些公理,所有可能的情况为:,网的中国墙策略的形式化定义;然后利用一个实例阐述了如何 a},}s},a,a,a},{a,a,e},s,s,s}或5,5,b} 通过基于CPN的形式化定义和覆盖图分析来验证中国墙策略 内:最初p是空的,按照公理34,李四可以从mul中的系统行为。 (下转第515页) 第2期 薛素静,等:基于单向哈希函教的远程口令认证方案 515 表1总结了 Wu- Chieu认证方案 Lee- Lin-Chan认证方案相互认证。 和本文所提认证方案的安全性质。 综上所述,本文所提认证方案相比于W-Cheu认证方案 种方案的安全性比较 和 Lee-Lin-(hang认证方案具有更高的计算效率 安全属性 Wu-Chicu Lcc-Lin-Chang 本文所提 认证方案 认证方案 认证方案 结束语 被动攻击 安仝 安仝 主动击 安全 不安全 安全 本文首先分析了 Wu-Chieu改进后的远程认证方案仍然易 猜測攵击 不安全 安全 安全 遭受一种离线口令猜测攻击。攻击者能够猜测出合法用户的 窃取智能卡攻击 不安全 全 双向认证 实现 口令,并能通过使用窃取合法用户的智能卡来假冒该合法用 会话坐钥分发 完美前向保密性 无无无 实现 户。同时,本文还分析了Iein-Chag认证方案易遭受伪造 攻击的安全缺陷,攻十者能够假冒另一个合法用户以获得对远 程系统资源的访问权。在此基础上,本文提出一种基于单向哈 4性能分析 希函数和 Diffie-Hellman密钥交换协议的远程口令认证方案 表2比较了 Wu-Chieu认证方案、 Lee- Lin-Chan认证方案参考文献: 和本文所提认证方案的计算效率。从表中可以看出, Wu-Chieu[1] PEYRET P, LISIMAQUE G, CHUA Y. Smart cards provide very 认证方案需要执行总共三次模幂运算、六次哈希运算和两次按 high security and flexibility in subscribers m anagement[ J.IEEE 位异或运算。Ie- Lin-Chang认证方案需要执行总共八次哈希 Trans on Consumer Electronics, 1990, 36(3): 744-752 运算和四次按位异或运算。本文所提认证方案只需执行总共2] LAMPORT L. Password authenlicalio: with insecure cunmlunicaLiol 四次模幂运算、六次哈希运算和两次按位异或运算。其中四次 IJ. Communications of the ACM, 1981, 24(11): 770-772 模幂运算是为了实现相互认证和完美前向保密性这两种安全[3] HWANG M S,LLH. A new remote user authentication scheme 性质。 using smart cards[ J]. IEEE Trans on Consumer Electronics 表2三种方案的计算成本比较 2000.46(1):28-30 Wu-Chieu 本文所提 [4 SUN H M. An eflicient remule user authentication scheine using smart 计算类型认证方案 认证方案 认证方案 cards J.IEEE Trans on Consumer Electronics, 2000, 46(4) 用户远程系统用户远程系统用户远程系统 958-961 模幂运算1 0 哈希运算2 [5 WUST, CHIEU B C. A user friendly remote authentication scheme XOR运算1 2 2 with smart cards[ J]. Computers Security, 2003, 22(6):547- 需要 需要 不需要 550 在 Wu-Chieu认让方案中,用户需要执行两次哈希运算和61 YANG Chou-chen,WAN, Ren-chiun. Cryptanalysis of a user friend 一次按位异或运算,远程系统需要执行四次哈希运算和一次按 ly remote authentication scheme with smart cards[ J]. Computers 位异或运算。在 Lee-Lin-(hang认证方案中,用户需要执行三 Security,2004,23(5):425-42 [7 WI ST, CHIEU B C. A note an a user friendly remote authenticatio 次哈希运算和二次按位异或运算,远程系统需要执行五次哈希 schene with snart cards[J. IEICE Trans on Fund, 2004. E87-A 运算和二次按位异或运算。在本文所提认证方案中,用户只需 (8):2180-2181 要执行一次哈希运算和一次按位异或运算,远程系统只需要执81LECC,LNCH, CHANG C O. An improyed low compu 行四次哈希运算和一次按位异或运算。从哈希运算和按位异 cost user authentication scheme for mobile communic ation[C//Proc 或运算的角色出发,可以看出本文所提方案与Wu- Chieu认证 of the 19th Advanced Information Networking and Applications ( IFFE 方案有着相同的计算效率。然而本文所提认证方案能够实现 AINA’05).2005:249-252 (上接第511页)对于复杂的大型实际系统来说,CPN模型会有 ference. New Orleans, Louisiana: IEEE Computer Society, 2000 非常多的节点,使得无法手工完成分析工作。因此,开发自动 159-167 分析和验证安全策略的工具是笔者今后的究方向。另外,利51 KNORR K. Multilevel security and inform ation flow in Petri net work 用Pe网处理无干扰策略和策略复合也是今后的研究內容。 nows[ C]//Prou uf the 9th Internalional Conference un Telecommuni cation Systems, Modeling and Analysis. Dallas, Texas: IEEE Cam 参考文献 puter Society, 2001: 9-20 [ IJ BREWERD, NASH M. The Chinese wall security policy[ C]//Proc [61 JIANG Yi-xin, LIN Chuang. YIN Hao, et al. Securily analys of the 1989 IEEE SyInpusiul on Securily anld Privacy. Oak land, Cali- mandatory access control model[ C]//Proe of IEEE International Con fornia: IEEE Computer Society Press, 1989: 206-214 ference on Systems, Man and Cybernetics. Hague, Netherlands [2 BELL D, LAPADULA L. The bell-lapadula model[ J.Jour IEEE Computer Society, 2004: 5013-5018 Computer Security, 1996, 4(2, 3): 239-263 [7 PETRI C A. Kom munikation mit automaten[ D]. Bonn: Institutfur In [3] AHMED T, TRIPATHI A R. Static verification of security require strumentelle Mathematik der Universit at Bonn 1962 ments in role based CSC W systems[ C]//Proc of ACM Symposium on [81 MURATA T. Petri nets: praperties, analysis and applications[ J1 Aceess Control Models and Technologies. New York: ACM Press Proceedings of the IEEE, 1989, 77(4): 541-580 2003:196-203 9 JENSEN K. An introduction to the theoretical aspects of coloured Pe 14 KNORR K. Dynamic access control through Petri net workflows tri nets: a decade of concurrency C |//Lecture Notes in Computer [C]//Proe of the 16th Annual Computer Security Applications Con Science.1994:230-272

...展开详情
试读 4P 论文研究-基于Petri网的混合安全策略建模与验证.pdf
立即下载 低至0.43元/次 身份认证VIP会员低至7折
抢沙发
一个资源只可评论一次,评论内容不能少于5个字
上传资源赚积分,得勋章
最新推荐
论文研究-基于Petri网的混合安全策略建模与验证.pdf 5积分/C币 立即下载
1/4
论文研究-基于Petri网的混合安全策略建模与验证.pdf第1页

试读结束, 可继续读1页

5积分/C币 立即下载 >