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
(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)
Thanks for your guidance! I now see they're (now-obviously!) things like TCP and http. I had missed their informal definition:
> Here we use the term protocol to denote a specification of the interaction patterns between different system components. [...] To give a
more concrete intuition, an informal specification of a protocol for an e-banking system may be as follows: The banking server repeatedly offers a menu with three options: (1) request a banking statement, which is sent back by the server, (2) request a payment, after which the client will send payment data, or (3) terminate the session.
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
(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)