editorial polishing

device-bound-key-pair.pv

@@ -164,7 +164,7 @@ EncompassingAuthenticationAssertionToBeSigned: {     // signed by the user crede
 
                 AuthDataForDevicePublicKeyAttestationToBeSigned: {
                     rpIdHash
-                    AAGUID                  // where do we get this from?
+                    AAGUID                  // where do we get this from if it is not conveyed in authData?
                     userCredentialIdLength  //   "   "  "   "   "    "
                     userCredentialId        //   "   "  "   "   "    "
                     devicePublicKey         //   "   "  "   "   "    "
@@ -236,7 +236,7 @@ reduc forall x: bitstring, k: key; sdec(senc(x,k),k) = x.
 
 (*User's ID  and Server's ID*)
 const cert:bitstring [private].
-const a:RP_id [private].
+const a:RP_id [private]. (* server's identity *)
 const credentialID2:bitstring [private].
 
 (*Table*)
@@ -254,10 +254,15 @@ query attacker(attskU).
 free attpkU: AttestationPublicKey[private].
 query attacker(attpkU).
 
-const k:key.
+const k:key. (* TLS record layer symmetric encryption key *)
+
+
 let processUser ( k: key,cert:bitstring, attskA: AttestationPrivatekey, attpkA:AttestationPublicKey) =
+
     (*Registration*)
-    in(c,s:bitstring);
+
+    in(c,s:bitstring); (* server sent
+
     let(challengeU:nonce, aU:RP_id)= sdec(s,k) in
     new skU:skey;
     let pkU = spk(skU) in
@@ -269,11 +274,10 @@ let processUser ( k: key,cert:bitstring, attskA: AttestationPrivatekey, attpkA:A
 let processServer (k: key, a:RP_id) =
 
     (*Registration*)
-    new challenge:nonce;
 
-    new attpkU3: AttestationPublicKey;
-    let ver1=(challenge,a) in
-    out(c, senc((challenge,a),k));
+    new challenge: nonce;
+
+    out(c, senc( (challenge, a), k) ); (* send challenge & RP_id over TLS *)
 
     in(c, s:bitstring);