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

Nadim Kobeissi nadim at symbolic.software
Sat Apr 11 10:10:03 CEST 2020


No, it isn't. Replay attacks are among other classes of things, such as
observational equivalence, that we want Verifpal to address this year. We
can add a small list in the user manual as to what's not covered yet, but
this sort of stuff doesn't go into the command-line documentation for the
tool itself.

If you wish to continue discussing this, please do so off-list, this isn't
a topic worth blasting to all the mailing list subscribers.

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


On Sat, Apr 11, 2020 at 9:52 AM Pittsburgh penguins Tv <
anderswnilson at gmail.com> wrote:

> Dear Nadim,
> when searching for 'replay', as an example, it's not found in the manual.
> Wouldn't it be easier to provide such information directly at the command
> prompt?
>
> Best regards
> Anders N.
>
> Den lör 11 apr. 2020 kl 09:32 skrev Nadim Kobeissi <nadim at symbolic.software
> >:
>
>> 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/d0813135/attachment.htm>


More information about the Verifpal mailing list