[Verifpal] Threats scenarios modelled, information in the tool help output

Nadim Kobeissi nadim at symbolic.software
Sat Apr 11 09:32:05 CEST 2020


Dear Anders,

This is why the Verifpal User Manual exists.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Sat, Apr 11, 2020 at 9:08 AM Pittsburgh penguins Tv via Verifpal
<verifpal at lists.symbolic.software> wrote:

> Dear Nadim,
> would it be possible to add in the 'verifpal help' which threat scenarios
> the tool takes into consideration, for the particular release? Is replay
> attack modelled? and similar information.
>
> Best regards
> Anders N.
>
>
> attacker [active]
>
> principal Alice[
>     knows private a
>     ha = HASH(a)
> ]
>
> Alice -> Bob: ha
>
> principal Bob[
>     knows private a
>     _ = ASSERT(ha, HASH(a))
> ]
>
> queries[
>     confidentiality? a
>     authentication? Alice -> Bob: ha
> ]
>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200411/1a513e92/attachment.htm>


More information about the Verifpal mailing list