Developing a proven, secure communication protocol from scratch

Miscellaneous
1

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.

2

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 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.

3 Likes
3

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:

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

2 Likes
4

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

6
1 Like
7

Do you wanna connect by email? 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.