# Developing a proven, secure communication protocol from scratch

**URL:** <https://discourse.rocq-prover.org/t/developing-a-proven-secure-communication-protocol-from-scratch/1988>\
**Category:** Miscellaneous\
**Created:** [June 23, 2023, 11:54am UTC](https://discourse.rocq-prover.org/t/developing-a-proven-secure-communication-protocol-from-scratch/1988 "2023-06-23T11:54:12Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![hmltn2](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/hmltn2/32/851_2.png) [@hmltn2](https://discourse.rocq-prover.org/u/hmltn2)\
**Post date:** [June 23, 2023, 11:54am UTC](https://discourse.rocq-prover.org/t/developing-a-proven-secure-communication-protocol-from-scratch/1988/1 "2023-06-23T11:54:12Z")

</div>

Here is the content of my recent stack overflow post discussing what I intend to begin working on, immediately:

Formally verified email or communication?

This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway.

I would like to consider the simplest possible formally verified communication protocol.

Is there a common approach for designing one?

For example: is it required to model all objects of the system, first?

For example, there are:

- people (who write the messages)
- the messages they send
- transportation avenues (like the internet)
- the concept of a message arriving, being received/saved/stored, being read, being replied to, etc
- message “states” like readable / unreadable (if you don’t want someone reading it while it travels)
- locations (addresses where the messages go)

My approach would be to use David Spivak’s Categorical Query Language because it suggests that category theory can be used as a “universal modeling language”. Perhaps I should first create an Olog, a category-theory ontology, as a first step to trying to formally prove the security of the communication protocol, for example, that there is no possible combination of states that would lead to an unexpected outcome, like a person losing the ability verify their identity to read their private messages, or send them from their identity, for example.

How should I do this?

I will attempt my approach above unless someone can guide me more.

The point is a way to send messages, formally proven to never allowed someone to hack your account or steal your identity, or spy on or intercept your messages. For example, you could have a kill-switch where even if somehow your account goes rogue, you can always shut it down - and that’s formally proven that the kill switch could never be deactivated (perhaps).

——

Would anyone like to discuss approaches with me, in the comments?

I will begin by learning type theory at last - a language to express whatever system I end up working in. Presumably Coq, since it is built on the calculus of inductive types. Or StandardML?

Thank you.

---

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [July 5, 2023, 8:31am UTC](https://discourse.rocq-prover.org/t/developing-a-proven-secure-communication-protocol-from-scratch/1988/2 "2023-07-05T08:31:07Z")

</div>

> [@hmltn2](#):
>
> For example: is it required to model all objects of the system, first?

My answer is no.  
Consider modeling one part of the system at first, and then define how different parts of the system work with each other.

For example, my experience with [coq-http](https://github.com/liyishuai/coq-http) was:

1. First define the syntax and a tiny subset of semantics.
2. Extend the semantics to cover a larger subset of the protocol.
3. Modify the syntax to enable symbolic evaluation of the model.
4. Plug the HTTP server model on a TCP network model to represent concurrency.

I didn’t design the network model in Day 1, as my brain cannot hold that many projects at once. Moreover, you can’t predict how the server model looks like, until you make it really interesting and worth plugging to the network.

---

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [July 10, 2023, 9:23pm UTC](https://discourse.rocq-prover.org/t/developing-a-proven-secure-communication-protocol-from-scratch/1988/3 "2023-07-10T21:23:40Z")

</div>

There are many works that model and verify message-passing distributed systems in Coq, at various levels of abstraction and sometimes down to executable code. A model or verification approach is usually justified by its demonstration on convincing examples of message-passing systems from the literature. Some examples:

- [Verdi](https://github.com/uwplse/verdi) (used to verify an [implementation of the Raft protocol](https://github.com/uwplse/verdi-raft))
- [Chapar](https://github.com/coq-community/chapar)
- [VLSM](https://github.com/runtimeverification/vlsm)
- [Disel](https://github.com/DistributedComponents/disel)
- [Aneris](https://github.com/logsem/aneris)
- [Velisarios](https://github.com/vrahli/Velisarios)

Most of these have research papers linked from their GitHub pages. Some support reasoning about or handling Byzantine failures.

---

<div class="post-metadata">

**Author:** ![juliushamilton](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/juliushamilton/32/948_2.png) [@juliushamilton](https://discourse.rocq-prover.org/u/juliushamilton)\
**Post date:** [April 10, 2024, 4:52am UTC](https://discourse.rocq-prover.org/t/developing-a-proven-secure-communication-protocol-from-scratch/1988/4 "2024-04-10T04:52:49Z")

</div>

Could you explain where the entry point / top level file of that Coq code is? I want to study it. Thanks

---

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [April 10, 2024, 5:13pm UTC](https://discourse.rocq-prover.org/t/developing-a-proven-secure-communication-protocol-from-scratch/1988/6 "2024-04-10T17:13:50Z")

</div>

- HTTP syntax [`http_reqest` and `http_response`](https://github.com/liyishuai/coq-http/blob/cabde79a4a0d978d031475c7443be7fd43a711c5/theories/Message.v#L145-L158)
- The server model [`http_smi`](https://github.com/liyishuai/coq-http/blob/cabde79a4a0d978d031475c7443be7fd43a711c5/theories/Semantics.v#L384-L387)
- The TCP network model [`tcp`](https://github.com/liyishuai/coq-http/blob/cabde79a4a0d978d031475c7443be7fd43a711c5/theories/Tcp.v#L70-L87) that can be [`compose`](https://github.com/liyishuai/coq-http/blob/cabde79a4a0d978d031475c7443be7fd43a711c5/theories/Tcp.v#L109-L195)d with the server model

---

<div class="post-metadata">

**Author:** ![juliushamilton](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/juliushamilton/32/948_2.png) [@juliushamilton](https://discourse.rocq-prover.org/u/juliushamilton)\
**Post date:** [April 10, 2024, 5:25pm UTC](https://discourse.rocq-prover.org/t/developing-a-proven-secure-communication-protocol-from-scratch/1988/7 "2024-04-10T17:25:47Z")

</div>

Do you wanna connect by email? [juliushamilton100@gmail.com](mailto:juliushamilton100@gmail.com)

I’m hard at work trying to build my first formally verified model of a system. I would love to be able to talk about this with someone. Can connect here in the discourse too of course.