具有安全盒与受损主体的编排

我们为编排级别的会话描述配备了安全基础设施的简单抽象。消息组件可以封装在（可能是嵌套的）“盒”中，并标注这些组件的预期源和目的地。这些盒将通过密码学来实现。串空间为这些编排提供了语义，其中某些角色可以由受损主体扮演。骨架是一种偏序结构，包含由常规（非受损）主体执行的局部行为（串）。如果一个骨架包含足够的常规串，使得它与受损主体的任何可能活动结合时实际上能够发生，则该骨架是被实现的。如果此外每个传输给常规参与者的消息也被交付，则它是交付保证（DG）实现的。我们在骨架上定义了一个新的变迁系统，其中的步骤会添加常规串。这些步骤解决了测试，即骨架中如果没有额外的常规行为就不可能发生的部分。我们证明了关于该变迁系统的三个主要结果。首先，每个极小的 DG 实现骨架都可以使用该变迁系统，从它所嵌入的任何骨架到达。其次，如果从骨架 A 不可能执行任何步骤，则 A 是 DG 实现的。最后，如果 DG 实现的 B 可以从 A 到达，则 B 是极小的。因此，该变迁系统提供了一种系统的方法，用于在存在受损主体的情况下构造编排的可能行为。