Formal patterns are formally specified solutions to frequently occurring distributed system problems that are generic, executable, and come with strong qualitative and/or quantitative formal guarantees. A formal pattern is a generic system transformation which transforms a usually infinite class of systems in need of the pattern's solution into enhanced versions of such systems that solve the problem in question. In this paper we demonstrate the application of formal patterns to protocol dialects. Dialects are methods for hardening protocols so as to endow them with light-weight security, especially against easy attacks that can lead to more serious ones. A lingo is a dialect's key security component, because attackers are unable to ''speak'' the lingo. A lingo's ''talk'' changes all the time, becoming a moving target for attackers. In this paper we present several formal patterns for both lingos and dialects. Lingo formal patterns can make lingos stronger by both transforming them and by composing several lingos into a stronger lingo. Dialects themselves can be obtained by the application of a single dialect formal pattern, generic on both the chosen lingo and the chosen protocol.

翻译：形式化模式是对分布式系统中频繁出现的、具有通用性、可执行性且带有强定性或定量形式化保证的问题的正式规范解决方案。形式化模式是一种通用的系统变换，它将通常无限类需要该模式解决方案的系统，转换为解决该问题的增强版本。本文展示了形式化模式在协议方言中的应用。方言是强化协议以实现轻量级安全性的方法，尤其能防御可能引发更严重攻击的简易攻击。行话是方言的关键安全组件，因为攻击者无法“说出”行话。行话的“话语”会不断变化，成为攻击者的移动靶标。本文提出了多种针对行话和方言的形式化模式。行话形式化模式既能通过变换单个行话使其更强，也能通过组合多个行话形成更强行话。而方言本身可通过应用单一的方言形式化模式获得，该模式对所选行话和所选协议具有通用性。