基于进程代数语义的带选择 strand space 模型

密码协议中的角色并非总是线性执行，而可能包含选择点导致协议沿不同路径继续。本文解决在密码协议的 strand space 模型中表示选择的问题，特别是在 Maude-NPA 密码协议分析工具中的使用。为实现此目标，我们开发并给出了一个支持丰富选择原语分类以组合 strand space 的密码协议进程代数的形式语义。在我们的分类中，确定性和非确定性选择被进一步细分。非确定性选择可以是显式的（即选择两条路径之一）或隐式的（即非确定性地选择变量的值）。类似地，确定性选择可以是显式 if-then-else 选择（即若谓词满足则选一条路径，否则选另一条）或隐式确定性选择（即仅当匹配某模式时才继续执行）。我们确定了一类包含有限分支及某些无限分支情况的选择，本文予以处理。我们提供了新进程代数的预期前向执行语义与 Maude-NPA 原始符号后向语义之间保持攻击可达性的互模拟结果。我们已将进程代数语法及其向 strand 的转换完全集成到 Maude-NPA 中。我们用多个例子说明了其表达力和自然性，并展示其如何有效用于形式分析。这允许用户从此使用进程语法编写协议，其比 strand space 语法更便于表达选择，后者中只能通过两个或更多在选点前相同的 strand 隐式指定选择。