[Verifpal] Runtime for analysis?

Friedrich Wiemer friedrich.wiemer at rub.de
Mon Mar 2 20:46:08 CET 2020


Hi,

I expect I now have a working model of the Needham-Schroeder protocol in
verifpal (see attached). When I run verifpal on this, it seems to run
very long at "Step 4, Analysis 430..." (I have started the same run on a
remote server, to see if there is an output in some hours.)

I assume that sometime (often?) the analysis runtime is quite high, so
this might be expected. But is it possible to get some information, if
verifpal is still working as expected?

Best,
Friedrich

-- 
Dr. Friedrich Wiemer,
Research Assistant

Symmetric Cryptography
Horst Goertz Institute for IT-Security,
Ruhr-University Bochum,

orcid.org/0000-0003-2998-6777
-------------- next part --------------
attacker[active]

principal Server[
    knows private k_sa
    knows private k_sb
    knows private k_ab
]
principal Alice[
    knows private k_sa
]
principal Bob[
    knows private k_sb
]

principal Alice[
    generates A
    generates B
    generates Na
]
Alice -> Server: A, B, Na

principal Server[
    m_bob = CONCAT(k_ab, A)
    e_bob = AEAD_ENC(k_sb, m_bob, nil)

    m_alice = CONCAT(k_ab, B, Na, e_bob)
    e_alice = AEAD_ENC(k_sa, m_alice, nil)
]
Server -> Alice: e_alice

principal Alice[
    e_alice_dec = AEAD_DEC(k_sa, e_alice, nil)?
    k_ab_dec_alice, B_dec, Na_dec, e_bob_dec = SPLIT(e_alice_dec)
]
Alice -> Bob: e_bob_dec

principal Bob[
    e_bob_decdec = AEAD_DEC(k_sb, e_bob_dec, nil)?
    k_ab_dec_bob, A_dec = SPLIT(e_bob_decdec)

    generates Nb
    eNb = AEAD_ENC(k_ab_dec_bob, Nb, nil)
]
Bob -> Alice: eNb

principal Alice[
    Nb_dec = AEAD_DEC(k_ab_dec_alice, eNb, nil)?
    Nb_minus_one = HASH(Nb_dec)
    eNb_minus_one = AEAD_ENC(k_ab_dec_alice, Nb_minus_one, nil)
]
Alice -> Bob: eNb_minus_one

principal Bob[
    Nb_minus_one_dec = AEAD_DEC(k_ab_dec_bob, eNb_minus_one, nil)?
    _ = ASSERT(Nb_minus_one_dec, HASH(Nb))?
]

queries[
    confidentiality? k_ab
    authentication? Alice -> Bob: eNb_minus_one
    authentication? Bob -> Alice: eNb
]
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200302/759f944e/attachment.sig>


More information about the Verifpal mailing list