[Verifpal] Crash when sending an already known value within concat and checking it with assert

Friedrich Wiemer friedrich.wiemer at rub.de
Wed Oct 21 22:18:45 CEST 2020

Here is another crashing model:


principal Client[
    generates skc
    pkc = G^skc
principal Server[
    generates sks
    pks = G^sks
Server -> Client: [pks]
principal Client[
    generates nc
    mcs = CONCAT(pkc, nc, pks)
Client -> Server: pkc, mcs
principal Server[
    pkc_recv, nc_recv, pks_recv = SPLIT(mcs)
    _ = ASSERT(pks, pks_recv)?
    generates ns
Server -> Client: ns
principal Client[ kcs = HASH(ns) ]

    authentication? Client -> Server: mcs
    authentication? Server -> Client: ns
    confidentiality? kcs

This seems to be related to sending the already known value 'pkS' to the server and then having the server check 'ASSERT(pks, pks_recv)'. Note that sending the already known value only works, because its "hidden" inside the concat. Maybe this should be handled similarly to sending the values directly, or does that not make sense?


Dr. Friedrich Wiemer,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20201021/791cc7f4/attachment.htm>

More information about the Verifpal mailing list