protocol developers

Abstract: We prove that the state space of every well-formed session type, quotiented by strongly connected components, forms a bounded lattice; n-ary parallel composition yields product lattices. Two consequences follow: duality preserves the lattice up to isomorphism, and Gay-Hole width subtyping corresponds to lattice embedding for non-recursive types. We validate this on 108 benchmark protocols across networking, databases, distributed systems, AI, and fault tolerance: all form lattices, 93 distributive, 15 non-distributive. Mechanised in Lean 4 with two independently developed tool implementations.

Abstract: The Participants-as-Interfaces (PaI) methodology for system composition proposes that system participants can be regarded as interfaces. For each system in a given collection, one participant is designated to serve as its interface. When the systems are composed, these interface participants are replaced with gateways that communicate with one another by forwarding messages. We generalise the approach to partial gateways, where gateways can forward only a chosen set of messages. As for the standard PaI approach, we exploit such extended version for systems of communicating finite state machines (CFSMs). This extension is fully detailed for the binary case, and can be scaled up to the multicomposition case. We prove that many relevant communication properties (deadlock-freeness, reception-error-freeness, etc.) are preserved by PaI composition via partial gateways in case also the connection policy (i.e. the system representing the way we wish gateways interact with each other) enjoys the same properties. Such a proof turns out to be just a corollary of a property preservation result for a restricted and partial composition method, dubbed fusion-composition. Fusion-composition hence turns out to be at the heart of the PaI composition approach.

Abstract: Post-quantum protection is delivered to a peer, not declared in a file: whether a session is quantum-resistant is a relation between a server's configuration and the clients that reach it. We show that no single peer can soundly gate that relation. Shipped SSH clients are not ordered: two of their post-quantum capability classes are minimal and incomparable, so a check pinned to either misses the other family's withdrawal. A peer taking both fares no better: it falls back and misses both, or, where classical outranks one family, catches just that one. No case flags both. Nothing above the wire carries the relation either. An artifact-side instrument cannot encode it, because a peer population is not one of its inputs; and across seven configurations on two protocols we find that not one of the five scalars deployed auditors expose to automation moves, while unrelated degradation moves the ones that discriminate at all: the auditors do compute the delivered algorithm, and discard it at the interface automation reads. Nothing else catches the loss either, because nothing breaks: removing a hybrid key exchange starts the daemon, validates the configuration, passes the tests and serves the client, and the adversary it defends against does not exist yet, so no functional signal can carry the loss even in principle. We then show that agents make that state reachable at scale, driving a validated downgrade in 40 of 40 episodes from ordinary engineering prose, against 0 of 40 on a matched neutral document.