[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:

attacker[active]

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) ]

queries[
    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?

Best,
Friedrich

--
Dr. Friedrich Wiemer,
orcid.org/0000-0003-2998-6777 
-------------- 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