[Verifpal] parser attack (1 of 2)

Mike tankf33der at disroot.org
Sat Sep 7 16:56:34 CEST 2019

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
	/home/mpech/verifpal/internal/app/verifpal/main.go:43 +0x2f5

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.


More information about the Verifpal mailing list