Cryptographic protocols are used to engineer trust in online transactions.  In real-world deployments, implementations must be
scalable and fault-tolerant.  We present two analyses that enable this.  The first determines when multiple sessions of protocols can
safely interact concurrently to achieve scalability.  The second determines the minimal backup of a running protocol, which enables
fault-tolerance and even has value as an analysis technique.

We also observe that typical protocol specification languages do not match the abstractions used by protocol designers.  We therefore
present a protocol specification language that matches design idioms. We offer a compiler that transforms these specifications into
executables that can be deployed.

We evaluate our work on a large repository of known protocols to demonstrate its utility.  Our work has been formalized, verified, and
implemented using the Coq proof assistant.