Homer演算：高阶移动嵌入式资源的类型智能卡模型与安全性建模

理论计算机科学电子笔记194（2007）23-38www.elsevier.com/locate/entcs高阶移动嵌入式资源的硬和软类型智能卡安全性建模1Mikkel Bundgaard和Thomas Hildebrandt2Jens Chr.Godskesen3哥本哈根IT大学Rued Langgaards Vej 7，DK-2300 Copenhagen S，Denmark{mikkelbu，hilde，jcg}@itu.dk摘要我们为高阶移动嵌入式资源（Homer）的演算提供了一个受直觉主义逻辑启发的类型系统，从而产生了第一个结合了直觉主义线性（不可复制）和非线性（可复制）高阶移动进程、嵌套位置和本地名称的进程演算。的类型系统保证在计算期间线性资源既不被复制也不被嵌入非线性资源中。我们使用微积分建模一个简单的电子现金智能卡系统，其安全性取决于（线性）移动硬件，嵌入式（非线性）移动过程，和本地名称之间的相互作用。 纯粹的线性演算无法表达嵌入式软件进程可以复制。相反，纯粹的非线性演算将无法表达移动硬件进程不能被复制。关键词：高阶进程传递，线性类型，可复制和不可复制资源，嵌套位置，安全性，智能卡1引言在Mobile Ambients [10]的开创性工作之后，已经提出了几种进程演算，包括Mobile Ambients [18，4]的变体，Seal演算[11]和Homer演算[15]，它们结合了（1）移动进程，（2）嵌套显式位置和（3）本地名称。 这些模型是由全球普适计算中的场景驱动的：移动进程被用来表示移动计算设备（即不可复制的设备，如笔记本电脑、PDA和1本研究由丹麦研究机构资助，资助编号：274-06-0415（CosmoBiz），编号：272-05-0258（移动安全）和编号：2059-03-0031（BPL）。2 程序设计、逻辑和语义组。3 计算逻辑和算法组。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.09.01124M. Bundgaard等人/理论计算机科学电子笔记194（2007）23智能卡）以及移动计算（即，可复制的软件代理和迁移过程）。嵌套的显式位置通常用于表示管理域、防火墙、移动设备的物理边界、软件消息的边界以及诸如加密、沙箱和存储器中的数据的位置之类的过程。 最后，本地名称用于表示私钥和对内存中位置的引用范围。在本文中，我们认为，移动计算硬件设备本质上是线性的，而软件中的移动计算本质上是非线性的：硬件设备不容易被复制，系统的安全性往往取决于这一事实，例如智能卡。因此，软件通常必须被明确地保护以防止复制，例如，通过将其封装在防篡改（并且不可复制）的硬件设备中。Mobile Ambients演算及其后代组合了线性移动过程（环境）和非线性可复制消息（值）。这些功能使演算适合移动计算建模。但是，由于没有一个演算允许在环境中进行一般的复制，因此很难表示可复制的移动计算。另一方面，最近的高阶过程演算，如Seal演算[11]和Homer [15]，已经在嵌套位置的上下文中引入了可复制的移动资源。但是，通过假设所有资源都是可复制的，这些演算作为不可复制的移动计算设备的模型有点令人惊讶的是，我们没有发现微积分结合线性和非线性移动嵌入式进程和本地名称。在本文中，我们因此提出了一个扩展，灵感来自于一个直觉线性逻辑，类型和效果系统的荷马在[13]中提出。扩展允许我们区分变量的线性和非线性使用（如线性lambda演算），并输入位置的名称（类似于引用类型），从而将位置的内容限制为线性或非线性。我们将非线性定义为非线性线性的一个子类型，它使非线性（软件）位置能够嵌入线性（硬件）位置。这也确保了非线性资源可以被用作线性资源。另一方面，类型系统保证线性资源永远不会被复制或嵌入到非线性资源中：如果线性资源可以嵌入到非线性资源中，则可以通过复制嵌入资源来复制它。在Homer中，可以使用复合位置路径引用嵌套资源。为了输入这些路径，我们引入了复合引用类型，保证了非线性位置中的线性位置永远不会被引用。我们声称，演算捕捉到了移动计算硬件设备和软件过程的内在可复制性特征，如上所述。我们证明这一主张，在第二节。5一个简单的电子现金系统的例子，其安全性取决于智能卡和ATM本身的不可复制性同样，软件过程的可复制性，在这种情况下加密的消息，构成了一个重要的安全威胁。我们并不认为这个例子证明了一个现实的智能卡系统的安全性，但它表明，一个现实的模型，M. Bundgaard等人/理论计算机科学电子笔记194（2007）2325移动计算和计算应允许线性和非线性移动过程。类型系统对无限行为的处理有影响。在大多数（无类型）高阶演算（HOπ[19]，λ-演算，CHOCS [23]，Homer [15]）中，可以通过进程传递（和进程复制）来编码有限行为。诸如Y-组合子、复制或一般递归之类的构造函数不是作为原语，而是作为派生构造。然而，Homer [15]中递归的编码依赖于复制资源的能力因此，我们只能对非线性资源的递归（以及复制）进行由于复制对于线性资源确实有意义，允许任意数量的相同资源可用，因此我们将其作为微积分中的原始构造函数引入。在全文[7]中，我们通过提供倒钩互模拟同余，弱和强标记互模拟，将[15]中的工作扩展到线性和非线性类型演算，并证明Howe的方法扩展到这种更丰富的类型设置，从而为线性和非线性移动嵌入式资源的上下文推理提供了一种技术。我们表明，标记的互模拟同余是健全的倒钩互模拟同余，并在强的情况下也是完整的。本文的结构如下。节中2我们提出了荷马演算，并在SEC。3.给出了转换语义。荷马的类型系统在第二节中介绍。4，我们在第二节中提供了智能卡的例子。五、节中6、总结并提出今后的工作。相关工作线性和非线性之间的相互作用已经在直觉主义线性逻辑的变体和相应的指称模型、项模型和子结构类型系统中得到了深入的研究模型和类型系统已经被用来描述和推理函数编程中共存的线性和非线性资源，例如内存管理和对系统资源的引用[24]，在最近的量子计算语言中使用经典控制[22]，以及在π演算中控制名称的使用（以及移动性）[17]。我们没有发现以前的研究线性和非线性移动过程相结合的嵌套位置和本地名称。Homer演算扩展了Plain CHOCS，但与最近的移动性演算（如Seal演算[11]，M演算[20]及其最近的继任者Kell演算[21]）共享思想，特别是表示嵌套命名位置中的可复制（非线性），客观移动匿名资源的能力类型系统已经为M演算（和Kell演算[3]）引入，以确保位置名称的统一性（用于确定性路由）。Seal演算的类型系统在[11]中给出，类型系统既类型活动进程又类型位置，从而使人们能够声明可以进入和退出位置的进程的类型。Homer中的复合地址路径在某些方面类似于com-26M. Bundgaard等人/理论计算机科学电子笔记194（2007）23在具有多元同步的π演算中发现的相反通道名称[9]。在[8]在Milner的多进π -演算型系统的基础上，给出了多进同步的一个型系统也有人建议使用复合通道中的第一个（或最后一个）元素的类型来键入复合通道名称，但这种想法并没有实现。Kobayashi等人在π演算[17，16]中对线性类型进行了详细的研究。最近Berger，Honda和Yoshida [1，2]研究了序列函数计算和类型π演算之间的联系。 对于高阶π-演算，Yoshida和Hennessy [27，26]研究了一个类型系统，该系统通过为每个进程键入一个描述进程可以访问的资源的接口来捕获移动进程的结果。线性和非线性资源类型系统的第一个版本在[12]中提出，用于移动资源的微积分[14]，荷马的前身，但理论从未发展。Homer最初在[15]中提出，同时采用了Howe文[13]中的结果得到了推广，证明了早输入强互模拟同余是倒钩互模拟同余的一个可靠而完整的刻画。Homer也在双图的设置中进行了研究[5]，并且在π演算的编码中研究了其表达性[6]。2荷马在本节中，我们介绍荷马的句法[13]与[14]的唯一区别是我们用复制扩展了语法。我们对N个字符串中的名称进行了定义，并将其命名为N个字符串在有限的集合的名称范围。我们让δ在名称的非空有限序列上的范围，称为路径，并让δ表示共路径。路径和协同路径用于引用任意深度嵌套的资源。我们让δ和δ的范围，并定义δ=δ。我们假设一组无限的过程变量V，其范围为x和y。过程表达式的集合p的范围为p，抽象的集合a的范围为由a，和c的由c排列的具体化由语法定义：p：：= 0|X|埃莱|ppJ|（n）p|！p， e：：= a|b、将所述第一a：：=（x）p，b：：=pJ：np， c：：=b|（n）c，其中，b的范围是不受限制的结核。我们让t表示集合p∈a∈c。当e表示抽象时，我们让e表示具体，反之亦然。具体化中的进程pJ直观地说，这组名称可以被认为是由资源分配的名称。注释用于在移动资源时控制动态范围扩展。之所以需要注释，是因为可以定义一个上下文来测试名称在移动资源中是否空闲。如果没有注释，任何两个进程在其M. Bundgaard等人/理论计算机科学电子笔记194（2007）2327X计算将是可区分的（关于这个问题及其解决方案的完整描述，请参见[13，15]）。在SEC中提出的类型系统。4保证了这个集合包含了进程pJ中出现的所有名字。进程构造函数是并发进程演算中的标准构造函数：非活动进程，0，进程变量，x，动作前缀，parallel composition，parallel composition，n，p，（n）p中的名称n的限制，以及p的复制，！p. Homer被定义为高阶微积分的简单扩展Plain CHOCS [23]允许活动进程位于命名位置，由以下形式的前缀表示：nnpJ：nn位置名为n，并将其替换为q中的变量x。当活动进程被移动时，位置消失（如在Seal中），剩余进程被激活。这两个前缀补充了被动过程的常用前缀pas inginCHOCSdenndbynnpJ：nnnpandn（x）q. 通过检查和分析，我们发现，在预处理器中的过程pJ：n中，对于一个简单的处理器，可能会出现如下情况，即过程p j：n中的过程p j：n与CHOCS中的过程p相同，既不能与其他过程反应也不能与其他过程交互。相互作用通过使用名称路径来获得嵌入式资源，从而允许进程将另一进程传递到（或移动）任意深度嵌套的活动嵌入式资源。例如，我们有缩减（忽略类型注释）n<$m（x）q<$$> nm<$p <$pJ−→n<$q[p/]<$<$pJ（1）和nnm（x）q−→nq[p/]、（2）其中nm是由名称n后跟名称m组成的名称路径。像往常一样，（x）绑定变量x，（n）绑定名称n。定义了t的自由名和束缚名（fn（t）和bn（t））以及t的变量（fv（t）和bv（t））的概念，并给出了简单的表达式：fnn（npJ：nnp）=nnf n（p），即. 该注释确定资源的自由名称。我们将一个没有自由变量的过程称为闭的，并让tc和pc分别表示闭项和过程的类。我们将在整篇论文中考虑直到α-等价的项，我们将把项和过程的α-等价类的集合分别记为t/α和p/α我们也将这个概念扩展到封闭过程和项的集合。我们使用标准的简写，并且经常在一个过程中省略0我不知道你在说什么。对于n个元素的集合，n={n1， . . ，nk}我们将为（n1）···（nk）t写出（n2）t。我们也将n写为单例集{n}，方便时，让δ和δ表示路径中的名称集合。对于任何两个集合s和sj，我们将将s和sJ的并集写成ss j，假设s sJ=。我们说过程上的关系R是一个同余，如果0R0和x R x，p R pJ和q R qJ蕴涵pp R qj：nppJ。我们定义了一个关于p/α的等式，它是一个同余式，并且满足（π，0）的（通常）幺半群规则和π演算的范围扩展。我们像往常一样定义抽象和具体之间的应用，只是替换更新了位置上的类型注释。X28M. Bundgaard等人/理论计算机科学电子笔记194（2007）23p[xc=（m）（p[p），x第二章. 1（应用和替代）对于c=（m）np：npJ当n（pJJ）=n时，我们定义了一个简单的函数a=（x）pJJ，c·a=（m）（pjJJp：n/]）andda·JJp：n/]J其中，在PJJ[p：n/x]中的变量的值在pjJ的结构中通常被定义为是可导的，除了在具体化的情况下，如果变量在子资源中显示为自由，则更新子资源的注释。也就是说，如果x∈fv（q），则n（<$q：m<$j<$qJ ）[p ： n<$/x] =<$q[p ：n<$/x] ： m<$j<$n<$$>qJ[p ： n<$/x] 。Ifx/∈fv （ q ） 则 （ <$q ： m<$j<$qJ ） [p ：n<$/x]=<$q：m<$J<$qJ[p：n<$/x]。请注意，当到达一个变量时，替换会丢弃该类型（请参阅应用程序A以获得应用和替换的完整定义3变迁语义学在本节中，我们为Homer提供了一个带标签的转换语义。与上一节一样，与[13]的唯一区别是我们用复制规则扩展了我们让π在标签集上的范围，定义为π：：= τ|（回忆|δ）。在π中，f n（π）是f n（δ），其中π=δ或π=δ′，而δ ′不是π。表1中的规则定义了一个带标号的变迁系统（tc/α，−→<$pc/α×<$×tc/α）.为了更简洁地表示嵌套活动资源的转换，我们关闭了流程操作符下的具体化和抽象化因此，我们认为，当n everc=（n）p1：n1panda susummingn（f n（pJ）<$n<$δ）=（usingsinging gα-conversionifneeded）wel et catch j den ote（n n）n n n（ppJ），welet（n）cdenote（n n）p 1：n 1 p，如果n ∈ n 1，并且其他wiseiten otes（n n）p 1：n 1（n）p，并且welet δc：n jpJdenot e（n n）p1 ：n 1 δp：nN.同样地，当n∈a=（x）p，且假设x/∈fv（PJ）（如果需要，可使用α-转换）时，我们设a∈PJ表示（x）（p∈PJ），（n）a表示（x）（n）p，且我们设δ∈a：n∈PJdenot e（x）δ∈p：n∈PJ。 这些shorter和s是在规则（nesting）、（rest）、（par）、（par J）和（repl1）中定义的。这些规则保守地扩展了普通CHOCS的规则。请注意，规则（同步）涵盖了两种不同类型的交互：如前一节所述的主动和被动资源移动，并且规则（嵌套）允许移动任意深度嵌套的主动资源，接收资源并执行内部计算步骤。为了允许这三种操作，我们使用操作δ·（）来扩展位置路径，定义为：δ·τ = τ，δ·δJ= δδJ。注意，该运算不针对δ定义，因为δ是“向下”的M. Bundgaard等人/理论计算机科学电子笔记194（2007）2329XXp：np：npp：np：np：np ：np：np：np：np ：n（prefix）e−→eϕπ（嵌套）p−→tδp：npJ−δ→·πδt：npJ（休息）p−π→t（n）p−π→（n）tp−π→t（n/∈fn（π））（同步）p−n→ejp−→e<$（面值） pp−→ t pJπJ（parp<$pJ−→τe·e<$pJ−π→tpp−→ p tJπ（回复1）p−π→t！p−π→tπ！（回复2）p−n→ap−n→c！p−→τ （a·c）！p表1过渡规则。因此在资源外部不可见由于δ·τ=τ，嵌套规则意味着δp：npJ−→τδt：npJ，ifp−→τt。作为使用规则（以及具体化和抽象化的简写）的示例，在从m（x）q-m→（x）q导出的预处理中，所以n−n→mtain（x）nq：nq。 Combiningwi thn mp：njpJ−n→mp：nnm（x）q：nnmJpJ−→τ（x）nq：n·吉吉ByDef. 二、1we get（x）nq：n·p：njpJ=nq[p：nJ/]：nnJpJ（ifx∈fv（q））.对于这一结果，我们可以用一个简单的方法来处理（2），我们有一个mp：njpJ−m→mp：njpJ，sonm吉吉JJ−n→m ⟨金河jj当hnm（x）q−n→m时，（x）q，我们得到nm吉吉Jjnm（x）q−→τ金河JJ·（x）q，如果我是Def。二、1是procesnpJ：nJjq[p：nJ/]。4类型系统我们现在准备提出在[13]中为荷马给出的类型和输出系统的扩展，以允许在线性和非线性资源之间进行区分我们将假设一个集合S={aff，un}，是一个无限制的集合（即，非线性）排序，并让S在排序范围内此外，我们将假设子类型重新-lation≤ onS使得unaff，这与我们的直觉相一致，即可以用一个无限制过程来代替一个无限制过程。<或者具体地说，正如SEC中的电子现金系统模型所体现的那样软件可以嵌入到硬件中并用作硬件，但不能反过来。.30M. Bundgaard等人/理论计算机科学电子笔记194（2007）23PROCESTYPESCNS是两个WPARTSW RI T TNA SNSNS 第一次，第二次，S，Rerdsifh e pocessisaprone e linearornon-linear. 这是一个很好的例子M. Bundgaard等人/理论计算机科学电子笔记194（2007）2331由类型系统在[13]中引入，并且可以被视为捕获进程使用或分配的名称的对象二、类型系统保证这个集合是进程中自由名称的超集。除了过程类型，我们还定义了具体和抽象类型。结核类型BUSINESSJINESS是一种概念性（概念性）概念：概念性概念性最佳类型SDSJnt类型是一种在SJ N T和Sj n de e之间进行访问时的最佳操作（x）p一个S类过程。 我们将只考虑抽象和具体类型，S≤SJ，这是由类型规则保证的。定义4.1（类型）我们定义了三种类型，处理类型Tp，具体类型Tc和抽象类型Ta，语法如下：T：：= T p|T c|不是Tp：：=Sn，Tc：：=STp，Ta：：=SDTp对于n/∈新的写作（SnthepeSnnandd（SSJn）nforthehecóncretionty pérés pérésján. 我们将TnJ定义为T类型的一个（不一定（Sn）n jJ=SnnJJ（STp）njJ=STpnJJ（SDTp）<$n<$JJ=SDTp<$n<$JJ。类型环境Γ将排序分配给名称和变量。定义4.2（类型环境）类型环境Γ是从名称和变量到排序的部分函数Γ：NV-S。我们将分别为定义域中的名称和变量写dom n（Γ）和dom v（Γ），并设dom（Γ）=dom n（Γ）≠dom v（Γ）。如果n/∈dom n（Γ），我们记为Γ，n：S，表示从n到S的映射的Γ的扩张，对于变量也是如此。我们将让Δ在没有变量映射的环境中变化。为了展示我们的类型规则，我们需要能够以一种方式组合两个环境，就像线性类型系统一样，约束线性使用的变量的存在。让l在名称和变量上都有范围，我们定义了偏两个类型环境Γ和Γ j的组合Γ JJ，表示为Γ Γ J= Γ JJ，通过ΓΓ J，如果{x| Γ（x）=aff}<${xJ|如果l∈dom（r），则dom（r J）蕴涵r（l）= r J（l），否则组合是unfined。这些要求强制执行，对于Γ ΓJ= ΓJJ，任何出现在ΓJJ中的名称都可以出现在Γ、ΓJ或两者中（如果它具有相同的排序）。对于无限制变量也是同样的情况，而同一个线性变量不可能同时出现在Γ和ΓJ中。这强调了，我们的类型系统关注的是进程的线性使用，而不是名称，因为在[17]中。我们还需要输入地址路径：如规则所定义的，32M. Bundgaard等人/理论计算机科学电子笔记194（2007）23Γ，n：SRefSJJJJΓ，n：Sn：SRefSΓ，n：S<$δn：SJJ（S≤S）参考S参考SJJ（变量）Γ， x：Sx：Sn （n）（r）（inactive） 0：unn（nn（Γ））（paralllel）rp：Sn联系我们J JJΓⓈΓ►pǁp:Sn˜∪n˜JJJ（剩余）Γ，n：Sp：Tp nT_p（n）：T_p（静置浓度）Γ， n：S（m）p：mnnJ：TnpCJΓ（mn）p：mnnp：Tc（embed）p：unn联系我们（重复）T_p：T你好！p：Tpp（x ∈ fv（p）. r（x）= un）（绝对值）Γ， x：SJp：SnΓ（x）p：SDSnJ（SJ≤S）（conc）rp：SnrJpJ：SJnJΓⓈΓ►⟨p:n˜⟩p:⟨S⟩Sn˜∪n˜JJJJ（S≤SJ）（ABS前）Γa：SJDSnΓ：SJJRefSJ中文（简体）（S≤S）JJ（浓度前）Γ►b:⟨SJ⟩Sn˜Γ►ϕ:SJJRefSJΓ►ϕb:Sn˜∪ϕ（S≤S）JJ表2键入地址路径。表3线性和非线性荷马的分类规则表2中类型SRefSJ被读取为经由S到 SJ的引用。 这些规则确保地址路径类型为SRefSJ的名称的排序形成非严格的降序链，从而确保在不受限制的资源，并且地址路径的第一个名称排序为S，路径的最后一个名称排序为SJ。例如，令r =m：aff，n：un，我们可以导出r mm：aff Refaff和r mmn：aff Ref un，但我们既不能导出r nm：un Refaff也不能导出rmnm：affRef aff。我们使用表3中的规则定义过程、抽象和具体的类型。该类型系统保守地推广了Homer [13]的先验类型（嵌入）系统，我们可以通过删除（嵌入）规则并将S视为单例集来获得，从而可以删除抽象和具体类型中对排序的所有引用，并完全删除副条件和环境。我们只解释了一些规则，其余的应该是不言自明的。（conc）规则允许我们输入一个基本的凝结，如果挤压过程有一个剩余过程的子排序。我们可以用（abs）来输入一个抽象，如果我们可以输入在一个扩展环境下的抽象体，其中x是抽象体排序的规则（pre-abs）允许我们形成一个过程M. Bundgaard等人/理论计算机科学电子笔记194（2007）2333只要接收到的进程的排序是抽象从地址路径期望的排序，就可以从抽象中提取。规则（embed）对应于具有子类型的类型系统中的通常包含规则，具体地说，它允许我们将不受限制的进程视为一个子类型进程。规则（repl）中的边条件确保了所有在p中自由出现的变量都是不受限制的，然而，Γ可能包含一个在p中不自由出现的随机变量。进程的类型化规则使用路径类型来确保资源提供者和接收者就所传递的内容达成一致，结合引用类型的思想，约束引用资源的类型，进程演算的类型，它约束在通道上通信的对象的类型。因此，对于类型化的地址路径r_ref：S_Ref_S_J，资源提供者和接收者都同意所通信的进程具有排序S_J（这约束可以通过提供者部分的包含和接收者部分的缩小来削弱）。路径类型中地址路径的最外层名称的排序S用于规则（pre-conc）和（pre-abs）的副条件中，以确保任何使用路径的进程都具有S的超排序，这意味着在不受限制的资源内的路径中永远不会出现一个新的名称。例如，如果n是一个整数，而m是一个整数，则在过程ssnmp：nnjq：Snn中，该整数是不受限制的，但类型规则强制S = aff，这意味着整个进程被类型化为一个进程。这是对线性资源的有限使用，但它很适合包含非线性移动计算的线性移动计算设备的场景：移动计算设备永远不能包含在软件进程中或由软件进程操纵。我们已经通过消除规则（嵌入）并遵循线性类型系统的方法实现了一个类型算法[25]。类型化算法要求我们用排序来注释名称限制，因为我们不能从限制中推断出正确的排序。参见该算法的全文[7]。我们可以证明关于类型系统的标准性质：未使用的名称和变量的加强，结构同余下的不变性等。同样，我们参考了全文[7]，这里只给出主要结果。正如在一个有子类型的类型系统中所期望的那样，我们有变量的收缩。命题4.3（变量的收缩）如果Γ，x：S≠t：T且SJ≤S，则r，x：S，t：T。请注意，我们通常不能对名称使用窄化（或加宽），因为这可能会使地址路径成为非类型的，即如果我们允许更改名称的类型，则可能会破坏顺序。Le mma4. 4 （ 子 结 构 ） Let Δp ： Snbeaclosedprocssande tr rJ ， x ： StJ ：TJbeatrmwithΔ r j定义t hnΔrjtJ[p：n/x] ：TJJ，其中TJJ= Tjn如果x∈fv（tJ）且TJJ=TJ其他rw是e。我们的类型系统确保了良好类型的术语满足几个属性，下面我们陈述主要属性。这些属性意味着资源的注释包含资源的自由名称，不受限制的术语中不能包含一个不受限制的术语，并且不受限制的术语不能被复制。34M. Bundgaard等人/理论计算机科学电子笔记194（2007）23jJ J JJK引理4.5（良型项的性质）将n（T）写为类型T的名称，s（T）定义为sn+ s n+ s，如果T是mSn+ s，SJDSn+s，或SJdSn+ s。我想：那么• fn（t）n（T）domn（r）和fv（t）domv（r）。• 如果x：aff∈ Γ，则x在t中至多出现一次自由。• 若x：aff∈ Γ且x∈fv（t），则s（T）= aff.• 如果s（T）= un，则对于每个子导子Γ J<$tJ：TJ，我们有s（TJ）= un。定理4.6（主语归约，标号转移关系）设p：Sn=0且p−π→t在下面的等式中成立。• π=τ，t=pJ，且r∈pJ：Sn∈。• π=π，t=a，且Γ_a：SJDSn<$SJJ≤S.和Γ：SJJRefSJ，对于某个SJ，• π=π，t=c和Γπc：πSJ∈S n，Γ π c：S j ∈ S n，Γ π c：SJ∈SJ，S j ∈SJ≤S。5电子现金智能卡应用在本节中，我们将提供一个简单的电子现金系统模型，说明线性和非线性移动资源、嵌套位置和本地名称的组合。首先考虑一个定义为crypte，k= e（x）ekx：crypt：{k}.该进程能够接收名为e的资源，然后将其放置在名为k的位置中，该位置嵌套在名为e的位置中。如果k是加密密钥，则可以认为该过程能够对在公共信道e上通信的过程（或消息）执行单个加密。这可以用在由能够提供硬币c= 0：n的ATM组成的简单电子现金系统中，如果位置v中的过程可以用私钥k加密随机数n：.Σatm=（k）v=crypte，k：{e，k}=cashk.Σ现金k=！（n）ven 0：：{n}vekn（x）c0：。在控制过程中，ATM的现金k被发送到位置v中的过程内部的位置e。随后，从子位置vekn检索进程。如果成功了，那么一定是位置v内的进程在位置k中嵌入了随机数，然后ATM发出一枚硬币。因此，我们得到以下转换在m−→τ−→τ.（k）（n）（vekn 0：：{n}：{k，n}：{e，k，n}veknJ（x）c0：）（k）（pM. Bundgaard等人/理论计算机科学电子笔记194（2007）2335其中，p=def（nJ）（v_e_k_k_j_0：{nJ}_k：{k，nJ}_k：{e，k，nJ}_k）是包含“使用过的”智能卡的插槽控制过程可以潜在地执行任意次数。然而，预期的行为是，只有一个硬币将被交付，因为卡上的方法只能加密一次。唉，如果槽v中的进程可以被复制，那么安全性就被破坏了。电子现金复制窃贼可以定义为：thief=v（x）（vx：vx：），其通过v（x）拾取电子现金过程并创建两个副本。然后（再次让p=def（nJ）（vek 0：{nJ}：{k，nJ}：{e，k，nJ}））安全性将崩溃τ。ΣATM机窃贼−→（k）vcrypte，k：{e，k}vcrypte，k：{e，k}cashk−→τ∗≡ （k）（ppcashk）c 0：c0：。在上一节中给出的类型系统允许我们将位置v作为一个双线性类型。 因此，我们可以将位置v中的进程建模为嵌入在不可复制的智能卡中（并且还确保整个系统也不能被复制 首先，我们证明系统是良好类型的。引理5.1设Δ = e：un，c：aff，v：aff，则Δ atm：aff {e，c，v}.然后，我们表明，如果槽v是线性的，则我们不能键入系统atm窃贼，因为这使得不可能复制槽的内容，即。智能卡。第五点。2对于yΔ， v：af f，nΔ， v：af f，n Δ，m=f：SnΔ。和排序S，它是不可能得到的证明（略）假设可以通过给定的条件导出Δ，v：aff f f， x：afff fQ请注意，加密的随机数是不受限制的。如果我们重复使用相同的秘密名称n作为卡的挑战，安全性将被破坏。交换-ping本地名称（n. ）和控制过程定义中的复制将现金k定义为（n）！ ven 0：：{n}vekn（x）c0：，一个小偷，在姓名n被发送（并在卡上被加密）之后，ATM复制卡的加密内容，可以定义为：小偷J=ve（x）（vex：：{e}ve（xJ）vex：：{e}），其中，并行组合的右手侧接收并丢弃ATM第二次发送的询问消息，并向卡提供36M. Bundgaard等人/理论计算机科学电子笔记194（2007）23}复制的加密内容。让.Σp=def！ ven 0：：{n}vekn（x）c0：，Q=defvek 0：{n}：{k，n}：{e，k，n}，以及qJ=defvekn 0：：{n}：{k，n}：{e，k，n}我们有以下过渡在m处，fJ−→τ−→τ∗≡ {k, n. v0：{e，k，n}vekn（x）c0：pqjve（xJ）qj- 是的Σ{k，n}vc这种安全威胁不会在纯粹的线性演算中表现出来。我们将在未来的工作中应用[7]中提出的互模拟同余来证明类型化atm在任何上下文中确实是安全的。6结论和今后的工作我们已经成功地扩展了Homer的先验类型和结果系统，以提供第一个将线性和非线性嵌套移动嵌入过程与本地名称相结合的过程演算。通过一个具体的电子现金智能卡系统，我们已经举例说明了微积分捕获移动计算硬件和嵌入式移动软件计算之间的差异，这对于普适和无处不在的计算的安全性至关重要我们相信，在本文中为荷马提出的类型系统可以适用于其他演算结合移动嵌入式资源与本地名称，例如移动环境和密封演算。我们希望调查其他的变化和应用程序的线性类型和更具表现力的类型系统荷马在移动安全和计算机支持的移动自适应业务流程（CosmoBiz）的研究项目，在IT大学的Copen的。引用[1] 伯杰，M.，K. Honda和N. Yoshida，Sequentiality and the π-calculus，in：S. Abramsky，编辑，第五届类型化Lambda演算和应用国际会议论文集（TLCA29比45[2] 伯杰，M.，K. Honda和N. Yoshida，Genericity and the π-calculus，Acta Informatica42（2005），pp.83-141[3] 比丁格山口和J。-B. Kell演算：操作语义和类型系统，E。Najm，联 合Nestmann 和P. Stevens， 编辑 ， 第 五届 IFIP基 于对 象的 分 布式 系 统形 式化 方 法国 际 会议 论文 集（FMOODS109-123[4] Bugliesi ， M. ， G. Castagna 和 S. Crafa ， Access control for mobile agents ： The calculus of boxedambients，ACM Transactions on Programming Languages and Systems（TOPLAS）26（2004），pp.57比124M. Bundgaard等人/理论计算机科学电子笔记194（2007）2337[5] Bundgaard，M.和T.Hildebrandt，具有hlocaln ames的高阶移动嵌入式资源的双图语义，in：A.Re nsi nk，R.他是一个很好的人。 Ko�nig，editor s，验证和并发研讨会的Graph转换的程序设计（GT-VC'05），电子注释Theoretical Computer Science154（2006），pp. 7比29[6] Bundgaard，M.，T. Hildebrandt和J.C. Godskesen，A CPS encoding of name-passing in higher-ordermobile embedded resources，Theoretical Computer Science356（2006），pp. 422-439.[7] Bundgaard ， M. ， T. Hildebrandt 和 J.C. Godskesen， Typing linear and non-linear higher-ordermobile embedded resources with local names，Technical Report TR-2007-97，IT University ofCopenhagen（2007），可从www.example.com获得http://www.itu.dk/~mikkelbu/typedHomer.pdf。[8] Carbone，M.，“信任和流动性，”博士。Thesis，BRICS（2005）.[9] Carbone，M.和S. Ma Joueis，关于π-演算中多进同步的表达能力，Nordic Journal of Computing10（2003），pp. 70比98[10] 卡尔代利湖和A.D. Gordon，Mobile Ambients，Theoretical Computer Science240（2000），pp.177-213[11]Castagna，G.，J. Vitek和F.Z. Nardelli，The Seal calculus，Journal of Information and Computation201（2005），pp. 1-54[12] Godskesen，J. C.和T.刘文，移动计算资源的可复制性类型（2004），在形式化方法与安全国际研讨会上发表，南京，中国。[13] Godskesen，J. C.和T. Hildebrandt，将Howe的方法扩展140-151[14] Godskesen，J.C.，T. Hildebrandt和V.Sassone，移动资源的演算，在：L。Brim，P. Jancar，M. 我知道你很聪明。 Kucera，editors，prooceedingingsofthe13thiiintérnatitionalCocurrenceceonCocurrencycyTheory（CONCUR'0 2 ） ，Le c t u r e N o t e s in C o m p u t e r S c i e n c e 2 4 2 1 （ 2 0 0 2 ） ， pp . 272-287。[15] 希尔德布兰特，T.，J. C. Godskesen和M.Bundgaard，Homer的互模拟同余-高阶移动嵌入式资源的演算，技术报告TR-2004-52，哥本哈根IT大学[16] Kobayashi，N.，Type systems for concurrent programs（2002），inProceedings of UNU/IIST 10thAnniversary Colloquium.[17] Kobayashi，N.，B. C. Pierce和D. N. Turner，Linearity and the pi-calculus，ACM Transactions onProgramming Languages and Systems（TOPLAS）21（1999），pp. 914-947[18] Levi，F.和D. Sangiorgi，Mobile safe ambients，ACM Transactions on Programming Languages andSystems（TOPLAS