# 1 "fail1.eva"

NEW
 A, B : principal
 N : number
 K : key
 A knows A, B, K
 B knows B
 a, b : principal
 {
  1. A -> B : A, { N }_K
  2. B -> A : N
 }
 s. session A=a, B=b