hi all,
This file successfully verified, Im expecting error.
'a' is already in global scope via Bob and cant be created inside Alice.
As example, cases 1-3 creates 'a' in different ways and all fails as expected and handled.
===
attacker[active]
principal Bob[
generates v
a = G^v
]
principal Alice[]
Bob -> Alice: a
principal Alice[
// 0.
knows private a
// 1. constant assigned twice (a)
//generates k
//a = G^k
// 2. known more than once and in different ways (a)
//knows public a
// 3. constant generated twice (a)
//generates a
]
queries []
===
(mike)