cfm · November 19, 2024 17:14
diff --git a/README.md b/README.md
diff --git a/Makefile b/Makefile
 trace.md: Makefile trace.py trace.yml
 	echo '```mermaid' > $@
 	./trace.py < trace.yml >> $@
 	echo '```' >> $@
diff --git a/trace.md b/trace.md
diff --git a/trace.py b/trace.py
 #!/usr/bin/env python3
 # This is a tool for visual derivation analysis---non-attack-oriented taint or
 # generic data-flow analysis---of a network protocol.  It depicts values and
 # their dependencies within and across locations and scopes, with some checks
 # to validate reuse.
 #
 # Standard input: YAML like `trace.yml`.
 #
 # Standard output: Mermaid graph diagram.
 # - Visual dependencies (graph edges) indicate:
 #   - local derivations (within subgraphs);
 #   - values received (across subgraphs).
 # - Listed dependencies are local, transitive, and cumulative: what's this value
 #   made of?
 #
 # Exceptions:
 # - `ValueError` if a key is reused across scopes within the same location.

 import yaml
 import sys

 data = yaml.safe_load(sys.stdin.read())

 print("graph TD")

 # The `nodes` dictionary is overloaded between global `key`s and fully-specified
 # paths like `{location}.{scope}.{key}`.
 nodes = {}
 # Edges are direct derivation relationships: `x --> y` means that `y` is derived
 # from `x`.
 edges = []
 # Iterate over locations in the trace; each will be a subgraph.
 for location, scopes in data.items():
    print(f"subgraph {location}")
    # Iterate over scopes in this location; each will be a subgraph.
    for scope, keys in scopes.items():
        print(f"subgraph {location}.{scope}")

        # Iterate over keys in this scope; each will be a node.
        for x in keys:
            # Save the key's definition at its fully-specified path so that we
            # can trace its dependencies.
            path = f"{location}.{scope}.{x}"
            nodes[path] = keys[x]
            nodes[path]["deps"] = set()

            # Iterate over the key's dependencies; each will be an edge.
            x_from = keys[x].get("from", [])
            for y_path in x_from:
                # Build the dependency's fully-specified path so that we can
                # refer to it globally.
                y_location, y_scope, y = y_path.split(".")

                # Identities were received from another location, which will be
                # indicated with a graph edge.
                if y != x:
                    nodes[path]["deps"].add(y)
                elif y_location == location and y_scope != scope:
                    raise ValueError(
                        f"{path} is reused across local scopes at {y_path}"
                    )
                # Otherwise, dependencies accumulate transitively within a
                # location.
                nodes[path]["deps"] |= nodes.get(y_path, {}).get("deps", set())

                arrow = "-->"
                # Mark "encryptions" by contact with a public key.
                if "PK" in y and y != x:
                    nodes[path]["encrypted"] = True
                    arrow = "--o"
                # Mark "decryptions" by contact with a secret key.
                elif "SK" in y and y != x:
                    nodes[path]["decrypted"] = True
                    arrow = "--x"

                edges.append(f"{y_path} {arrow} {location}.{scope}.{x}")

            # Output the node's definition, including all local dependencies for
            # this path.
            deps = ""
            if len(nodes[path]["deps"]) > 0:
                deps = " ←<br>" + "<br>".join(sorted(nodes[path]["deps"]))
            if "encrypted" in nodes[path] and "decrypted" in nodes[path]:
                print(f"{path}((**{x}**{deps}))")
            elif len(x_from) == 0:
                print(f"{path}>**{x}**{deps}]")
            else:
                print(f"{path}[**{x}**{deps}]")

        print("end")  # scope subgraph
    print("end")  # location subgraph

 # Output all the edges at the end, since they belong to the global graph.
 print("\n".join(edges))
