The paper defines them as programs in a process calculus (which is fairly standard as far as theory for protocols is involved): Definition 1 (Asserted protoc

The paper defines them as programs in a process calculus (which is fairly standard as far as theory for protocols is involved): Definition 1 (Asserted protocols) Asserted protocols, or just protocols for short, are ranged over by S and are defined as the following syntax rules: S ::= |p.S action prefix | +{ l_i : Si }_i∈I branching | µt.S fixed-point | t recursive variable | end end | assert(n).S assert (produce) | require(n).S require | consume(n).S consume Process calculi are "fundamental" descriptions of computation analogous to lambda calculus but oriented around communication instead of function calls. (As far as paper structure, I find that usually the important "basic" definitions in programming language research papers are usually in Section 2, since Section 1 serves as a high-level overview). Basically, a protocol consists of a a sequence of sends/received on a particular channel, mixed with some explicit logic and loops/branches until you reach the end. There's some examples in Section 2.1 which are too complicated to reproduce here. As a general note on reading protocols- for (good, but industry-programmer-unfriendly) technical reasons they're defined and written as "action1.action2.action3.rest_of_program" but mentally you can just rewrite this into { action1(); action2(); action3(); ... rest_of_program ... } (in particular, making "the rest of the program" part of each statement makes specifying scope much easier and clearer, which is why they don't just use semicolons in the first place)