[Verifpal] global scope

Mike tankf33der at disroot.org
Sat Sep 7 21:28:36 CEST 2019

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.

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 []                                                                      

More information about the Verifpal mailing list