[Verifpal] parser attack (1 of 2)

[Nadim Kobeissi]

Dear Mike,

Thank you very much for reporting these parsing errors. I’ve fixed them in the latest commit to the master branch.

I very much appreciate your contributing to Verifpal, and hope that you will conduct more testing and discover more issues that we can fix.

Looking forward to hearing from you again,

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

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