加权时间自动机：网络安全属性模型检验与定时释放密码

理论计算机科学电子笔记99（2004）229-243www.elsevier.com/locate/entcs网络上时间锁定秘密安全释放的模型检验1Salvatore La Torre1Aniello Murano1， 2Mimmo Parente11Universtit`adegliStudidi iSalerno，84041Baronissi（SA），Itally.2希伯来大学，耶路撒冷91904，以色列。{slatorre，murano，parante}@ unisa.it摘要加权时间自动机扩展了时间自动机的位置和转换成本。这使我们能够将定量测量与运行相关联，因此可以在此模型上研究与系统设计实际相关的几个问题（最优可达性，最优控制等）。在本文中，我们认为，加权时间自动机是合适的模型，研究一些安全性质。特别是，我们描述了一个场景，我们希望通过计算机网络发送消息，并希望使用足够的密码学来确保消息的保密性，直到一定的时间期限。我们假设，入侵者试图解密的消息只能使用本地的资源（计算能力）的消息访问的节点：我们给出的证据，这一假设的基础上介绍的场景Rivest，沙米尔和瓦格纳。 节点的计算能力以每次操作的次数表示单位我们展示了如何通过加权时间自动机很好地捕获这种设置，其中：底层时间自动机对网络的特征进行建模，位置上的权重表示每个节点的计算能力。因此，我们可以使用模型检查技术来建立所需的安全属性。保留字：模型检验，加权时间自动机，定时释放密码1介绍在定时释放密码[12]中，消息M以这样的方式加密，即没有人（除了发起者）可以解密它，直到经过所需的时间量Θ。只有在时间Θ之后，消息M才是可用的，并且任何人都可以阅读它。是选择一个1本工作是由MURST在其出版物“MetodiForormaliperer laSicurezzaedilTempo“（ME FISTO）的第一篇文章中提出的。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.010230S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-对称密钥，也就是说，加密和解密消息使用同一个密钥。通常，密钥是一个在加密阶段很容易计算的函数（一旦知道了一个大的合数N的因式分解）。在解密阶段，每个人都只能在经过预定量的时间θ之后才能解密消息（除非成功地对N进行因式分解）。时间Θ可以由消息的发起者选择如下：令sq是基本的计算机操作（模N的平方操作），并且令tsq是目的地机器执行sq所需的时间，则Θ =tsq·k，其中k是发起者选择的正整数。由于这个基本操作本质上是顺序的，因此可以通过简单地给出要执行的平方操作的数量k来正如[12]中所报道的，定时发布加密的可能应用有很多：例如，可以在给定的截止日期后打开投标的拍卖，必须在每个月初完成的付款，等等（参见[6]，其他示例）。在本文中，我们分析了自然的情况下，定时释放密码是用在一个消息，必须通过一个网络的计算机，ers之前被交付到目的地。因此，发送方（Alice）不能仅依赖于接收方（Bob）可以执行sq的速度，如[12]中所述，而是还必须考虑扮演广告角色的网络的遍历节点。她的目标是尽可能多地在M该场景在图1中继续，其中边缘被标记有指示消息可以穿过该边缘所花费的最小和最大时间的间隔，并且节点被标记有指示消息在被转发到相邻节点2之前可以在其中被处理的最小和最大时间的间隔。现在假设Alice选择了k=J，则需要的sq操作的数量计算密钥，并使用该密钥对M进行设CM（k）为周期数.她想知道哪些是她向网络注入CM（k）的保证。 更准确地说，令CM（k）是使用定时释放密码，使得需要J平方模N运算来解密它，在本文中，我们解决以下决策问题：安全问题：给定一个不安全的计算机网络G，[2]虽然对于大型网络（例如互联网）来说，很难收集到有关网络的信息，但我们可以合理地假设，对于某些公司使用的专用网络来说，这些信息也是有用的。S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-231[第1、 2项][0，2]中的值年q1[1，3][0，1]年q3[4、 8]一[3、 5][1、 2][0、 2]B[1、5]Q2[二、三][第1、2项]年q4[0， 3]中的值Fig. 1. 一种网络，其边缘具有延迟时间，节点具有处理时间。A和目的地B，时间期限θ <Θ min和时间间隔[Θ min，Θ max]，CM（k）是否可以从A发送到B，使得它在时间Θ之前不能被破译，并且B可以在间隔[Θ min，Θ max]内的某个稍后时间读取M？我们建议在加权的框架内重新表述我们的安全问题，时间自动机，然后使用模型检查技术解决它在[2]中引入了时间自动机来建模实时系统，即与物理过程交互的系统，其正确行为关键取决于实时考虑。时间自动机是一个用有限个实值时钟集合扩充的有限自动机。根据当前位置和当前时钟值启用转换。 在在一次跃迁中，时钟可以瞬间复位，时钟的值正好是自上次复位以来所经过的时间。加权时间自动机通过将权重（不同的成本）与位置和转换相关联来扩展时间自动机。该模型在[3，5]3中被独立引入和研究，目的是为时间自动机提供性能他们的结局，位置的权重给出了每个时间单位停留在该位置，并且切换的权重是进行该离散转换的成本。因此，成本与每个运行相关联，作为两个加数的总和：所采取的开关的成本之和在每个位置花费的时间的成本之和。通过这种方式，每次运行都与时间的线性成本函数相关联，该函数考虑了访问的位置和所进行的转换。网络可以自然地建模为时间自动机，其中节点表示为位置，并且发送和接收消息的动作网络行为的时间特征（如传输延迟、延迟时间、处理时间等）可以通过时钟、重置和时钟约束来捕获。在这样的模型中，权重可以用于捕获每个节点的计算速度，即，平方运算3在[5]中，加权时间自动机被称为线性定价时间自动机。232S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-可以在特定位置执行的每个时间单元4。在这种情况下，安全问题可以重新表述为以下加权时间自动机上的决策问题。给定一个加权的时间自动机A和一个权重为w的目标位置T，对于在总时间tr≤Θ的T处结束的所有运行r，我们提出以下问题，其中Jr表示r的成本：• 如果tr= Θ，那么Jr是否小于Jr？• 是否存在t≥0使得t+tr∈[Θmin， Θmax]且w·t+Jr=Jr？我们把这个决策问题称为时间成本有界可达性问题（简称TBR问题）。显然，为了决定这个问题，确定在时间Θ内到达T的所有运行中到达T的最大和最小成本运行是足够的。 在本文中，我们给出了一个解决方案，包括减少这些问题的类似问题的加权（离散）有向图，然后使用标准算法来解决它们。该减少需要构造在参数Θ的长度和时钟变量的数量方面具有指数大小的图。如果我们使用Dijk-stra对于TBR问题，我们有一个平凡的下界，从可达的时间自动机是已知的P空间完全[2]。我们记得在[3]和[5]中独立地研究了加权时间自动机上的最小成本可达性问题。让我们注意到，这些论文中使用的方法并不直接适用于计算运行的最大成本。此外，同样对于运行的最小成本的计算，这里我们考虑更简单的设置（我们对我们考虑的运行的时间具有上限），并且即使这不允许实现决策算法的计算复杂度的显著改进，描述也要简单得多。文献[8]研究了无循环加权时间自动机的最小费用可达性和最小费用控制问题在[1]中，权重w可以与每个位置q相关联，使得w给出在q中花费的单位时间的成本。 在这样一个模型中，给定一个成本区间I和两个状态s和t，决策问题（持续时间有限的可达性）被解决。持续时间有界的可达性不同于时间成本有界的可达性，因为后者除了成本界限之外还具有时间界限作为参数最后，时间最优[4]在一般框架中，节点的计算速度可能取决于几个参数：执行任务的数量、资源分配等。在这里，我们假设我们对这些参数的期望值有一个准确的评估，从而对在网络的每个节点上执行平方运算的期望速度有一个准确的评估S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-233可达性，即到达给定目标位置的最短时间，首先在[7]中考虑。 在那篇论文中，作者讨论了时间自动机中时间延迟的上下界计算问题。最小时间可达性也在[11]中被考虑，相关的最小时间控制问题在[4]中被考虑。本文的其余部分组织如下。在第2节中，我们回顾了定时发布密码[12]中使用的主要思想，并陈述了我们的安全问题。在第3节中，我们回顾了加权时间自动机的定义，并介绍了我们的符号。我们对加权时间自动机的TBR问题的解决方案在第4节中给出。最后，在第5节中，我们给出了一些评论。2定时释放加密在本节中，我们回顾如何使用所谓的在第2.2节中，我们简要描述了我们设置中的问题2.1时间锁拼图时间锁谜题是一个计算问题（谜题），除非机器执行至少一定时间的计算，否则下面是Rivest等人如何创建实现定时释放加密的时间锁难题。Alice有一个给Bob的消息M，但她想在一段时间内加密M，也就是说，她不想Bob（或任何其他人）在时间θ过去之前解密消息。要执行此加密，她执行以下步骤：(i) 她生成一个合数N，计算为两个大素数p和q的乘积。除此之外，她还计算了欧拉函数Φ（N）=（p−1）（q−1）。(ii) 她计算出k= Θ·spBob，其中spBob是Bob每单位时间可以执行的模N(iii) 她随机选取a模N5并将M加密为CM（k）=M+a2k（modN）。这个操作是通过计算第一个e= 2k（mod Φ（N）），然后计算CM（k）=M+ae（modN）来高效地执行的(iv) 她将谜题（N，a，k，CM（k））发送给Bob，并删除所有创建的变量（如p和q）。5 为了实际目的，也可以使用a234S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-因此，谜题的创建和解决是基于对所选k的数字a2k的计算。所使用的方案是密钥加密/解密，并且密钥是数字a2k。 如果N的因式分解是已知的，那么这个数可以通过做O（log N）次乘法来有效地计算，否则计算2k的唯一方法是计算k次迭代平方，也就是说，每次平方只能在前一次平方的结果上执行。具体来说，我们必须计算函数F（0）= a20和F（i）=（F（i−1））2，其中0Jmax。4. 她计算出Θmin = Θ +（J-Jmax）/spBob和Θmax = Θ +（J-Jmin）/spBob.在本文的其余部分，我们将讨论自动执行上述步骤2的工具假设我们可以直接从上述方案确定Jmin和Jmax，则以下性质成立。命题2.1对于A的所有路径p，且完成时间tp≤ Θ，沿p的平方运算的总数小于J。命题2.2对于A的所有路径p在时间t p ≤ Θ min到达Bob的位置，要执行的剩余操作数可以在时间t j计算，使得t j + t p ∈ [Θ min，Θ max ]。观察到命题2.1确保没有人可以在时间Θ之前破译消息，并且命题2.2确保Bob可以在[Θmin， Θmax]内破译消息，3加权时间自动机在本节中，我们回顾了时间自动机和加权时间自动机的定义和表示法。一个时间自动机模拟一个实时系统。我们假设有一个中央（实值）时钟，模型可以使用有限的时钟变量（也称为简单的时钟）以及时间约束来检查时间要求的满足情况。每个时钟都可以被视为与中央时钟同步的计时码表，因此可以读取或设置为零（重置）：重置后，时钟自动重新启动。在每个自动机中，时间约束由时钟约束表示。设C是一组时钟，时钟约束集合包含：• x≤y+c，x≥y+c，x≤c且x≥c<$x，y∈C且对自然数c;• 其中δ，δ1，δ2∈θ（C）.因此，一个Clockin erp re tion是一个映射ν：C −→R+。我们不使用0来表示时钟解释，将每个时钟映射到0。如果ν是一个时钟解释，λ是一组时钟，d是一个实数，我们用ν+d表示时钟解释，它给出每个时钟x的值ν（x）+d，用236S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-++一λ（ν）与ν仅在时钟值上不同的时钟解释x∈λ，它赋0。特别地，我们将使用λ（ν+d）来表示时钟解释，如果x∈λ，则为时钟x赋值0，否则为ν（x）+d。定义3.1一个时间自动机A是一个元组（tuple，Q，Q0， C，inv），其中：• [001 pdf 1st-31 files]是一组有限的符号（字母表）;• Q是位置的有限集合;• Q0<$Q是初始位置的集合;• C是n个时钟变量的有限集合;• 是Q ×n× n（C）×2C× Q（边）的有限子集;• inv：Q −→q（C）将每个位置q映射到其不变量inv（q）。边沿上的时钟约束称为保护。时间自动机A的一个状态是一对<$q，ν<$，其中q∈Q，ν∈Rn。 初始状态是一对，其中q0∈Q0是初始位置。 时间自动机的语义由状态集上的转换系统给出。该系统的变迁分为离散步和时间步。一离散步骤是σJJ其中（q，σ，δ，λ，qJ）∈θ，ν满足δ，νJ=q，νλ（v），且νJ满足inv（qJ）。 时间步长是其中νJ=ν+d，q，νd≥0，且对所有0≤DJ≤d，v+dj满足inv（q）。台阶σ，dJ J当req，ν−→d时q，ν当νJJ∈ Rn时，则是由εq，νJJ∈σ→εqJ，νJ∈σ。字母表上的时间序列（σ，τ）使得σ∈R，τ∈R，和|σ|为|τ|.时间自动机A在时间序列（σ，τ）上的运行r，其中σ=σ...στ=τ...τ是一个有限序列σ1，τ1σ2，τ2σk，τk1k1kq0，ν0 −→qk，vk 我们说r从q0开始到qk结束。 我们用游程A表示，一组A运行，而运行N包含所有游程r的游程A在时间序列（σ，τ）上，使得τ是整数序列（即，延误σ1，τ 1σ 2，τ 2在这些运行中是自然数）。对于游程r=<$q0，ν0<$− → <$q1，ν1<$−→σk，τkσ1σ2σk... −→ <$qk，νk<$，r的签名是q0−→q1−→. - →qk，即的顺序和离散的步骤。更进一步，r所花费的总时间是Ki=1 τi.加权时间自动机是具有成本函数的时间自动机A•Js：n-→N（切换成本），以及• Jd：Q −→N（持续时间成本）。给定A 的游程r，设e1，. ，ek是在r和q0，.，q，k是访问位置的序列。 我们与RS. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-23701以下费用：克• Js（r）=i=1Js（ei），以及克-1• Jd（r）=i=0τi·Jd（qi）.与运行r相关联的总成本则为J（r）=Js（r）+Jd（r）。在下面的例子中，我们展示了一个加权的时间自动机，它模拟了一个简单的计算机网络。例3.2考虑图2中的定时转换系统。 它将图1中的网络建模为加权时间自动机。除了已经在图1中的位置之外，还有5个附加的位置p0、p1、p2、p3、p4用于实现传输延迟，即，从消息从网络的节点发送的时刻到相同消息在目的地节点接收的时刻所经过的时间。我们需要使用位置来建模传输延迟，因为时间自动机中的转换是瞬时的（即，它们不需要时间），我们需要以区分网络的每个节点处的处理时间和传输时间。唯一的起始位置是A。图2中的自动机使用两个时钟。时钟x用于计算在每个位置花费的时间，因此在每次转换时重置（为了更清楚地表示，在图2中我们省略了边缘上的重置），时钟y用于测量从A到达B的总时间。位置上的权重表示网络中相应节点的计算能力，即每个时间单位可以执行的操作数量。因此，0标记所有不表示实际节点的位置p0、p1、p2、p3、p4的网络。边缘上没有权重，只有微不足道的不变量因此，在图中省略了它们。警卫被用来模拟处理和传输延迟。考虑当Ar=A，（0，0）A−→0时的rp，（0，0）51. 5）−0→。21. 7）−→1q，（0，2.第七章）0的情况。1（0，2.第八章）六、3（0，9. 1）无菌。成本1 3⟩−→β3，−→与r相关联的是J（r）= 0。2·w1+ 0. 1·w3，表示在从A到B的路径上在网络中执行的计算。r的总时间为9。1.Q4WTA的决策与优化问题在本节中，我们讨论两个加权定时自动机的优化问题，解决第2.2节中给出的方案的第2步。解决这些问题足以解决加权时间自动机上的一般决策问题，加权时间自动机是验证安全性的自然框架238S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-一一w10x≤2w30x≤1w00Ax= 01≤x≤2均p0第一季第一季第三季1≤x≤ 3p31≤x≤ 2x≤24≤x≤8w5By= 0时3≤x≤5Q2w22≤x≤31≤x≤2p2q40w4p4x≤30y≤151≤x≤ 5图二. 一个简单的网络模型本文讨论的类型的属性。第2.2节方案的第2步需要计算网络可以使用Alice选择的精确时间Θ执行的模N我们可以把这个问题简化为在加权时间自动机中计算最小和最大成本运行为此，我们可以将网络建模为例3.2中的加权时间自动机，然后我们添加一个目标位置T，并从对应于网络中实际节点的所有位置转移到T。我们让这个增加的转换由z= Θ保护，其中z占自计算开始以来的总时间设A是加权时间自动机，T是目标位置。在固定时间Θ的最大成本可达性是计算在T结束且其总时间为Θ的所有运行的最大成本的问题类似地，在固定时间Θ的最小成本可达性是计算在T结束并且其总时间为Θ的所有运行上的最小成本的问题。让我们回想一下，在固定时间的最小成本可达性是[3]和[5]中讨论的最小成本可达性问题的特殊情况。在下文中，我们将把加权时间自动机上定义的最小成本和最大成本可达性问题简化为加权有向图上的类似为了简化我们的结果的介绍，我们限制到加权的时间自动机与警卫和不变量是封闭的集合（封闭的警卫和不变量）。这不失一般性，因为对于时间自动机A，在时间Θ处的运行的最小和最大成本是通过将所有严格不等式变为非严格不等式而从A获得的加权时间自动机Aj的最小和最大成本（参见[3]）。我们开始使用以下技术引理，该引理允许我们将对最优路径的搜索仅限于游程N内的路径。引理4.1设A是一个具有封闭保护的加权时间自动机，不变量 给定一个游程r∈游程A，有两个游程r1，r2∈游程N等J（r1）≤J（r）≤J（r2），并且r1和r2的签名与R的签名S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-239D一证据 设r是σ1，τ1σ2，τ2σk，τk. 从重置来看，q0，ν0 −→ <$qk，νk<$的不变量的访问位置，和警卫采取的过渡对r，它是可能的，以建立一个系统的线性不等式I的变量y1，.，yk，使得对于实数d1，.，dk满足I，σ1，d 1Jσ2，d2σk，dkJq0，ν0 −→ <$qk，νk <$是A的游程。请注意，I中的变量的值都是1，并且是时钟约束自然数，我们有对应于I的多面体集合P的所有角点都有自然数作为分量。回想一下，多面体集合上的线性成本函数在其角点之一处达到其最小值/最大值。因此，我们可以选择（d1，. ，dk）∈ P，使得a的成本运行σ1，d1Jσ2，d2σk，dkJq0，ν0 −→ <$qk，νk<$在P上最小化/最大化和d1，.，d，k是整数。 Being（τ1，.，τk）∈P，由于我不严格，我们得到引理。Q上面的引理允许我们在加权有向图上进行计算事实上，我们可以限制访问状态q，ν的运行，其中ν（x）是每个时钟变量x的整数。 对于以下构造，我们假设A具有在所有转换上从不复位的时钟（即， 我们假设该时钟总是包含从计算开始以来经过的总时间）。让这只钟是Y。 设GA=（V，E）是带权函数W定义为：• V ={q，ν|v（x）∈ {0，.，Θ}对所有x∈C和ν满足inv（q）};• （u，v）∈E且W（（u，v））=c当且若e其中u−→1v是一个时间步且dc=J（q），或u−σ→v是A的一个离散序列p，对应于 a跃迁e和c=Js（e）。G A的一个顶点<$q，ν<$q使得ν（y）= d称为在时间d的一个顶点。给定一个游程r∈游程N，使得它的总时间不大于Θ，我们记为ρ（r）σ1，τ 1σ 2，τ 2GA的相应路径。对于给定的游程r=<$q0，ν0<$− → <$q1，ν1<$−→σk，τkw1wm. . . −→ <$qk，νk<$，路径ρ（r）isu0−→. . −→umwhhereforri=0， . . . ，m，ui是<$qj，νj+ h<$，其中h ≤ τj+1，j ∈ {0，... ，k}且i = h +Jl=1（τl+1）（假设如果j = 0，则sum=0）6。与路径ρ（r）相关的总成本为W（ρ（r））=Mp=1 wp.以下定理成立。定理4.2设A是加权时间自动机，T是目标位置，Θ是正实数。 它认为r是A从q0∈ Q0开始，到T结束的一个游程，其代价最大（分别为最小值），当且仅当ρ（r）是最大成本（分别为6.由G A a g a ph确定的f is的序列唯一地确定fis的序列。240S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-一GA中从θq0，0θ到θT，νθ的最小成本）路径，其中θT，νθ是时间Θ处的顶点。证据 通过引理4.1，我们可以将对最小/最大成本运行的搜索限制在运行N中的运行。 从关联到A的加权图 GA的定义，我们有A的一个游程r，从<$q0，0<$p开始，到T结束当且仅当在GA中存在从<$q0，0<$p到形式为<$T，<$p的顶点的对应路ρ（r）。此外，r的总时间是Θ，当且仅当是时间Θ的顶点。为了结束证明，我们只需要证明r和ρ（r）的代价是一致的。令r=σ1，τ1σ2，τ2σk，τk.根据定义，路径ρ（r）是q0，ν0w1 −→q1，ν1WM−→ ... −→ qk，νkσj+1，τ j+1使得每一个跃迁都是u0−→. −→umwi+1wJj j −→r中的n_qj+1，v_j+1对应于一条s-路u_i-→. . −→iuiJ 在ρ（r）中，其中拉吉l=1（τl+ 1）（如果j= 0，则i= 0）和iJ=i+（τj+1+ 1）。召回当0≤p≤τj+1时，ui+p=<$qj，νj+p<$，且ndW（（ui+p，ui+p+1））=Jd（qj）.此外，uiJ−1=且W（（uiJ−1，uiJ））=Js（ej），其中ej是σj+1discretestep<$qj，νj+τj+1<$−→<$qj+1，νj+1<$。所以，他和他一起做了一件事 wi+1wJu−→. . . −→iuJ是τ·J（q）+J（e），这正是相关iij +1dJSJσj+1，τ j+1其中h<$qj，νj<$−→<$qj+1，νj+1<$。对于每个j = 0，迭代此参数，... k，我们有J（r）= W（ρ（r））。Q利用上述结果，我们得到以下定理。定理4.3最小成本（分别为最大成本）在固定时间的加权时间自动机的可达性可以在指数时间内求解证据 通过定理4.2，给定一个加权时间自动机A，我们可以将这样的问题限制为在加权有向图GA中搜索最小和最大费用路。通过简单的计算，GA的顶点数为：|·（Θ + 1）n，其中Q是位置的集合，并且n是|·(Θ +1) n, where Q is the set oflocations and n is the number of clocks ofA.因此，GA的大小在位置的数量上是线性的，并且在Θ的表示的长度和时钟的数量两者上是指数的。为了计算加权有向图上的最优加权路径，我们可以使用标准算法，在多项式时间内运行的顶点数。例如，我们可以使用Dijkstra算法来计算来自单个源的最短路径。 因此，我们得到了定理。Q在本节结束时，我们讨论与所考虑的优化和安全问题相关的决策问题设θ≤ Θmin≤ Θmax和J∈是自然数。 给定加权时间自动机A和权重为w的目标位置T，我们感兴趣的是：I=S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-241以下决策问题：（问题1）对于所有在T结束的总时间至多为Θ的游程r，我们希望确定J（r）是否小于J（r）。（问题2）对于所有在T结束的总时间为θ的运行r，我们希望确定是否存在t≥0使得t+ Θ∈ [Θmin， Θmax]且t·w+J（r）=J。我们把上面的问题1和2统称为时间成本有界可达性问题。为了解决问题1，我们可以计算在时间Θ内运行到T而为了解决问题2，除了解决最大成本可达性问题之外，我们还计算在时间Θ运行到T的最小成本。事实上，令Jmin和Jmax分别为在时间Θ运行到T显然，存在满足问题2所要求的条件的t，当且仅当Jmin+（Θmax− Θ）·w≥J和Jmax+（Θmin− Θ）·w≤J成立。利用上述结果，我们得到了预期的结果。定理4.4加权时间自动机的时间-费用有界可达性是可判定的，并且可以在指数时间内求解。由于时间自动机的可达性问题是P空间完全的[2]，我们也得到了这个问题的下界推论4.5加权时间自动机的时间-费用有界可达问题是P空间困难的。5结论在这篇论文中，我们讨论了在计算机网络上的定时释放密码Rivest等人在[12]中引入并研究了定时释放加密，其动机是发送“信息到未来”。在本文中，我们扩展了他们的方法来分析一个自然的场景，其中定时释放加密用于必须在目的地交付之前通过计算机网络的消息。因此，需要考虑所使用的网络的几个参数，以确保消息的保密性直到某个时间期限。 特别是 给定一个不安全的计算机网络G与源A和目的地B，我们已经解决了以下安全问题：我们已经提出了一个解决这个安全问题的基础上加权242S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-时间自动机解决方案包括将问题转化为这类自动机的决策问题，时间-费用有界可达性。我们已经研究了这个问题，并提出了一个算法，需要的时间指数的时间期限的大小和在自动机中使用的时钟的数量。我们观察到这个问题不太可能有次指数解，因为从标准时间自动机[2]中可达性的计算复杂性，我们得到这个问题是P空间困难的。在某些情况下，可以合理地假设消息的接收者只能控制网络中的某些节点，因此消息只能路由到这些相邻节点而不是其他节点。我们可以通过将网络建模为加权时间自动机上的两人游戏来捕获这个框架，并搜索接收者的获胜策略我们将在未来的研究中探索这种情况。引用[1] R. 巴尔角 Courcoubetis和T.A. 亨辛格 计算累计 延迟实际上- 时间系统第五届计算机辅助验证国际会议论文集，CAVSpringer，1993年。[2] R. D.L.迪尔时间自动机理论。理论计算机科学，126：183[3] R. Alberr，S. La Torre和G. J·帕帕斯 加权时间自动机中的最优路径。 在Proc. of the 4thInternational Workshop on Hybrid Systems：Computation and Control，HSCCSpringer，2001年。出现在理论计算机科学。[4] E. Asarin和O.马勒尽快：时间自动机的时间最优控制。 在proc 第二届国际混合系统研讨会：计算与控制，LNCS 1569，第19 - 30页。Springer，1999年。[5] G. Behrman，T. Hune，A. Fehnker，K. Larsen，P. Pettersson，R. Romijn和F.凡德拉格定价时间自动机的最小成本可达性。在第四届混合系统国际研讨会论文集：计算和控制，HSCC161. Springer，2001年。[6] D. Boneh ， M. Naor ， Timed Commitments ， Advances in Cryptology ： Proceedings ofCryptology[7] C. Courcoubetis和M.扬纳卡基斯实时系统中的最小和最大延迟问题。第三届计算机辅助验证国际会议论文集，LNCS 575，第399 - 409页。施普林格，1991年。[8] S.拉托雷湾Mukhopadhyay和A.穆拉诺无圈加权时间自动机的最优可达性与控制。第二届IFIP理论计算机科学国际会议，IFIP TCSKluwer，2002年。[9] K. G.拉森湾 Behrman，E. Brinksma，A. Fehnker，T. Hune，P. Petersson，and J. Romijn. 尽可能便宜：定价时间自动机的有效成本最优可达性。在Proc. of the 13th InternationalConference on Computer Aided Verification，CAVSpringer，2001年。[10] W.毛，定时发布密码学，在SAC 2001会议录中，S。Vaudenay和A. Youssef（Eds.），计算机科学笔记卷。2259，342S. La Torre et al. / Electronic Notes in Theoretical Computer Science 99（2004）229-243[11] P. Niebert，S. Tripakis和S.尤文 时间自动机的最小时间可达性。在Proc. 第八届IEEE地中海控制与自动化会议，2000年。[12] R.L.Rivest，A.Shamir，D.A.华格纳， 时间锁谜题与定时释放密码，技术报告，麻省理工学院/LCS/TR-684 。可查阅网址：（theory.lcs.mit.edu/rivest/RivestShamirWagner-timelock.ps）。