On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments (Long Version)

决定密码协议的安全属性。关键周期的应用

Deciding security properties for cryptographic protocols. Application to key cycles

有大量的工作致力于安全协议的形式化验证。在本文中，我们重新审视和扩展的NP-完全决策过程有限的会话数。我们使用一个，现在的标准，演绎约束形式主义建模的安全协议。我们的第一个贡献是给出一组简单的约束简化规则，它允许将任何演绎约束系统减少到一组解决的形式，代表所有的解决方案（在会话的范围内）。因此，我们证明，决定存在的关键周期是NP-完全的有限数量的会话。键环的问题已经提出了最近的工作有关的计算和符号模型。所谓的符号模型的可靠性实际上要求没有关键周期（例如，enc（k，k））在协议的执行中发生。否则，需要更强的安全性假设（如KDM安全性）。我们表明，我们的决策过程也可以应用于再次证明的可判定性的认证类属性和可判定性的一个显着的片段的协议与时间戳。

精确的混合选择多方会话类型

Mixed Choice Multiparty Session Types, Precisely

本文针对含会话委托等特性的混合选择多方会话类型，证明其子类型关系的精确性，开发通用类型系统并实现相关检查算法，经案例研究验证其有效性。

Imprecise Probability for Multiparty Session Types in Process Algebra

In this paper we introduce imprecise probability for session types. More exactly, we use a probabilistic process calculus in which both nondeterministic external choice and probabilistic internal choice are considered. We propose the probabilistic multiparty session types able to codify the structure of the communications by using some imprecise probabilities given in terms of lower and upper probabilities. We prove that this new probabilistic typing system is sound, as well as several other results dealing with both classical and probabilistic properties. The approach is illustrated by a simp…

限定会话类型的类型检查算法

A type checking algorithm for qualified session types

我们提出了一个类型检查算法，建立一个基于会话的纪律在PI演算米尔纳，Parrow和沃克。我们的会话类型被限定为线性或无限制。线性类型的通信通道保证只在一个线程中出现，可能会出现多次;之后它们会演变为不受限制的通道。会话协议由类型构造函数描述，该构造函数表示同一个通信通道的两端。我们确保了算法的合理性，通过显示消耗所有线性资源的过程被接受的类型系统保留在计算过程中的类型，类型检查是一致的w.r.t.结构一致性

异步多方会话中的混合选择

Asynchronous Multiparty Sessions with Mixed Choice

本文提出一种异步多方会话的校验算法，支持输入和输出前缀的非确定性选择，通过全局类型系统确保通信标签集的连贯性，证明了类型正确性和会话保真性，展示了混合选择在异步多方协议中的表达力。

混合选择多方会话中的分离性与可编码性（技术报告）

Separation and Encodability in Mixed Choice Multiparty Sessions (Technical Report)

本文为混合选择同步多方会话演算提出通用类型系统并证明其安全性，进而通过可编码性与分离性分析比较九个演算的表达能力，证明MCMP严格强于经典多方会话。

Domain-Aware Session Types (Extended Version)

We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global progress, and termination. Typing also ensures that …

Generalised Multiparty Session Types with Crash-Stop Failures (Technical Report)

Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily. Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session π-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the …

比较无死锁会话类型进程

Comparing Deadlock-Free Session Typed Processes

除了遵守规定的协议，以通信为中心的系统永远不应该“卡住”。这个需求已经通过诸如进度或（死）锁自由度之类的活动属性来表达。已经提出了几个类型的纪律，确保这些属性的移动进程。不幸的是，人们对这些规程之间的精确关系以及它们所引发的类型化过程的类知之甚少。本文对两类无死锁的会话型并发进程L和K进行了比较。类L因其规范性而突出：它自然地产生于将线性逻辑命题解释为会话类型。类K，通过将会话类型编码到Kobayashi的使用类型中获得，包括在其他类型系统中不可类型化的进程。我们证明了L严格包含在K中。我们还确定了L和K重合的精确条件。一个关键的观察是，并行进程之间的共享程度决定了类型化进程的新表达层次结构。我们还提供了一个保持类型的重写过程中的进程在K到L。这个过程表明，虽然共享程度是有效的，但它是区分类型化进程的一个相当微妙的标准。

异步多方兼容性的逻辑解释

A Logical Interpretation of Asynchronous Multiparty Compatibility

本文在命题即类型框架下将多方兼容性的相干性条件推广为转发器，并证明转发器完全刻画所有类型良好的多方兼容进程。

具有有界和无界递归的协作过程的类型检测活性

Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion

我们提出了第一个会话类型系统，保证可能非终止通信进程的请求-响应活性属性。这些类型用一组所需的响应来扩充标准二进制会话类型的分支和选择类型，这表明每当选择特定标签时，最终也必须选择一组其他标签，即其响应。我们证明，这些扩展类型是严格的表达比标准的会话类型。我们提供了一个类型系统的过程演算类似于一个子集的内部（基于数据）和外部（基于事件）分支，消息传递，有界和无界循环的协作BPMN流程。我们证明了这个类型系统是合理的，即，它保证了无死锁进程的请求-响应活性。我们在一个无限状态系统的具体例子上说明了微积分和类型系统的使用。

作为通用进程类型的会话类型

Session Types as Generic Process Types

行为型系统比通常的静态分析更安全。它们基于“类型即进程”的思想，为特定的属性提供专用的类型代数，从协议兼容性到竞争自由、锁自由甚至响应性。有两种成功的方法，尽管它们有很大的不同，它们是会话类型和进程类型。前者允许使用特定类型（证明）系统来指定和验证（分布式）通信协议;后者允许从系统规范中推断出一个过程抽象，使用通用类型（证明）系统可以更简单地验证属性。这些方法之间的关系是什么？一般的一个可以substantially具体的一个？代价是什么？前者可以作为后者的编译器吗？本文介绍的工作是朝着回答这些问题迈出的一步。具体地说，我们定义了一个逐步编码的pi演算会话和会话类型（系统的盖伊和孔）到一个pi演算的进程类型（通用类型系统的五十岚和小林）。我们对会话类型环境、极性（区分会话通道端点）和标记总和进行编码。我们展示了编码的正向和反向操作对应，以及类型对应。为了在进程类型子类型中忠实地编码会话子类型，需要向目标语言添加记录构造函数和新的子类型规则。总之，作为协议抽象的会话类型的编程便利性可以与pi演算的简单性和功能相结合，特别是利用通用类型系统提供的框架。

概率会话类型中通过子类型化实现的组合式接口细化

Compositional Interface Refinement Through Subtyping in Probabilistic Session Types

本文提出概率混合选择多方会话π演算及其灵活子类型系统，允许用多个通道细化单个接口，并证明主体归约、无错误性和无死锁性，从而支持概率分布式通信的组合式验证与逐步细化。

异步多参与方会话类型中的崩溃停止故障

Crash-Stop Failures in Asynchronous Multiparty Session Types

针对现实分布式系统中的崩溃故障，提出一种带崩溃停止语义的异步多参与方会话类型理论，通过崩溃处理分支和可选可靠性假设，保证良类型进程的无死锁、协议一致性与活性。

并发中的终止性再探讨

Termination in Concurrency, Revisited

本文从终止性视角比较了 $π$-演算进程的两种类型系统（基于权重的方法与线性逻辑的 Curry-Howard 对应），揭示了它们之间的精确联系及其支持的客户端/服务器交互类别。