软约束与安全性：完整性策略和加密协议的统一视角与定量方法

理论计算机科学电子札记142（2006）11-29www.elsevier.com/locate/entcs安全性的软约束詹保罗·贝拉1Dipar timentodiMaticaeInformatiCatStefano Bistarelli Stefano Bistarelli2，3Dipartimentodiscienze，Universit'adegliStudi“G. D'A意大利比萨西蒙·N 福利4爱尔兰科克大学计算机科学系摘要完整性策略和加密协议有很多共同之处。它们允许多个参与主体，并由控制主体应该或不应该执行的操作的规则集组成。它们旨在维护各种安全属性，其中最重要的是完整性，保密性和身份验证。本文对完整性策略和加密协议的分析采取了统一的观点：它们是必须被设计为对给定的已知威胁模型的攻击具有足够鲁棒性的工件。例如，完整性策略规则提供了对内部欺诈威胁的弹性该框架建模使用（软）约束和分析对应的软约束的满意度问题。软约束促进了分析完整性、机密性和身份验证的定量方法举例如下：完整性策略可以在不同的环境下实现不同级别的完整性;协议消息可以为不同的主体享受不同级别的机密性;主体可以与不同的主体实现不同级别的认证。关键词：约束，安全协议，完整性策略。1电子邮件：giamp@dmi.unict.it2 电子邮件地址：bista@sci.unich.it3电子邮件：stefano. iit.cnr.it4电子邮件：s. cs.ucc.ie1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.01112G. Bella等人/理论计算机科学电子笔记142（2006）111引言完整性、机密性和身份验证是基本的安全属性。在本文中，我们使用的约束求解框架，统一研究他们所有的完整性政策和密码协议的背景下。完整性策略定义了信息修改被授权并由系统安全机制强制执行的情况这是通过根据系统和基础设施对系统的安全相关组件施加的约束来对系统和基础设施进行建模来完成的这导致了完整性一致性的定义，可以作为约束解决问题来解决。使用基于约束的框架的另一个优点是，可以使用软约束对完整性进行定量分析[6，7，8，2，18，19，11，14，17]。定量分析提供了系统安全性的细粒度测量，而不是传统的“清晰”约束所提供的简单加密协议是不安全网络的主体之间的一组规定的消息交换机密性是消息的属性，不向恶意主体公开。另一个关键目标是身份验证，确认主体参与协议会话。到目前为止，保密性基本上被形式化为一个仅仅是“是或否”的属性，所以人们可以直接声明一个密钥是否保密。我们研究的动机是为这个目标研究一个更好的正式概念。我们已经开发了l-保密级别的概念，其中l是安全级别，表示达到目标的强度由于采用了基于半环的软约束规划，安全级别每个主体为每条消息分配自己的安全级别- 不同级别的不同消息-表达主体这让我们正式确定不同的目标级别被授予不同的主体。本文的结构如下。第2节介绍了约束和约束求解问题。第三节首先提出了一种在清晰约束框架内对系统进行建模的抽象方法，然后描述了如何使用软约束进行定量完整性分析。本文继续介绍用于分析密码协议的关键SCSP，关于保密性的定义，以及一个重要的例子（第4节）。最后给出了一些结论（第5G. Bella等人/理论计算机科学电子笔记142（2006）11132约束求解约束求解是一种新兴的软件技术，用于对大型问题进行声明式描述和有效求解约束编程过程包括需求（约束）的生成和这些需求的解决方案，由专门的约束求解器。当一个问题的需求被表示为一个变量上的布尔谓词的集合时，我们得到了所谓的清晰（或经典）约束满足问题（CSP）。在这种情况下，问题通过找到满足所有约束的变量的任何分配来解决有时，当需要对问题进行更深入的分析可以使用软约束。软约束将定性或定量值关联到整个约束或其变量的每个分配这些值被解释为偏好或重要性或成本的水平水平通常是有序的，反映了某些水平（约束）比其他水平更好的事实。当使用软约束时，有必要通过合适的组合算子指定如何从约束中的偏好获得全局解的偏好水平软约束概念的几种形式化目前是可用的。在下文中，我们参考了基于c-半环的形式化[6，7，9，2]，它可以被证明是广义的，并且可以表达清晰和软约束[7，3]。2.1基于半环的CSP基于半环的约束从偏序集合中为它的变量的每个实例化分配一个相关联的值。当处理清晰约束时，值是布尔真和假，表示可接受和/或不可接受的值;当处理软约束时，值被解释为偏好或概率或成本。框架还必须处理约束的组合。要做到这一点，必须考虑到这些额外的值，因此形式主义必须为值和约束的元组的组合（×）和比较（+）提供合适的操作这就是为什么这种形式化是基于c-半环的概念2.2半环一个半环是一个元组A，+，×，0，1 <$A，使得：A是一个集合，0，1∈A;+是交换的，结合的，0是它的单位元;×是结合的，分布在+上，1是它的单位元，0是它的吸收元。C-半环14G. Bella等人/理论计算机科学电子笔记142（2006）11（在下文中，我们将始终使用半环这个词来代表c-半环。让我们考虑关系≤S在A上使得a≤Sbi <$a+b=b。可以证明：≤S是偏序;+和×是单调的≤S;0是它的最小值，1是它的最大值，并且<$A，≤S<$A是具有最小上界算子+的完备格。此外，若×是幂等元，则：+分布在×上，且<$A，≤S<$A是具有最大下界算子×的完全分配格。≤S关系是我们用来比较元组和约束的关系：a≤Sb直观上意味着b比a好。2.3约束问题给定有限域D上的半环S=A，+，×，0，1<$A和变量的有序集V，约束是一个函数，给定变量的赋值η：V→D，返回半环的值通过使用这种符号，我们定义C=η→A为从S，D和V开始可以建立的所有可能约束的集合。考虑一个约束c∈ C。我们定义他的支撑为supp（c）={v∈V|n，d1，d2.cη[v：=d1]cη[v：=d2]}，其中.η[v：=d]vJ=d如果v=VJ，否则为ηvJ。请注意，cη[v：=d1]可以是cηJ，其中reηJ与关联不相同v：=d1（即运算符[]优先于应用程序）。约束求解问题是一对约束集C，con，其中con是约束集，C是约束集：con是约束集C的感兴趣的变量集，然而，约束集C也可能涉及不在con中的变量。注意，经典CSP是SCSP，其中所选择的c-半环是：{f alse，true}，许多其他“软”CSP（概率、加权等）可以通过使用合适的半环结构（Sprob=[0， 1]，max，×， 0，1，Sweight =R，min，+，+∞，0 ）的。示例1图1显示了模糊CSP5的图形表示。变量X和Y和约束分别由节点和无向（c1和c3为一元，c2为二元）弧表示，半环值被写入相应元组的右侧感兴趣的变量5 模糊CSP可以在SCSP框架中建模，通过选择c-半环SFCSP=[0，1]，max，min，0，1G. Bella等人/理论计算机科学电子笔记142（2006）1115（a）0 → 0。9（a，a →0。8（a）0 →0。9（b）0 →0。1（b）→ 0. 5（c= 0）。9C1X（a，b）→0。2（a，c）→0。2（b，a）→ 0（b，b →0c2）（b，c）→ 0。1（c，a → 0。8（c，b）→ 0。2（c，c → 0。2（c= 0）。5C3YFig. 1.模糊CSP。(that是集合con）用双圆表示这里我们假设变量的定义域D只包含元素a、b和c。如果半环值表示概率/模糊值，则例如元组a，c→ 0。2可以被解释为意味着X和Y分别具有值a和cΔ2.4组合约束当存在一组软约束C时，约束的组合权重使用运算符C×C → C计算，定义为（c1<$c2）η=c1η×Sc2η。给定一个约束c∈ C和一个可变的v∈V，V−{v}，写作c（V−{v}）是约束cJs. t。 cjη =d∈Dc η [v：= d].在-形式上，投影意味着从支持中消除一些变量这通过将剩余变量上的每个元组关联到半环元素来完成，该半环元素是由原始约束关联到该元组在被消除的变量上的所有扩展的元素的总和简而言之，通过半环的乘法运算进行组合，通过加法运算进行投影。2.5解决方案SCSPP= C，con的解是约束Sol（P）=（C）con。也就是说，我们组合所有的约束，然后在con中投影变量。通过这种方式，我们得到了支持度（不大于）con的约束，它是由整个SCSP“诱导”的。请注意，当所有变量都感兴趣时，我们不需要执行任何投影。解决方案本身就是约束，可以通过扩展≤S阶。我们说一个约束c1至少和c2如果c1±c2，其中对于任何变量赋值η，则c1± c2 c1 η≤S c2 η16G. Bella等人/理论计算机科学电子笔记142（2006）11inv支付船号发票验证船供货商验证装运支付V基础设施投资支付支付系统企业因此，如果c1±c2成立，那么约束c1可以被认为是约束c 2的细化或例子2再次考虑图1的模糊CSP的解决方案。它将一个半环元素与变量X的每个定义域值相关联.这样的元素是通过首先将所有约束组合在一起，然后将获得的约束投影到X上来获得的。例如，对于元组A，9（这是在约束c1中分配给X = a的值），0。8（这是分配给c 2中的X = a，Y = a的值）和0。9（其中是c中Y=a的值3）。因此，该元组的结果值为0。8.我们可以对元组a，b→ 0做同样的工作。2，α，cα → 0。2，αb，αb →0，b，b1，αc，αc → 0。8，βc，βb → 0。2，则c→ 0。2.然后将获得的元组投影到变量X上，获得解⟨a⟩ → 0. 8，b→ 0。1，且θcθ → 0。8.Δ3分析完整性策略完整性策略定义了信息修改被授权并由系统安全机制强制执行的情况。然而，在复杂的应用程序系统中，完整性策略可能被错误地指定，因此，用户可能被授权修改可能导致意外系统危害的信息。在本节中，受[4，5]结果的启发，我们描述了如何使用约束求解来建模和分析应用系统完整性策略的有效性。在下文中，我们通过使用[12，13]中的示例来展示如何将功能需求表示为在系统生命周期内不变的注. 船舶表示约束变量图二、一个简单的支付企业示例3一个简单的企业接收发运，并为供应商生成相关付款需求分析确定了操作shipnoteG. Bella等人/理论计算机科学电子笔记142（2006）1117和付款，分别对应于装运货物的到达（票据）及其相关付款。为保证完整性，分析确定了一项要求，即系统向供应商支付的款项不应超过所发运货物的规定价值让约束变量ship和pay分别表示到目前为止发货的总价值约束概率将需求描述为变量ship和pay上的不变量。诚信支付≤船舶图2概述了这一要求的可能实现职员核实发货单，并将发票详细信息（行动发票）输入计算机系统，计算机系统反过来向供应商付款这个实现是用变量ship、pay和变量invv来描述的，invv表示到目前为止生成的发票的总价值。职员处理的发票数量不应超过装运数量，因此，职员办事员发票≤船舶对发票处理应用系统的要求是申请支付≤发票企业设计被指定为约束，进口申请办事员通过将Appl和Clerk约束组合在一起来获得。由于Imp1确保了高级别的要求Probity，因此在该系统中确保了直观性和完整性。Δ在上面的例子中，供应商到系统的接口V是根据变量ship和pay建模的这些变量之间的约束用于描述我们对系统的要求我们希望通过这个接口来确保实现保持诚实，也就是说，Imp{ship，pay}± Probity我们不关心“内部”变量inv的可能值根据定义，上述等式定义了Imp{ship，pay}的所有可能解都是18G. Bella等人/理论计算机科学电子笔记142（2006）11也就是说，对于变量的任何赋值η，进口1吨{ship，pay} η≤S概率η定义3.1我们说需求S局部地精化需求 R通过由变量集V i SV±RV描述的接口。示例4继续示例3，假设应用系统将可靠地运行并支持Appl. 然而，假设办事员总是可靠地作为办事员行事是不合理的。实际上，店员可以采取任何行为：Clerk（inv≤shipinv>ship）=true进口2----办事员----申请Imp2是实际企业的更真实的表示。它比以前的设计Imp1更准确地反映了其基础设施的可靠性。然而，由于投资不再受约束，它可以取任何值，因此，支付不受约束，我们有Imp{ship，pay}/± Probity也就是说，该系统的实施不够稳健，无法以安全的方式处理内部故障并维持原有的诚信要求。Δ在[15]中，完整性被认为是可靠性的一个属性。可靠性被描述为“计算机系统的一种在[12，13]中，这种可靠性的概念可以被看作是一种细化，企业的可靠性的性质由此被明确规定。定义3.2（可依赖性）如果R给出了企业的需求， S是其建议的实现，包括有关其基础设施可靠性性质的细节，则 S在由变量集E描述的接口处与 R一样依赖安全，当且仅当 S=E±R=E职责分离[20，10]是实现完整性的常见实现技术。虽然容错技术复制了一个操作，但职责的分离可以被认为是跨不同用户域的操作分区。例5当货物到达时，职员在货物进口处验证托运货物（在系统中输入托运货物）。当发票到达时，不同的职员将详细信息输入系统，如果发票与发票匹配，则生成付款只要行动是分开的G. Bella等人/理论计算机科学电子笔记142（2006）1119P1验证托运托运P3更新委托装船通知供货商支付P2核对发票地位发票P4V基础设施反相生成支票应用系统企业支付con船则输入伪造的托运货物或发票的单个职员可以被系统检测到。这在图3中描绘。图三. 支持职责设变量inv和con分别表示到目前为止收到的发票和寄售的总值规范Clerk1、Clerk2和App3定义了对系统变量的约束，反映了预期由Clerk和应用系统维护Clerk1库存≤发货Clerk2库存≤发货App3支付金额≤min（con，inv）即使一个职员失败，这个系统也像诚实一样可靠，也就是说，我们有（ Clerk1Clerk2Clerk3 ） {ship ， pay}±Probity（Clerk2Clerk3）{ship ，pay}±Probity（ Clerk1Clerk3 Clerk3 ） {ship，pay}±Probity请注意，没有约束意味着它不将变量限制为任何值。然而，该系统不能承受两个办事员的故障，也不能承受应用软件的故障删除由两个职员或应用程序施加的App 3发货、付款/±诚信（Clerk1<$Clerk2）{ship，pay}/±Probity根据目前的定义，我们的规范有利于支付企业，而不是供应商：付款可能会很晚，或者根本没有付款，但绝不会是假的。如果一个职员失败，那么付款可能不会进行。实际上，基础设施包含许多附加组件;记录故障的审计日志和做出判断并纠正这些不一致的管理程序Δ20G. Bella等人/理论计算机科学电子笔记142（2006）113.1定量完整性分析上一节中的示例使用明确的约束来描述系统需求和实现。当需要对系统进行定量分析时，则例6再次考虑诚实性要求，并假设我们的目标不仅是有一个正确的实现，而且，如果可能的话，有“最好的”可能的为了做到这一点，我们考虑变量ship和pay之间的软约束，它为配置ship=a和pay=b分配由整数a-b6表示的偏好水平。如果我们正在为买家寻找最好的实施方案，那么我们将努力最大限度地提高这一水平。通过这种方式，可以比较同一系统的不同实例，并且可以检查和分析不同的实现。软约束也为评估和比较不能支持预期需求的弹性较低的实现例如，如果无法找到满足以下条件的可接受实现Imp：Imp{ship，pay}±Probity然后，人们可能会（在某种意义上）通过选择弹性较低但可接受的实现中的最佳实现而感到满意。给定不太有弹性的实现Imp1和Imp2，则它们对应的半环级别提供允许选择弹性较低的实现中的“最佳”的相对排序。基于概率的推理也可以在软约束框架内完成例如，考虑一个Imp3实现，它确保付款次数永远不超过3，而不管收到的发货次数。这表示为：杂质含量≤ 3。假设有一个变量装运的约束，它指定了在某个时间可能进行的装运数量的概率如果概率分布的性质使得ship的值通常更有可能大于3，则Imp3是一个并非不合理的实现（尽管Imp3{ship，pay}±Probity不成立）。Δ6这个值代表了从船舶上支付的费用。我们的目标是让pay=ship，但有时这是不可能的，我们的目标是最小化a-b差异。G. Bella等人/理论计算机科学电子笔记142（2006）11214密码协议安全协议规定了计算机网络的远程主体应该如何交互，以获得特定的安全目标。保密和身份验证的关键目标可以以各种形式实现，每种形式的强度都不同。在本节中，受[1]结果的启发，我们描述如何使用软它们不再像以前的文献中那样被形式化为仅仅是/否属性，而是获得了一个额外的参数，即安全级别。例如，不同的消息可以享受不同级别的机密，或者主体可以通过不同的主体实现不同级别的身份验证。4.1安全半环我们的安全半环用于指定每个主体安全级别的范围从最安全（最高）级别未知到最不安全（最低）级别公开。直觉上，如果AA在m上的安全级别越低为了简单起见，我们声明安全级别的粒度和被授权知道m的主体的数量之间没有关系。更正式地说，给定一个自然数n，我们定义安全级别的集合L如下：L ={未知，私有，交易1，交易2，. . . ，traded n，public}我们引入一个加法算子+sec和一个乘法算子，×秒为了给这两个运算符下一个简洁的定义，并简化下面的处理，让我们定义一个方便的双重命名：–≡交易-1–≡交易0–≡交易n+1让我们考虑一个指数i和一个指数j，它们都属于整数的闭区间[-1，n+1]。我们用下列公理定义+sec和×secAx. 1：交易i+秒交易j=交易max（i，j）Ax. 2：交易i×交易sec j=交易min（i，j）22G. Bella等人/理论计算机科学电子笔记142（2006）11结构Ssec=Lsec，+sec，×sec，public，unknown，可以很容易地被证明是一个c-半环。利用安全半环，我们定义了网络约束系统CSn=其中：• Ssec是安全半环（4.1节）;• V是一个有界的变量集。• D是一组有界值，包括空消息{||}和所有原子消息，以及通过关联和加密递归获得的所有消息。. 网络约束系统表示可以在其上执行密码协议的计算机网络。V的元素代表网络主体，D的元素代表所有可能的消息。原子消息通常是主体名称、时间戳、随机数和加密密钥。从协议会话期间看到的消息的操纵中发展的主体我们定义规则来计算每个主体对新生成的消息的安全级别。这些规则规定，每次通过加密或解密操作消息时，消息的安全级别都会有所降低图4中给出了一组可能的规则，其中函数def与投射到通用主体A上的通用约束相关联。可以研究不同的规则来捕获其他特征。串连：v1，v2unknown;f（m1）=v1;f（m2）=v2; publicintfinds（{|m1，m2|}）=v3publicintfinds（{|m1，m2|}）=（v1+secv2）×secv3拆分：v3unknown;f（m1）=v1;f（m2）=v2; publicintfinds（{|m1，m2|}）=v3def（m 1）= v 1 ×secv 3; def（m 2）= v 2 ×sec v 3加密方式：交易l1，交易l2<未知;f（m1）=t radedl1;f（m2）=t radedl2;f（{|M1|}m2）=t radedl3publicintfinds（{|M1|}m2）=（t radedl1+ 1+se radedl2）×seradedl3解密：交易l2，交易l3<未知;f（m1）=t radedl;f（m−1）=t radedl;f（{|M1|}）=交易量122m23def（m1）=交易l1×交易秒l2+ 1×交易秒l3见图4。 安全级别G. Bella等人/理论计算机科学电子笔记142（2006）11234.2初始、政策和可归责SCSP协议P的策略是一组规则，其中声明了协议执行所需的先决条件，例如哪些消息是公共的，哪些消息对于哪些主体是私有的。通过我们的安全级别捕获这些策略规则是直观的（第4.1节）。准确地说，这些规则可以转化为网络约束系统的一元约束。对于每个主体A∈ V，我们定义一个一元约束，该约束规定A它将安全级别公共与所有人都知道的那些消息相关联，通常是主体名称、时间戳和公钥;将级别私有与A如果P使用对称密码，则为A的A将在协议执行期间发明的秘密，或其他当事人这个过程定义了我们为P命名的初始SCSP，它指定了P的会话尚未启动时主体协议P的策略还指定了在一对主体之间的会话期间必须交换的消息如何形成。我们从协议策略中读取A→B：m形式的每个允许步骤及其非正式描述，它解释了A是发明了m还是它的一部分。然后，我们根据所考虑的事件，通过向初始SCSP添加新的约束，为P构建策略SCSP。如果该事件是主体A如果该事件是主体A向主体B发送消息m，则考虑与A上的消息m相关联的每当m通过操纵其他消息获得时，这个级别通过蕴涵计算（图4）（而不是m是例如刚刚发明的新随机数，其安全级别由算法的前一一个二进制约束，它将新计算的安全级别分配给元组{||}，m{\displaystyle m}（并且对于所有其他元组都是未知的）现在被添加到变量A和B对上的当前SCSP。对于策略所允许的有限数量的事件中的每一个事件重复该推理当没有更多的事件要处理时，当前的SCSP作为P的策略SCSP返回，这是我们的协议的形式化模型由协议P引起的真实网络历史必须考虑某些主体的恶意活动。每一个这样的历史可以被看作是一系列的事件的形式：一个主体的发明新的消息，一个prin-unr的发送消息，没有被拦截，而第二个事件意味着，24G. Bella等人/理论计算机科学电子笔记142（2006）11消息的倾向接收者确实得到了消息，第三个意味着一些恶意主体阻止了发送的消息的传递我们可以将任何真实网络历史中某个点的任何网络配置建模为SCSP。我们将协议P和源于协议执行的网络配置nc作为输入。增加了对第三类事件的处理：当A向B发送消息并被另一个主体C拦截时，必须在A，C而不是A，B对上声明相应的约束。我们得到了我们称之为P的可归责SCSP。4.3正式确认使用安全级别，我们开发了机密和机密攻击的统一定义，似乎可以捕获任何策略要求。直觉上，如果一个主体对一条消息在实践中，确定我们对l-置信度的定义是否在SCSP中成立需要计算可归责SCSP的解，并将其投射到某些利息本金上。l越高，目标越强。定义4.1[l-置信度]给定可归责SCSPp和本金A，我们说对于A在pi <$Sol（p）<${A}（m）=l中存在m的l -置信度。通过初步的分析，我们可以研究在没有恶意行为的理想条件最重要的是，通过实证分析，我们可以研究协议在现实威胁下执行所产生的特定网络配置上实现的目标我们专注于相应的归咎SCSP，计算其解决方案，并将其投影到一个主要的利益：我们获得所有消息的主要在策略SCSP上执行相同的操作后，我们可以比较结果。如果可归因的某个水平低于策略的相应水平，则可归因SCSP中存在发作事实上，已经发生了一些恶意操作，这些恶意操作对由可归责SCSP建模的网络配置做出了贡献，从而降低了策略SCSP所规定的一些安全级别。重要的是要强调，任何当事人都可能故意或无意地执行了这些操作。定义4.2[确认攻击]给定一个策略SCSPP，同一协议的一个可归责SCSPp，以及一个主体A，我们说A对pi中的m进行了确认攻击。G. Bella等人/理论计算机科学电子笔记142（2006）1125对于A，在P中有m的l-置信度，对于A，在p中有m的lJ-置信度，并且LJ

下载后可阅读完整内容，剩余1页未读，立即下载