improves formatting

Author: ArquintL

README.md

@@ -45,7 +45,7 @@ More specifically, our claims are as follows:
 - [Claim 5](claims/claim5/claim.md): The Protocol Model for the signed Diffie-Hellman key exchange satisfies forward secrecy & injective agreement
 - [Claim 6](claims/claim6/claim.md): The Diffie-Hellman case study satisfies I/O independence
 - [Claim 7](claims/claim7/claim.md): The Gobra program verifier successfully verifies the CORE in the Diffie-Hellman case study
-- [Claim 8](claims/claim8/claim.md): The APPLICATION in the Diffie-Hellman case study satisfies conditions (C1)--(C4) and (C6)--(C8)
+- [Claim 8](claims/claim8/claim.md): The APPLICATION in the Diffie-Hellman case study satisfies conditions (C1)-(C4) and (C6)-(C8)
 - [Claim 9](claims/claim9/claim.md): Our tools detect deliberately seeded bugs in both case studies
 
 Alternatively, we describe next how to manually run the Docker image and interact with the Docker container.

claims/claim1/claim.md

@@ -1,4 +1,4 @@
-# Claim 1 -- Protocol Model for SSM Agent
+# Claim 1 - Protocol Model for SSM Agent
 As described in Sec. 5.1.1, we model the security protocol for establishing a remote shell session between an SSM Agent running on an AWS EC2 instance and an AWS customer in Tamarin and prove (1) secrecy for the two symmetric session keys and (2) injective agreement on the SSM Agent's and AWS customer's identities and the session keys.
 
 `run.sh` supports this claim by invoking Tamarin on the protocol model stored in `ssm-agent/model/protocol-model.spthy` and proving all lemmas stated therein.

claims/claim2/claim.md

@@ -1,4 +1,4 @@
-# Claim 2 -- I/O Independence for SSM Agent
+# Claim 2 - I/O Independence for SSM Agent
 As described in Sec. 5.1.2, we successfully execute a taint analysis on the entire SSM Agent codebase to prove that all I/O operations within the APPLICATION are independent of protocol-relevant secrets.
 
 `run.sh` supports this claim by executing the taint analysis. The taint analysis uses the configuration `ssm-agent/argot-proofs/argot-config-agent.yaml`, in particular the configuration under key `dataflow-problems`. This configuration specifies that the analysis considers implicit flows, that the `GenerateKey` function in the `crypto/elliptic` package is a source of taint, and all functions that are treated as sinks. Since the taint analysis errors if taint flows from the source to any sink, successful execution of the analysis proves that there are no taint flows.

claims/claim3/claim.md

@@ -1,4 +1,4 @@
-# Claim 3 -- Core Refinement for SSM Agent
+# Claim 3 - Core Refinement for SSM Agent
 As described in Sec. 5.1.3, we identified the `datachannel` package as the SSM Agent's CORE and successfully verify this package using the Gobra program verifier.
 
 `run.sh` supports this claim by running Gobra to verify the `datachannel` package. This proves that all protocol-relevant I/O operations within the CORE are permitted by the protocol model that we verified in Tamarin and that we have a correct proof in separation logic for the verified methods in this package.

claims/claim4/claim.md

@@ -1,6 +1,6 @@
-# Claim 4 -- Analyzing the Application for SSM Agent
-As described in Sec. 5.1.4, we implemented static analyses checking conditions (C1)--(C4) and (C6)--(C8) (as stated in Sec. 4.3).
-The conditions (C1)--(C8) ensure that callers of the CORE (which is verified by Gobra, cf. claim 3) satisfy the preconditions of CORE methods.
+# Claim 4 - Analyzing the Application for SSM Agent
+As described in Sec. 5.1.4, we implemented static analyses checking conditions (C1)-(C4) and (C6)-(C8) (as stated in Sec. 4.3).
+The conditions (C1)-(C8) ensure that callers of the CORE (which is verified by Gobra, cf. claim 3) satisfy the preconditions of CORE methods.
 In particular, we implemented a pass-through analysis to check conditions (C1), (C3), and (C8) and an escape analysis for conditions (C4) and (C6).
 Furthermore, we use a pointer analysis to check condition (C7) and an immutability analysis based on the pointer analysis to check condition (C2).
 As mentioned in Sec. 5.1.4, our escape analysis fails as it detects that a CORE instance and a thread-safe logger object escapes the thread in which it got created, and our pass-through analysis is a prototype reporting many false positives.

claims/claim5/claim.md

@@ -1,4 +1,4 @@
-# Claim 5 -- Protocol Model for Diffie-Hellman
+# Claim 5 - Protocol Model for Diffie-Hellman
 As described in Sec. 5.2, we model the security protocol for the signed Diffie-Hellman key exchange in Tamarin and prove (1) forward secrecy for the two symmetric session keys and (2) injective agreement on the identities of the two involved protocol role instances and the session keys.
 
 `run.sh` supports this claim by invoking Tamarin on the protocol model stored in `dh/model/protocol-model.spthy` and proving all lemmas stated therein.

claims/claim6/claim.md

@@ -1,4 +1,4 @@
-# Claim 6 -- I/O Independence for Diffie-Hellman
+# Claim 6 - I/O Independence for Diffie-Hellman
 As described in Sec. 5.2, we successfully execute a taint analysis on the Diffie-Hellman codebase to prove that all I/O operations within the APPLICATION are independent of protocol-relevant secrets.
 
 `run.sh` supports this claim by executing the taint analysis. The taint analysis uses the configuration `dh/argot-proofs/argot-config-dh.yaml`, in particular the configuration under key `dataflow-problems`. This configuration specifies that the analysis considers implicit flows, that the `parsePrivateKey` and `createNonce` functions are sources of taint, and all functions that are treated as sinks. Since the taint analysis errors if taint flows from the source to any sink, successful execution of the analysis proves that there are no taint flows.

claims/claim7/claim.md

@@ -1,4 +1,4 @@
-# Claim 7 -- Core Refinement for Diffie-Hellman
+# Claim 7 - Core Refinement for Diffie-Hellman
 As described in Sec. 5.2, we successfully verify the CORE (package `initiator`) the using the Gobra program verifier.
 
 `run.sh` supports this claim by running Gobra to verify the `initiator` package. This proves that all protocol-relevant I/O operations within the CORE are permitted by the protocol model that we verified in Tamarin and that we have a correct proof in separation logic for the verified methods in this package.

claims/claim8/claim.md

@@ -1,4 +1,4 @@
-# Claim 8 -- Analyzing the Application for Diffie-Hellman
-As described in Sec. 5.2, we successfully execute the immutability, escape, pointer, and pass-through analyses on the Diffie-Hellman case study, which establishes the conditions (C1)--(C4) and (C6)--(C8) (as stated in Sec. 4.3).
+# Claim 8 - Analyzing the Application for Diffie-Hellman
+As described in Sec. 5.2, we successfully execute the immutability, escape, pointer, and pass-through analyses on the Diffie-Hellman case study, which establishes the conditions (C1)-(C4) and (C6)-(C8) (as stated in Sec. 4.3).
 
 `run.sh` supports this claim by running these analyses.

claims/claim9/claim.md

@@ -1,4 +1,4 @@
-# Claim 9 -- Soundness
+# Claim 9 - Soundness
 As described in Sec. 5.3, we deliberately introduce bugs in our case studies and check that our tools fail as expected.
 
 `run.sh` supports this claim by seeding bugs in