基于RBAC的网络安全策略模型的着色Petri网工具及其应用分析

理论计算机科学电子笔记121（2005）117-142www.elsevier.com/locate/entcs基于RBAC策略R. 拉布尔德湾Naserr，F.Graset，F. Bar r`ere，A. Benzekri1IRIT -SIERAUniversit'ePaulSabatierToulouse，France摘要安全策略模型允许对安全目标的实现进行推理。当实现安全机制时，很难针对安全目标正式验证安全属性，特别是在网络环境中。为了评估实现的安全特性，应该考虑有关网络拓扑、转发以及过滤和转换引擎的细节。在本文中，我们提出了一个着色Petri网为基础的工具，它可以图形化地描述一个给定的网络拓扑结构，网络安全机制和所需的安全目标。该工具计算不同的功能来设置安全属性，并使用生成的可达性图分析的死状态正式验证解决方案。可以研究不同的安全属性，如机密性和可用性。保留字：网络安全，安全管理，有色Petri网。1介绍网络配置的设计、运行和维护是安全管理任务的重要组成部分。 基本上，分布式应用程序的安全性由一组通过安全机制实现的网络安全服务来支持。管理员应确定要使用的安全服务和要应用的安全机制配置一旦部署，网络安全1 电子邮件：{laborde，nasser，grasset，barrere，benzekri}@ irit.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.011118R. Alberde等人理论计算机科学电子笔记121（2005）117随着时间的推移，策略经常变得难以管理，因为添加了更多的规则，并且在检索、管理和删除旧的不必要的规则方面存在真正的困难。这一事实导致在网络设备中管理主动安全策略的痛苦不断增加。传统的SNMP代理管理平台过于简单，无法解决复杂的问题.出于这个原因，最近出现了不同的体系结构和技术，它们增加了管理代理在这种情况下，我们发现了基于策略的管理方法，该方法考虑了抽象的安全策略[4，12，18，20，33，34]，这些策略可以在不同的级别[25，30]上表示，从业务目标到设备特定的配置参数。将一个明确的目标转化为相应的配置的过程称为推导过程[2，24，31]。从类似的角度来看，基于多代理系统范式的方法[14]希望管理代理更加自主，以便能够合作创建满足定义目标的策略。这里使用的术语策略目标是在前一种方法中的策略抽象层之后使用的。最后，作为第三种方法，最新出现的作品[36，37，38，39]通过使用前缀“自我”作为主旨的“自适应自主计算”概念来继续这个想法然而，通过上述方法寻求的自动化还不足以进行安全管理。目前还没有一种自动的网络安全策略评估方法。访问控制模型[5，9，29]为安全目标的定义提供了解决方案。事实上，它们是一种正式的技术，用来定义什么是允许的，什么是不允许的。此外，还有几种与每个模型相关的技术[7，9，28，32]，以保证安全策略是正确的。然而，这些模型没有考虑相关的安全机制或策略。网络安全管理本质上是一种分布式功能，由具有不同能力的各种设备（PC、路由器、安全网关、防火墙等）协调提供。因此，相同的目标可以通过不同的组合物从而不同的策略来实现。例如，加密可以通过过滤机制或加密机制来实现因此，有必要开发一种自动化的错误评估技术，以确定正确的安全网络策略是什么在安全上下文中使用了各种形式验证技术：定理证明器（EHDM [22]，PVS [27]）和模型检查/查找技术（SMV [6]，NPA [21]，Alloy [13]）。所有形式化的规范语言，如Z，LOTOS或Petri网[16，19]也被使用。可惜R. Alberde等人理论计算机科学电子笔记121（2005）117119没有提出与这些技术一起使用的与网络安全相关联的模型。因此，我们提出了一个新的形式化验证工具，这是特定于网络安全策略。它包括应用安全策略模型、网络安全策略/机制模型和网络拓扑模型。本文的结构如下。在第2节中，我们从我们的角度解释了网络安全的含义。在第3节中，我们定义了我们的形式化规范语言和形式化求值方法。在第4节中，我们介绍了我们的工具，它实现了前面的概念，并自动化的评估任务。此外，我们还展示了一个使用的小例子。 最后，在第6节中，我们展示了我们的结论和我们对未来工作的计划2网络安全策略在访问控制模型[5，29]中，我们选择了NIST RBAC模型[9]，因为它简化了管理任务。实际上，角色概念允许聚合用户的权限，然后它方便了管理员对用户权限的修改此外，角色之间的层次结构代表了根据不同观点对组织建模的良好工具。2.1NIST RBAC模型NIST小组提出了RBAC模型的标准化[9]。它由两个子模型组成：核心模型和层次模型（图1）。核心模型包括五组基本数据元素：• A 人或智能代理。• A “role” is a job function within the context of an organization with someassociated semantic regarding the authority and responsibility on the userassigned 我们可以注意到，这个定义非常模糊。• “许可”是对一个或多个• An “operation” is an executable image of a program, which upon• An最后，将一组角色分配给用户，并将一组权限分配给角色。会话是一个用户到一组授权角色的映射层次模型为支持角色层次结构添加了关系存在不同的方法来构建角色层次结构：基于特权120R. Alberde等人理论计算机科学电子笔记121（2005）117用户用户分配作用权限分配操作对象用户会话角色_会话许可届会议−D角色层次Fig. 1. NIST RBAC模型[26]或基于用户2.2应用程序安全策略和网络安全策略之间的关系是什么当用户访问服务时，在用户启动服务的设备和支持服务执行的设备之间交换一组数据流（图2）。因此，可以感知网络安全策略和应用安全策略例如，如果应用程序安全策略声明用户u1可以读取对象o1- noted（u1，o1，+read），则这意味着设备之间的相应数据流（O1，+read）用户U1的设备和O1的设备可以存在于网络上。因此，相关联的网络安全策略必须允许数据流在这两个设备之间流动（o1，+read）-记为（device（u1）Participatedevice（o1），+flow（o1，read））。相反，如果应用程序安全策略声明用户u2不能读取对象o2（标注为（u2，o2，-read）），则在u2和o2的设备之间不应存在并行流（o2，read）。因此，网络安全策略必须禁止u2和o2的设备之间的流（o2，读），即，（device（u2）Participatedevice（o2），flow（o2，read））。 我们从应用程序中报告此信息，网络级别，以阻止这些数据流，从而防止拒绝服务或基于漏洞利用/有效载荷的攻击。定义2.1标为“d”的推导关系定义为：u∈USERS，（u，o，±a）（device（u）Participate（o），f low（o，±a））. （一）2.3关于在RBAC系统中，用户是根据他们的角色来考虑的因此，派生关系如下：r∈ROLES，R. Alberde等人理论计算机科学电子笔记121（2005）117121访问控制规则应用程序安全策略数据流网络安全策略计算机服务器图二.安全策略推导运算符，<$u，uJ∈USERS，u uJ·（r，（opj，oi））n赋（u，r）n分配的（uJ，r）分配的（u j，r）分配的d（设备（u）参与设备（oi），+流（oi，opj））分配的（u j，r）分配的d（设备（u）参与设备（oi），+流（o i，op j））分配的（u j，r）分配的d（设备（u）参与设备（o i），+流（o i，op j））分配的d（设备（u）参与设备（o j），+流（o i，op j））分配的d（设备（u）参与设备（uJ）device（o i），−flow（o i，op j））。此后，我们认为没有层次结构，并且角色具有不相交的权限（如果不是这种情况，我们可以创建此集合的分区）：这样的约束将帮助我们根据分配给一个角色的权限对数据流进行分组，然后通过角色识别它们。然后，我们通过角色的名称来记录与分配给角色的权限相对应的一组队列。根据这些定义，我们提出了我们的方法，包括一个网络体系结构规范语言和一个安全机制验证对RBAC安全策略过程。3网络体系结构模型及安全机制分析在网络环境中，所有适用于数据流的处理都可以分为四类功能：• 消费/生产数据流的机制，如终端系统，• 传播数据流的机制，如通信的支持，• 将数据流转换为另一种数据流的机制，如安全协议，• 过滤数据流的机制，如防火墙。因此，我们的过程包括对这些功能和这些功能之间的交互进行建模。因此，我们定义了一种具有形式语义的图形语言，以支持网络安全策略验证过程。推导122R. Alberde等人理论计算机科学电子笔记121（2005）117用户A用户B数据访问控制规则网络基础设施C：结束流功能：渠道功能：过滤器功能：活动实体：变换功能：被动实体图三. 网络拓扑在我们的模型（图3）中，我们发现了一组主动实体和一组被动实体，以及一组作用于信息流的功能（结束流，通道，转换和过滤器）。主动实体对应于RBAC模型中的用户，被动实体是RBAC模型中的对象集合。我们使用有色Petri网（CPNs）描述我们的语言的语义。CPNs [15，17]为分布式和并发系统的构建和分析提供了一个框架。系统的CPN模型描述了系统可能处于的状态以及这些状态之间的转换3.1着色Petri网CPN的状态通过位置（绘制）表示如椭圆或圆形）。每个位置都有一个相关联的类型（颜色集），确定该位置可能包含的数据类型。CPN的状态称为标记。它由位于（分布）各个地方的许多令牌组成。每个令牌都带有一个值（颜色），该值属于令牌所在位置的类型。出现在特定地点的标记称为该地点的标记。CPN的标记是彼此可区分的，因此是“有色的”，与具有“黑色”不可区分标记的低级Petri网相反。地点的标记通常是多组标记值。多重集合类似于集合，不同之处在于同一个元素可能会出现几次。这意味着一个地方可能有几个具有相同令牌值的令牌为CR. Alberde等人理论计算机科学电子笔记121（2005）117123例如，1CPN的动作通过转换（画成矩形）来表示。过渡和地点由弧线连接。一个CPN的动作包括发生的transi- tions。转换的发生从连接到传入弧的位置（输入位置）移除标记，并将标记添加到连接到传出弧的位置发生转换时添加和删除的标记的确切数量及其数据值由弧表达式确定除了弧表达式之外，还可以将布尔表达式（带变量）附加到每个过渡。布尔表达式称为守卫。它指定我们只接受布尔表达式计算为true的绑定。 CPN有一个独特的标记-初始标记-用于描述系统的初始状态。CPN也可能有一个或多个标记-死标记-不能产生任何其他标记。它们描述了系统的死状态然而，CPNs并没有给PN带来任何额外的描述能力因此，任何标记的CPN都可以与同构PN相关联。将CPN转化为PN的阶段称为“展开”。之后，分析是用CPN或PN（发生图的时序逻辑，关联矩阵的线性代数，经典PN属性）。3.2功能的定义我们使用令牌对数据流进行建模。数据流的特征（源、目标、使用的服务）由标记的颜色表示。每个功能都由作用于令牌的特定CPN子网络建模。然后，一个规范的CPN模型是子网络的互连。因此，我们定义了一个全函数，将所有规范映射到CPN的子集中。这种组件方法可以自动将规范转换为等效的CPN。3.2.1结束流程功能终端流（EF）是特定于终端系统的功能，即，数据和应用服务器以及工作站。它将应用程序/用户流传输到网络。因此，产生/消费数据流的功能由CPN子网指定，CPN子网生成具有相应颜色的令牌并接收令牌（图4）。我们考虑两种类型的终端流功能：124R. Alberde等人理论计算机科学电子笔记121（2005）117我我r1，r2，.，RN见图4。 端流功能CPN模型• 主动结束流功能（AEF）：如果任何主动实体连接到EF，则EF被称为主动。• 被动结束流功能（PEF）：如果任何被动实体连接到EF，则EF被称为被动。我们为每个EF附加一个角色列表，用于指示EF可以生成的流。该列表对应于分配给代表AEF的连接活动实体的用户的角色集。在PEF的情况下，它是分配给与连接的被动实体的对象有关的权限的角色集。在根据我们的一个规范构建的CPN中，令牌对应于特定的流。因此，令牌是元组它定义了颜色域FLOW，其中：• SENDER∈ {AEF，PEF}，• ROLE∈ROLES是角色的集合，• TY PE∈ {EF，T R}表示是否转换该流（参见• NAME是结束流功能的名称.我们用一个place（efem）来指定生产者能力，这个place最初包含end-credit-ow功能可以发送的所有数据credit-ow令牌（即assignef（R，efi）1J）和transition（tefi）将其连接到另一个功能。 它的消费能力表现在由存储接收到的令牌的一个位置（EF_rec）来存储。3.2.2渠道功能通道功能对物理网络进行建模它在一个接口上接收数据流此功能可视为广播信道。当一个数据流被定向时，它不仅被寻址的目的地接收，而且被连接到这个通道的所有系统指定了传播数据流的功能1'（SENDER，role1，EF，efi）++1'（SENDER，role2，EF，efi）++...1'（SENDER，role3，EF，efrec（s，r，t，name）我埃夫埃姆（s，r，t，我泰夫我R. Alberde等人理论计算机科学电子笔记121（2005）117125←→功能1（s，r，t，name）c_fct功能2（s，r，t，name）ci_fct2...函数n（s，r，t，name）（s，r，t，name）ci_fctn（s，r，t，name）i 1（s，r，t，name）[not（member（（s，r，t，name），flow_list）][not（member（（s，r，t，name），flow_list）][not（member（（s，r，t，name），flow_list）]tci_fct1tci_fct2updatelist（（s，r，t，name），flow_list）流程表updatelist（（s，r，t，name），flow_list）流程表updatelist（（s，r，t，name），flow_list）ci_hist图五. 渠道功能CPN模型通过CPN子网从功能接收令牌并将副本发送到所有其他连接的功能。因此，通道子网络由每个连接功能的一组耦合（位置，转换）组成（图5）。过渡连接到所有其他功能。 例如，tci f ct1连接到函数2，函数3，，functn.我们还添加了一个地方（ci hist），其中包含所有to的列表穿过海峡的海牛它连接到每个转换，以确保令牌可以通过通道功能一次且仅一次。3.2.3transform功能转换功能在其两个接口之一上接收数据流，并且根据转换规则，它通过另一个接口发送该数据流或其转换。转换功能配置的语法的BNF定义如下：<变形配置>：：=[interface><<：：= [name><角色列表>：：=<角色>|<角色><“，”角色列表>因此，变换CPN子网根据变换规则改变某些标记的颜色。 我们在弧后过渡上设置函数来改变标记的颜色（图6中的T transf funct1和T transffunct2）。此外，如果一个功能可以转换一个数据流，它应该能够恢复原始的数据流（见7.1.1节）。 我们还添加了两个位置（hist tf if ct1f ct2和hist tf if ct2f ct1），以保存. . . .. . .函数n信道功能2功能1tci_fctn流程表126R. Alberde等人理论计算机科学电子笔记121（2005）117←|角色_列表1角色_列表2见图6。 转换功能CPN模型已经通过了这个功能。3.2.4过滤器功能过滤器功能停止或转发数据流。我们在防火墙、应用级网关或过滤路由器中发现了此 但我们将其限制为仅连接两个功能。过滤规则显式地表达了它的两个接口之间允许的数据流。如果它们前面有过滤器功能配置语法的BNF定义如下：<过滤器配置>：：=[interface><<<规则>：：=<名称><当前列表>：：=当前><当前><工作流>：：=：：=“AEF”|“PEF”因此，过滤器CPN子网根据它们的颜色和过滤规则停止或不停止一些令牌（图1）。7）。我们通过使用保护来限制过渡所允许的颜色来表示过滤规则（参见第7.1.2节）。然后，一个颜色不在转换保护中的标记不能被解雇。 过渡tf ifct（分别）tfifct fct）用于过滤1221来自函数1的数据流（分别函数2）到函数2（分别函数1）。在此外，我们添加两个位置（hist fif ct1f ct2和hist fif ct2f ct1）以保存已经通过该功能的所有流。hist_tfi_fct1_fct2（s，r，t，（s，r，t，name）tf_fct我1_fct2（s，r，t，name）ttf _fct_fcttransf_funct1（s，r，t，name）我1 2功能1功能2tf _fct_fct（s，r，t，我2 1transf_funct2（s，r，t，name）（s，r，t，（s，r，t，hist_tf_fct_fct我2 1ttfi_fct2_fct1功能1功能2R. Alberde等人理论计算机科学电子笔记121（2005）117127函数1功能2Rule1Rule2见图7。 过滤功能CPN模型3.3安全分析我们使用模型检查技术来确定规范是否满足安全属性。然而，该技术对组合爆炸问题是敏感的。因此，我们暴露了两个定理，使我们能够限制我们的分析CPN只有两个状态的可达图。定理3.1在任意指定产生的CPN的可达图中有且仅有一个死状态。证据参见第7.2.1节。Q定理3.2初态和死态的分析是必要和充分的。证据 参见第7.2.2节。Q定理3.2保证了我们只需要研究可达图中的初始状态和第一个定理确保我们通过模拟获得死状态。因此，不存在用于死状态分析的组合爆炸问题，然后可以研究大尺寸规格。我们现在给出初始状态和死状态必须满足的安全属性我们使用以下符号：• FUNCT，功能集，• FILTER，一组滤波器功能，• ACT IV E，一组活动的结束流程功能，• PASSIV E，一套被动式终端流功能，（s，r，t，name）hist_fi_fct1_fct2功能1【价值还是价值或......]1 2功能2（s，r，t，name）（s，r，t，name）f _fct_fct（s，r，t，name）我1 2[值“1”或值“2”或]（s，r，t，name）（s，r，t，name）（s，r，t，name）f _fct_fct我2 1（s，r，t，name）hist_fi_fct2_fct1tfi_fct1_fct2tfi_fct2_fct1128R. Alberde等人理论计算机科学电子笔记121（2005）117⊆ו ROLES，角色的集合，• SENDER={AEF，PEF}，• 互联FUNCTFUNCT，定义功能之间直接连接的关系，• A：（ACT IVEPASSIV E）→2ROLE，定义分配给结束流程功能的角色集的关系，• COLOR，CPN中的颜色集合，• P LACE，CPN中的位置集• T okens：P LACE→Bag（COLOR），其中Bag（COLOR）是COLOR上的多重集的集合。它提供了一组呈现在一个地方和一个状态中的彩色标记。为了简化属性的编写，我们使用特殊字符 表达状态|=属性表示CPN可达性中的状态图满足性质-si是初始状态，sf是死状态。现在，我们定义安全属性。定义3.3保密性基本上，机密属性保护数据免受未经授权的披露。因此，在我们的模型中，它禁止end-Cowflow功能在任何时候从任何未分配的角色接收未转换的数据流。<$ef∈ACTIVE，<$r∈ROLES，r∈/Assigned（ef）F型|=<，r，EF，>∈/Tokens（ef3.4完整性属性rec（2）传统上，完整性的属性禁止未经授权的实体任何创建、修改或销毁对象。然后，在我们的模型中，此属性意味着结束流功能只能通过其分配的角色生成数据流。ef∈ACTIVE伊什岛|=<，r，，ef>∈/Tokens（ef3.5可用性的性质rec（三）此属性规定所有授予的服务必须可用于所有授权实体。在网络环境中，与这些服务相对应的数据流必须能够在两个设备之间传输。因此，在我们的模型中转换它会导致：被动）端-数据流功能必须能够使用所有数据流，R. Alberde等人理论计算机科学电子笔记121（2005）117129由每个被动（分别）发送的分配角色。活动）结束流功能。设ACT IV Er={ef a∈ ACT IV E|r ∈ f（f a）}PASSIV E r={ef p∈PASSIV E|r∈ f（f p）}r∈ROLES，S F|= ∈ T okens（ef rec）<$∈ Tokens（ef rec）一个p（四）当我们打算解决设备配置时，我们用新的安全属性来完成这些定义3.6分割属性有了这个属性，我们希望尽可能地限制数据流的传播。它声明数据流只能传递位于数据流源和可能的正确目的地之间设ACT IV E r={ef a∈ ACT IV E|r∈（ef a）}PASSIV Er={ef p∈PASSIV E|r∈ f（f p）}<$f∈FILT ER，<$fct1， fct2 ∈FUNCT，<$r ∈ROLES，Connected（f，fct1）已连接（f，fct2）（s f|= ∈T okens（histfct1f ct2）Efa∈ACT IV Erfct2∈P ath（f，efa））（s f|= ∈T okens（histfct1f ct2）ffp∈PASSIV Erfct2∈P ath（f，efp））（5）以下两个约束旨在抑制在通常上下文中不使用的已实现的过滤或转换规则定义3.7非生产性过滤规则设f是连接到泛函fct1和fct2的滤波器泛函。我们说过滤规则FRL，它让数据流从fct1传递到fct2，如果这个流从不试图通过过滤器功能，那么它是非生产性设规则FRL=fct1→ fct2t（s，r），其中fct1，fct2∈FUNCT，t∈ {EF，TR}，s∈AEF，PEF，r∈ROLES则FRL是非生产的iSF|=∈/Tokens（histffct1fct2）（六）定义3.8非生产性转换规则设tf是连接到泛函fct1和fct2的变换泛函。我们说转换规则TRL，它将具有角色r的数据流从fct1转换到fct2，如果任何具有角色r的130R. Alberde等人理论计算机科学电子笔记121（2005）117R在任何时间都在方向FCT1-FCT2上设TRL =fct1→ fct2r，其中fct1，fct2∈FUNCT，r∈ROLEnTRL是n n nnp roductiveisf|=<，r，EF，>∈/Tokens（histffct1fct2）n，r， TR，>∈/Tkens（histffct2fct1） （七）4网络安全策略评估实例在本例中，我们考虑企业网络基础设施的传统情况。它由一个专用网络和一个DMZ组成。整体由边缘路由器连接。在专用网络中，安装了一个App Server服务器，并在DMZ中安装了一个FTP服务器（图1）。8）。 应用层安全性策略是一种非层次化的RBAC策略。它定义了两个用户组：VPN成员组和其他用户组。 此组织仅基于授予的权限。App Server服务器仅专用于VPN成员组使用的服务。FTP服务器有两个目录：/confidential和/pub。目录机密包含仅可由VPN成员用户组访问的数据。所有人都可以访问pub目录的数据。User1、User2、User3和User4属于VPN会员和其他组 User5只是Others组的成员。应用层安全策略可以表示为：VPN（VPN成员）={（+所有访问，FTP服务器/机密），（+all access，AppServer）}其他（Others）={（+all access，FTPServer/pub）}图图8还显示了网络拓扑规范和用我们的语言实现的网络级安全策略。我们还将CPN规范中使用的名称附加到每个功能中。首先，我们指出，我们的方法不考虑设备作为实体，而是基于对数据流进行的处理。专用网络、非军事区和互联网互连基础设施由于通道功能而被指定，因为我们使用它们的传输功能。这种大粒度的规范方法只考虑这些基础设施提供的最小功能集：它们的互连能力。相反，可以根据边缘路由器所显示的规格进行细化。它显然具有互连功能（通道功能），设置为具有过滤功能（三个过滤功能）和加密机制（转换功能，R. Alberde等人理论计算机科学电子笔记121（2005）117131应用程序_用户5专用网络互联网User1路由器User3User2DMZ用户4FTP服务器/机密/pubVPN会员ef1VPN会员别人EF2专用网络规则1规则2F1边缘路由器F2VPN会员TF1规则6F3EF5互联网TF2别人VPN会员VPN会员其他EF3DMZVPN会员其他EF4见图8。 VPN示例例如安装了一个UART模块）。路由的建模是通过过滤器功能的过滤规则来完成的服务器由两个PEF指定。App Server服务器具有VPNmembers角色，因为只有具有VPNmembers角色的用户才具有访问权限。对应于FTP服务器的PEF具有Others和VPNmembers角色，因为权限（+所有访问，FTP服务器/发布）被分 配 给 Others 角 色 ， 而 （ + 所 有 访 问 ， FTP 服 务 器 / 机 密 ） 被 分 配 给VPNmembers角色。用户1和用户2的设备由单个AEF（EF1）表示，因为用户1和用户2具有相同的角色（其他人和VPN成员），并且这些AEF连接到相同的通道功能，这要归功于角色的概念，它减少了规范的整体大小。 以相同的方式，用户3和用户4的设备由AEFEF5指定。的用户5的设备由AEFEF4指定。自动添加AEF与权限减少的角色一起使用，可以定义可以授予通道功能的置信度（参见[3]以获得“通道信任属性”的完整定义 在这个例子中，Rule3规则4132R. Alberde等人理论计算机科学电子笔记121（2005）117我们没有具体说明互联网网络的结构，但它被认为是 作为互连环境，其中任何连接的用户至少具有访问FTP服务器的/pub目录的权限。这允许根据所需和/或已知细节的水平进行指定的极大灵活性现在我们将解释安全策略。与以下各项相关的过滤规则我们的示例的过滤器功能是：• 规则1=EF（AEF，其他），（AEF，V PN成员）• 规则2=EF（PEF，其他）• 规则3=EF（PEF，其他），（PEF，V PN成员），（AEF，V PN成员）• 规则4=EF（AEF，其他），（AEF，V PN成员）• 规则5=EF（PEF，Others），（AEF，Others）T R（PEF，V PNmembers）• 规则6=EF（AEF，Others）T R（AEF，V PN members）定义了两个转换功能，以保护VPN成员角色数据流在互联网通道功能上的安全。 事实上，使用Others角色连接到Internet通道功能的用户永远无法访问FTP服务器或App服务器上的机密数据。我们使用CPN/tool [40]创建与规范相关的CPN（图10）。它显示了最初的标记。图10指出，对于大尺寸规格，手动构建CPN变得复杂。因此，我们使用Java编程语言开发了一种自动执行评估任务的工具。它将一个指定文件作为输入（图9）。首先，分析了句法。如果语法正确，它将生成等价的CPN并检查所有属性。最后，它产生一个结果文件（图11），表明性能是否满足。如果一个属性不满意，解释原因。在我们的例子中，该工具表明（图11），confi-n的属性得到满足，并且不存在非生产性的转换规则。尽管如此，由于ef2无法接收到任何数据流，使用来自ef5的VPN成员角色，ef1无法接收任何具有来自ef3和ef5的角色VPNmembers不能接收来自ef2的角色VP-Nmembers的任何流。 由于过滤器功能f 3中从tf1到Internet的规则EF（AEF，Others），分区属 性 不 满 足。最 后，在过滤器功能f2中从dmz到边缘路由器的过滤规则EF（AEF，VPN成员）是非生产性的。综上所述，本规范R. Alberde等人理论计算机科学电子笔记121（2005）117133/* 终端流功能定义 */#名称= ef1#roles = others，vpn-members;#connection = private_network<公司简介#名称= ef2#roles = vpn成员; #connection= private_network<公司简介#名称= ef3#roles = others，vpn-members;#connection = dmz#name = ef4#roles = others;#连接=互联网#名称= ef5#roles = others，vpn-members;#connection = tf2/* 转换函数定义 */<运输>#name = tf1#connection1 = edge_router#connection2 = f3#rules_1->2 = vpn成员;#rules_2->1 =无;<运输>#name = tf2#connection1 = ef5#connection2 =internet#rules_1->2 = vpn成员;#rules_2->1 =无;/* 过滤器功能定义 */<滤镜>#name = f1#connection1 =私有网络#connection2 =边缘路由器#rules_1->2 =EF（AEF，others），（AEF，vpn-成员）;TR NONE;#rules_2->1 =EF（PEF，其他）;TR无;<滤镜>#name = f2#connection1 = dmz#connection2 =edge_router #rules_1->2 =EF（PEF，others），（PEF，vpn-members），（AEF，vpn-members）;TR NONE;#rules_2->1 =EF（AEF，others），（AEF，vpn-members）;TR NONE;<滤镜>#name = f3#connection1 = tf1#connection2 =互联网#rules_1->2 =EF（PEF，其他），（AEF，其他）; TR（PEF，vpn成员）;#rules_2->1 =EF（AEF，其他）;TR（AEF，vpn-成员）;/* 通道功能定义 */<频道>#name = private_network#connection = ef1，ef2，f1;<频道>#name = edge_router#connection = f1，f2，tf1;<频道>#name = internet#connection = f3，ef4，tf2;<频道>#name = dmz#connection = ef3，f2;并不安全5相关作品见图9。 规格文件不同的工作侧重于适当的工具援助。基于模型的管理方法[18，20]利用被管理系统的面向对象模型设计者以图形方式定义三个抽象层次模型，工具指导推导。此外，最先进的工具之一[34]建议134R. Alberde等人理论计算机科学电子笔记121（2005）117见图10。 我们的VPN示例1'（AEF，Others，EF，ef4）ef4em流（s，r，t，updatelist（（s，r，t，n），list_f）列表_流程（s，r，t，tef4 ef4reclist_f[]hist_c2流（s，r，t，hist_f1_c1c2（s，r，t，（s，r，t，（s，r，t，流ef2rec[not（member（（s，r，t，n），list_f））]updatelist（（s，r，t，n），list_f）list_f流流（s，r，t，[not（member（（s，r，t，n），list_f））]C2F1TC2F1流hist_tf1_c2c4hist_f3_tf1c41‘(PEF,（s，r，t，[not（member（（s，r，t，n），list_f））]（s，r，t，n）c1ef2 tc1ef2（s，r，t，案例RVPN成员=> 1'（s，r，TR，n）流量（s，r，t，n）|_ => 1'（s，r，t，n）C4ef4TC4EF4（s，r，t，（s，r，t，流ef2em tef2（s，r，t，n）[（s=AEF，r= Others，t=EF）（s=PEF，r= VPN成员，t=EF）]（s，r，t，n）[(s=PEF和r=其他和t=EF）或（s=AEF和r=其他和t=EF）或tf3tf1c4（s=PEF，r= VPN成员，t=TR）]updatelist（（s，r，t，n），list_f）（s，r，t，[]流流（s，r，t，（s，r，t，（s，r，t，[not（member（（s，r，t，n），list_f））]（s，r，t，n）TC2TF1hist_c4f1c1c2 tf1c1c2TF1C2C4ttf1c2c4f3tf1c4（s，r，t，c2tf1流流列表_流程流（s，r，t，（s，r，t，c4tf1TC4TF1（s，r，t，流（s，r，t，流（s，r，[not（member（（s，r，t，n），list_f））]updatelist（（s，r，t，n），list_f）list_f[(s=PEF和r=其他和t=EF）][not（member（（s，r，t，n），list_f））]（s，r，t，n）ttf1c4c2 tf1c4c2（s，r，t，n）（s，r，t，（s，r，t，n）tf3c4tf1 f3c4tf1（s，r，t，（s，r，t，ef1rectf1c2c1 f1c2c1（s，r，t，流流C2f2TC2F2c4tf2（ s，r，t，n）流（s，1‘(AEF,VPNmembers,EF,ef1)++1‘(AEF,Others,[not（member（（s，r，t，n），list_f））]（s，r，t，n）c1ef1 tc1ef1TC4TF2流（s，r，t，（s，r，t，流[(s=AEF，也r=其他，也t=EF）或其他（s，r，t，ef1em tef1hist_tf1_c4c2（s=AEF，r= VPN成员，t =TR）]流[not（member（（s，r，t，n），list_f））]案例R流流VPN成员=>| _ => 1'（s，r，t，n）（s，r，t，hist_f1_c2c1流hist_f3_c4tf1流（s，r，t，流[not（member（（s，r，t，n），list_f））]（s，r，t，（s，r，t，流TC1F1c1f1案例RVPNmembers =>1'（s，r，TR，n）ttf2ef5c4|_ => 1'（s，r，t，n）（s，r，t，n）（s，r，t，n）hist_tf2_ef5c4tf2ef5c4流流（s，r，t，（s，r，t，hist_f2_c3c2tf2c3c