[Verifpal] global scope

[Nadim Kobeissi]

Dear Mike,

I’m very grateful for this continued feedback. This parsing error has also been addressed. Keep them coming!

Thanks again,

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Sep 7, 2019, at 9:28 PM, Mike via Verifpal <verifpal at lists.symbolic.software> wrote:
> 
> 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)
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal