diff --git a/examples/epassport/remote_aa.vp b/examples/epassport/remote_aa.vp index bfdcd015..141e1601 100644 --- a/examples/epassport/remote_aa.vp +++ b/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 diff --git a/examples/epassport/remote_aa_bound.vp b/examples/epassport/remote_aa_bound.vp index f2ca145d..3e2b91a8 100644 --- a/examples/epassport/remote_aa_bound.vp +++ b/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]