Comment by 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)