adds a description of the DH and SSM Agent implementations to the respective READMEs

Author: ArquintL

README.md

@@ -29,14 +29,14 @@ git submodule update --init --recursive -- ar-go-tools ssm-agent
 Whenever we refer to the SSM Agent, we mean the fork of the SSM Agent codebase that implements the protocol for establishing encrypted interactive shell sessions.
 
 - `ssm-agent/model` contains the Tamarin model of the protocol used by the SSM Agent to establish interactive shell sessions
-- `ssm-agent/implementation` contains the entire SSM Agent codebase.
+- `ssm-agent/implementation` contains the entire SSM Agent codebase and the corresponding [README](https://github.com/ArquintL/amazon-ssm-agent/tree/update-diodon?tab=readme-ov-file#secure-sessions-overview) provides an overview.
     - `ssm-agent/implementation/agent/session/datachannel` contains the Go package representing the CORE.
 - `ssm-agent/argot-proofs` contains the scripts used to verify the SSM Agent with Argot.
 
 
 ### Diffie-Hellman (DH) Implementation
 - `dh/model` contains the Tamarin model of the protocol used by the DH implementation to perform a DH key exchange
-- `dh/implementation` contains the entire DH codebase.
+- `dh/implementation` contains the entire DH codebase and the corresponding [README](dh/implementation/README.md) provides an overview over the codebase.
     - `dh/implementation/library` and `dh/implementation/initiator` contain the Go packages representing the CORE.
 - `dh/argot-proofs` contains the scripts used to verify the DH implementation with Argot.
 

dh/implementation/README.md

@@ -1,5 +1,16 @@
 # Go Diffie-Hellman Implementation
 
+## Implementation Overview
+`main.go` represents the App that performs all I/O.
+The Core is implemented in `initiator/initiator.go`.
+More specifically, the `Initiator` struct stores all state related to a protocol session.
+In addition, this file provides methods with the `Initiator` struct being the receiver to produce outgoing and consume incoming messages.
+We prove (using Gobra) that producing and consuming these messages correspond to steps in the protocol model.
+This allows us to treat outgoing messages as being untainted from a taint analysis point of view, such that the corresponding I/O operation in the App satisfies I/O independence.
+For this purpose, `library/io.go` provides a function `PerformVirtualOutputOperation` that enforces (via its specification) that a caller gives up an I/O permission for sending a message.
+Thus, we configure the taint analysis (in `../argot-proofs/argot-config-dh.yaml`) to treat this function as a sanitizer, i.e., that this returns untainted data.
+
+
 ## Building & Running the Initiator Role
 Build:
 ```