Clarify plaintext NFC visibility in the remote AA examples

examples/epassport/remote_aa.vp

@@ -12,10 +12,12 @@
 // The phone reaches the service the way a browser reaches a server: it
 // sends a fresh channel key encrypted to the service's public key, which it
 // knows authentically, and both directions then travel under that key. The
-// service does not authenticate the phone. NFC between phone and chip is
-// guarded: the attacker is somewhere on the internet, not near the passport.
-// The bank opens the answer and checks the chip's signature in one step, so
-// that the first use of the answer is the bank's decision.
+// service does not authenticate the phone. In this model, the attacker can
+// interfere with the internet connection and read the plaintext NFC
+// exchange between phone and chip, including aaSig. NFC messages are guarded
+// against replacement; BAC/PACE Secure Messaging is not modeled on this
+// link. The bank opens the answer and checks the chip's signature in one
+// step, so that the first use of the answer is the bank's decision.
 //
 // The holder may also be asked to prove their identity to a dishonest
 // service. The scenarios[] block gives the phone two configurations: the

examples/epassport/remote_aa_bound.vp

@@ -22,11 +22,13 @@
 // nChal. That nonce reuse lets it forge a chalMsg on the phone's channel
 // carrying the challenge of a third bank run, one it opened with its own
 // channel key. The phone, which is connected to the bank, hashes bankPub
-// with that challenge, the chip signs, and the attacker presents the
-// signature in its own run, where the bank accepts it. A TLS server
-// contributes fresh values to the channel keys, so a replayed key message
-// would not give two server runs the same keys; this channel is weaker
-// than TLS.
+// with that challenge, and the chip signs. The attacker then reads aaSig
+// from the guarded NFC exchange and encrypts it for its own bank run,
+// where the bank accepts it. This trace requires the attacker to learn the
+// plaintext aaSig from the modeled NFC link, in addition to exploiting
+// nonce reuse on the phone-bank connection. A TLS server contributes fresh
+// values to the channel keys, so a replayed key message wouldn't give two
+// server runs the same keys; this channel is weaker than TLS.
 
 attacker[active]