[nathanrf]

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)

[hyperthesis]

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.

I would say it's like how you use an API.