`SIGNVERIF` with original value (like proof-of-identity)

[cobratbq]

I want to prove the identity of one party through signing an arbitrary value provided by the other party.

Either:

• I do not know/have the appropriate query to express this verification, or
• the SIGN/SIGNVERIF pair of operations does not work with all available guarantees (i.e. n from both parties must be same if SIGNVERIF succeeds), or
• verification prematurely fails with conclusion that SIGN received malicious n

Furthermore, it isn't clear whether the query authentication? Bob -> Alice: n means "Alice is convinced that the n that Bob sent is authentic", or that it means "the n that Bob sent to Alice remains/arrived unchanged, i.e. is authentic". One takes a particular principal into the equation, while the other takes the perspective of the variable.

Goal: express/prove that n has remained unchanged as confirmed by Bob through signature verification? (Therefore, Bob knows that "Alice" is the Alice of the identity (sk, pk) and that she received the unchanged n.)

Clarification to the script below:

• assume sending [pk] was done some other time, in another way, some other channel. This is the way I know to model known information between parties.
• at the end of this sample, Bob has initiative. The sample is a (reduced) part of a larger protocol where Bob next needs to decide whether or not to continue.

attacker[active]
principal Alice[
    knows private sk
    pk = G^sk
]
Alice -> Bob: [pk]
principal Bob[
    generates n
]
Bob -> Alice: n
principal Alice[
    sig = SIGN(sk, n)
]
Alice -> Bob: sig
principal Bob[
    _ = SIGNVERIF(pk, n, sig)?
]

queries[
    confidentiality? sk
    authentication? Alice -> Bob: sig
    // The protocol detects when 'n' is not authentic, because Alice's signature will fail to verify against Bob's (original) 'n'.
    authentication? Bob -> Alice: n
]

See mailinglist conversation for more details and elaboration.