diff --git a/trace.yml b/trace.yml
 journalist: # Location (or role): Where is this value (who has it)?
  long-term: # Scope: What is the lifetime of this value?  How long/far is it it applicable?
    # key: name of value
    #   from: list of other `{location}.{scope}.{key}` paths on which this path
    #     (this key, in this scope, at this location) depends
    J_SK: {}
    J_PK:
      from:
        - journalist.long-term.J_SK
    JC_SK: {}
    JC_PK:
      from:
        - journalist.long-term.JC_SK
  per-message:
    JE_SK: {}
    JE_PK:
      from:
        - journalist.per-message.JE_SK
    message_id:
      from:
        - journalist.per-request.kmid
        - journalist.per-request.enc_m_id
    message_ciphertext:
      from:
        - server.per-message.message_ciphertext
    ME_PK:
      from:
        - server.per-message.ME_PK
    k:
      from:
        - journalist.per-message.ME_PK
        - journalist.per-message.JE_SK
    m:
      from:
        - journalist.per-message.k
        - journalist.per-message.message_ciphertext
    S_PK:
      from:
        - journalist.per-message.m
    SC_PK:
      from:
        - journalist.per-message.m
    message:
      from:
        - journalist.per-message.m
  per-request:
    pmgdh:
      from:
        - server.per-request.pmgdh
    enc_m_id:
      from:
        - server.per-request.enc_m_id
    kmid:
      from:
        - journalist.per-request.pmgdh
        - journalist.long-term.JC_SK

 source:
  long-term:
    J_PK:
      from:
        - journalist.long-term.J_PK
    JC_PK:
      from:
        - journalist.long-term.JC_PK
    JE_PK:
      from:
        - journalist.per-message.JE_PK
    S_SK: {}
    S_PK:
      from:
        - source.long-term.S_SK
    SC_SK: {}
    SC_PK:
      from:
        - source.long-term.SC_SK
  per-message:
    ME_SK: {}
    ME_PK:
      from:
        - source.per-message.ME_SK
    k:
      from:
        - source.per-message.ME_SK
        - journalist.per-message.JE_PK
    message: {}
    m:
      from:
        - source.per-message.message
        - source.long-term.S_PK
        - source.long-term.SC_PK
    message_ciphertext:
      from:
        - source.per-message.k
        - source.per-message.m
    message_gdh:
      from:
        - journalist.long-term.JC_PK
        - source.per-message.ME_SK

 server:
  per-message:
    message_ciphertext:
      from:
        - source.per-message.message_ciphertext
    message_gdh:
      from:
        - source.per-message.message_gdh
    ME_PK:
      from:
        - source.per-message.ME_PK
    message_id: {}
  per-request:
    RE_SK: {}
    RE_PK:
      from:
        - server.per-request.RE_SK
    kmid:
      from:
        - source.per-message.message_gdh
        - server.per-request.RE_SK
    pmgdh:
      from:
        - source.per-message.ME_PK
        - server.per-request.RE_SK
    enc_m_id:
      from:
        - server.per-request.kmid
        - server.per-message.message_id
	trace.md: Makefile trace.py trace.yml
	echo '```mermaid' > $@
	./trace.py < trace.yml >> $@
	echo '```' >> $@
	#!/usr/bin/env python3
	# This is a tool for visual derivation analysis---non-attack-oriented taint or
	# generic data-flow analysis---of a network protocol. It depicts values and
	# their dependencies within and across locations and scopes, with some checks
	# to validate reuse.
	#
	# Standard input: YAML like `trace.yml`.
	#
	# Standard output: Mermaid graph diagram.
	# - Visual dependencies (graph edges) indicate:
	# - local derivations (within subgraphs);
	# - values received (across subgraphs).
	# - Listed dependencies are local, transitive, and cumulative: what's this value
	# made of?
	#
	# Exceptions:
	# - `ValueError` if a key is reused across scopes within the same location.

	import yaml
	import sys

	data = yaml.safe_load(sys.stdin.read())

	print("graph TD")

	# The `nodes` dictionary is overloaded between global `key`s and fully-specified
	# paths like `{location}.{scope}.{key}`.
	nodes = {}
	# Edges are direct derivation relationships: `x --> y` means that `y` is derived
	# from `x`.
	edges = []
	# Iterate over locations in the trace; each will be a subgraph.
	for location, scopes in data.items():
	print(f"subgraph {location}")
	# Iterate over scopes in this location; each will be a subgraph.
	for scope, keys in scopes.items():
	print(f"subgraph {location}.{scope}")

	# Iterate over keys in this scope; each will be a node.
	for x in keys:
	# Save the key's definition at its fully-specified path so that we
	# can trace its dependencies.
	path = f"{location}.{scope}.{x}"
	nodes[path] = keys[x]
	nodes[path]["deps"] = set()

	# Iterate over the key's dependencies; each will be an edge.
	x_from = keys[x].get("from", [])
	for y_path in x_from:
	# Build the dependency's fully-specified path so that we can
	# refer to it globally.
	y_location, y_scope, y = y_path.split(".")

	# Identities were received from another location, which will be
	# indicated with a graph edge.
	if y != x:
	nodes[path]["deps"].add(y)
	elif y_location == location and y_scope != scope:
	raise ValueError(
	f"{path} is reused across local scopes at {y_path}"
	)
	# Otherwise, dependencies accumulate transitively within a
	# location.
	nodes[path]["deps"] \|= nodes.get(y_path, {}).get("deps", set())

	arrow = "-->"
	# Mark "encryptions" by contact with a public key.
	if "PK" in y and y != x:
	nodes[path]["encrypted"] = True
	arrow = "--o"
	# Mark "decryptions" by contact with a secret key.
	elif "SK" in y and y != x:
	nodes[path]["decrypted"] = True
	arrow = "--x"

	edges.append(f"{y_path} {arrow} {location}.{scope}.{x}")

	# Output the node's definition, including all local dependencies for
	# this path.
	deps = ""
	if len(nodes[path]["deps"]) > 0:
	deps = " ←<br>" + "<br>".join(sorted(nodes[path]["deps"]))
	if "encrypted" in nodes[path] and "decrypted" in nodes[path]:
	print(f"{path}(({x}{deps}))")
	elif len(x_from) == 0:
	print(f"{path}>{x}{deps}]")
	else:
	print(f"{path}[{x}{deps}]")

	print("end") # scope subgraph
	print("end") # location subgraph

	# Output all the edges at the end, since they belong to the global graph.
	print("\n".join(edges))
	journalist: # Location (or role): Where is this value (who has it)?
	long-term: # Scope: What is the lifetime of this value? How long/far is it it applicable?
	# key: name of value
	# from: list of other `{location}.{scope}.{key}` paths on which this path
	# (this key, in this scope, at this location) depends
	J_SK: {}
	J_PK:
	from:
	- journalist.long-term.J_SK
	JC_SK: {}
	JC_PK:
	from:
	- journalist.long-term.JC_SK
	per-message:
	JE_SK: {}
	JE_PK:
	from:
	- journalist.per-message.JE_SK
	message_id:
	from:
	- journalist.per-request.kmid
	- journalist.per-request.enc_m_id
	message_ciphertext:
	from:
	- server.per-message.message_ciphertext
	ME_PK:
	from:
	- server.per-message.ME_PK
	k:
	from:
	- journalist.per-message.ME_PK
	- journalist.per-message.JE_SK
	m:
	from:
	- journalist.per-message.k
	- journalist.per-message.message_ciphertext
	S_PK:
	from:
	- journalist.per-message.m
	SC_PK:
	from:
	- journalist.per-message.m
	message:
	from:
	- journalist.per-message.m
	per-request:
	pmgdh:
	from:
	- server.per-request.pmgdh
	enc_m_id:
	from:
	- server.per-request.enc_m_id
	kmid:
	from:
	- journalist.per-request.pmgdh
	- journalist.long-term.JC_SK

	source:
	long-term:
	J_PK:
	from:
	- journalist.long-term.J_PK
	JC_PK:
	from:
	- journalist.long-term.JC_PK
	JE_PK:
	from:
	- journalist.per-message.JE_PK
	S_SK: {}
	S_PK:
	from:
	- source.long-term.S_SK
	SC_SK: {}
	SC_PK:
	from:
	- source.long-term.SC_SK
	per-message:
	ME_SK: {}
	ME_PK:
	from:
	- source.per-message.ME_SK
	k:
	from:
	- source.per-message.ME_SK
	- journalist.per-message.JE_PK
	message: {}
	m:
	from:
	- source.per-message.message
	- source.long-term.S_PK
	- source.long-term.SC_PK
	message_ciphertext:
	from:
	- source.per-message.k
	- source.per-message.m
	message_gdh:
	from:
	- journalist.long-term.JC_PK
	- source.per-message.ME_SK

	server:
	per-message:
	message_ciphertext:
	from:
	- source.per-message.message_ciphertext
	message_gdh:
	from:
	- source.per-message.message_gdh
	ME_PK:
	from:
	- source.per-message.ME_PK
	message_id: {}
	per-request:
	RE_SK: {}
	RE_PK:
	from:
	- server.per-request.RE_SK
	kmid:
	from:
	- source.per-message.message_gdh
	- server.per-request.RE_SK
	pmgdh:
	from:
	- source.per-message.ME_PK
	- server.per-request.RE_SK
	enc_m_id:
	from:
	- server.per-request.kmid
	- server.per-message.message_id