[Verifpal] parser attack (1 of 2)

[Mike]

hi all,

As warmup before Monokex verification I decided to *attack* verifpal parser.


1. verifpal compiled from sources under master
2. Besides runtime crash check how I tricked the parser and used root generator on right side (forbidden):
b = a^G
3. if change line to "attacker[passive]" verifpal successfully exits.
 


$ verifpal verify crash-c.vp 
Verifpal 0.4.1 (go1.12.9)
© 2019 Symbolic Software — https://verifpal.com
WARNING: Verifpal is experimental software.

 Verifpal! parsing model...
 Verifpal! verification initiated at 17:32:55
 Analysis! Bob has sent c to Alice, rendering it public
     Info! attacker is configured as active
Deduction! c resolves to G^
panic: runtime error: index out of range

goroutine 1 [running]:
main.verifyActiveValueHasFreshValues(0xc0000c8600, 0x50a16d, 0x8, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, ...)
	/home/mpech/verifpal/internal/app/verifpal/verifyactive.go:121 +0x462
main.verifyActiveClearFreshValues(0xc00009e040, 0xc0000c8600, 0xc0000d5bc8, 0xc0000d5bc8)
	/home/mpech/verifpal/internal/app/verifpal/verifyactive.go:89 +0x1e8
main.verifyActive(0xc00009e040, 0xc0000c8600, 0x0, 0x0, 0x50a1bd)
	/home/mpech/verifpal/internal/app/verifpal/verifyactive.go:39 +0x33f
main.verify(0xc00009e040, 0xc0000c8600, 0xc00009e040, 0xc0000c8600, 0x1)
	/home/mpech/verifpal/internal/app/verifpal/verify.go:25 +0x477
main.main()
	/home/mpech/verifpal/internal/app/verifpal/main.go:43 +0x2f5


===
attacker[active]                                                                
                                                                                
principal Bob[                                                                  
    generates v                                                                 
    a = G^v                                                                     
    b = a^G                                                                     
    c = G^b                                                                     
]                                                                               
principal Alice[]                                                               
                                                                                
Bob -> Alice: c                                                                 
                                                                                
principal Alice[                                                                
    v1 = G^c                                                                    
]                                                                               
queries [                                                                       
    authentication? Bob -> Alice: c                                             
]
===

                   

p.s. Verifpal is promising and like fresh air. My congratulations.


(mike)