Need suggestions about alternative modeling to avoid using restrictions in --diff mode

[Yuheng Wen]

Hi Group,

I am modelling a multi-party protocols involving corruptions, key ratcheting, and trust actions to prove unlinkability using observational equivalence mode. I originally used two restrictions to control what users can be selected for entering the "challenge" rule. But later I realized restrictions are not recommended in --diff mode. I am wondering if anyone knows a good alternative way of modelling to avoid using restrictions in this case? 

Thank you!

Yuheng

theory time_alternative

begin

/* this file does not create time action for In, but just give the power to In itself in a open channel */

/* We do not assume In have the power to obtain blinded public keys in this model

1. We do not consider how the topologies of message broadcating affect the anonymity

2. Used standard signature specification

3. Used one rule for Trust (no follow and accept) */

builtins: multiset

functions: sign/2, pk/1, verify/3, true/0, false/0 //sign(m, sk), pk(sk), verify(sig, m, pk)

equations: verify(sign(m, k), m, pk(k)) = true()

restriction corrupt_after_chall_1:

"All corrupt_time uct1 uct2 signtime id1 id2 #i #j. SignedTime(signtime, uct1, uct2, id1, id2) @ #i & CorruptPK(id1,corrupt_time)@#j ==> Ex x. signtime + x = corrupt_time"

restriction corrupt_after_chall_2:

"All corrupt_time uct1 uct2 signtime id1 id2 #i #j. SignedTime(signtime, uct1, uct2, id1, id2) @ #i & CorruptPK(id2,corrupt_time)@#j ==> Ex x. signtime + x = corrupt_time"

// "Ratcheted" is a action fact used to track when things are ratcheted so one cannot

// ratchet to the same time twice

restriction ratchet_once:

"All id t lsk1 lpk1 lsk2 lpk2 #i #j. Ratcheted(id, t, lsk1, lpk1) @ #i & Ratcheted(id, t, lsk2, lpk2) @ #j ==> lsk1 = lsk2 & lpk1 = lpk2"

restriction OnlyOnce:

"All #i #j. OnlyOnce()@#i & OnlyOnce()@#j ==> #i = #j"

restriction OnlyOnce_Corrupt_TrustedKey:

"All id1 id2 lpk1 trust_time #i #j. OnlyOnce_Corrupt_TrustedKey(id1, id2, lpk1, trust_time) @ #i & OnlyOnce_Corrupt_TrustedKey(id1, id2, lpk1, trust_time) @ #j ==> #i = #j"

restriction OnlyOnce_Trust:

"All id1_lpk #i #j. OnlyOnce_Trust(id1_lpk) @ #i & OnlyOnce_Trust(id1_lpk) @ #j ==> #i = #j"

rule KeyGen:

let lpk = pk(~lsk) in

[Fr(~lsk)]-->

[InitKeys(~lsk,lpk)]

rule CreateUser:

[Fr(~id),

InitKeys(id_lsk,id_lpk),

In(t)]

--[Ratcheted(~id, t, id_lsk, id_lpk), Created(~id, id_lsk, id_lpk), Created1(~id, id_lpk)]->

[!User(~id, id_lsk, id_lpk, t), // honestok = honest own key, false = holder for corrupt time

!Ratchet(~id,t, id_lsk,id_lpk),

Out(<~id, t>)] // user id is public so that In can pick any user for actions below

rule Ratchet: // create a public key at time t for id, stored in fact Ratchet()

[In(id),

In(t),

Fr(~lsk)]

--[Ratcheted(id, t, ~lsk, pk(~lsk))]->

[!Ratchet(id, t, ~lsk, pk(~lsk))]

rule GetRatchetKey: // adv can ratchet the public key from a known public key

let

wut = t + stept // wut = want user's time after this tick

in

[In(lpk),

In(stept),

!Ratchet(id,t,lsk,lpk),

!Ratchet(id,wut,lsk_new,lpk_new)] // variable name's scope is limited within one rule, so we can match id

--[GetRatchet(id, lpk_new)]->

[Out(lpk_new)]

rule Trust: // id1 trusts id2

[In(<id1, uct1>), // can pick any honest or corrupted users

In(<id2, uct2>),

!User(id1, id1_lsk, id1_lpk, uct1),

!User(id2, id2_lsk, id2_lpk, uct2)

]--[TrustOK(id1, id1_lsk, id1_lpk, id2, id2_lsk, id2_lpk), OnlyOnce_Trust(id1_lpk)]-> // once per public key

[Trust(id1, id2, id1_lpk, uct1)

]

rule Tick: //update chosen user's own public and secret keys

let

wut = uct + stept // wut = want user's time after this tick

in

[In(stept), // stept = step time

In(<id, uct>),

!User(id, lsk, lpk, uct), // uct = user current time

!Ratchet(id, wut, new_lsk, new_lpk)]

--[TickTime(uct, wut, stept)]->

[!User(id, new_lsk, new_lpk, wut),

Out(<id, wut>)] // here we make sure keys stored in Ratchet fact and User fact won't collide

rule Tick_trust: //update chosen user's chosen key from truster's keys list

let

wut1 = uct1 + stept

in

[In(id2),

In(id1),

In(stept),

Trust(id1, id2, id1_lpk, uct1),

!Ratchet(id1, wut1, new_id1_lsk, new_id1_lpk)

]--> [Trust(id1, id2, new_id1_lpk, wut1)]

rule Corrupt_ownkey: //can't corrupt earlier keys through this rule (i.e. corrupt only once)

[In(<id, uct>),

!User(id, lsk, lpk, uct)]--[CorruptPK(id, uct)]->

[Out(<lpk,lsk, id, uct>)]

rule Corrupt_trustedkey: // id1's public key (stored within id2) is corrupted, id1's key firstly been known

[In(id1),

In(id2),

Trust(id1, id2, id1_lpk, trust_time)]

--[CorruptPK(id1, trust_time), Corrupt_trustedkeyOK(id1, id1_lpk), OnlyOnce_Corrupt_TrustedKey(id1, id2, id1_lpk, trust_time)]->

[Out(<id1, id1_lpk, trust_time>),

Trust(id1, id2, id1_lpk, trust_time)

]

rule sig_diff:

let

sig = sign(~m, lsk_signed)

sig1 = sign(~m1, lsk1_signed)

in

[

In(t), // time of signing

//user 1

Fr(~m),

In(id),

!User(id, lsk, lpk, uct),

!Ratchet(id, t, lsk_signed, lpk_signed),

//user 2

Fr(~m1),

In(id1),

!User(id1, lsk1, lpk1, uct1),

!Ratchet(id1, t, lsk1_signed, lpk1_signed)

]--[OnlyOnce(), SignedTime(t, uct, uct1,id,id1), DidChall(t,id,id1)]-> // even though some time is not comparable, this rule only fires when two times are indeed comparable (forcing two time stem from two comparable set)

[Out(diff(sig, sig1))]

lemma executable_chall: // proven

exists-trace

"Ex t id id1 #i. DidChall(t,id,id1) @ #i"

lemma executable_Tick: // proven

exists-trace

"Ex uct wut stept #i. TickTime(uct, wut, stept) @ #i "

lemma executable_Ratchet: // proven

exists-trace

"Ex id t lsk lpk #i. Ratcheted(id, t, lsk, lpk) @ #i "

lemma executable_GetRatchetKey: // proven

exists-trace

"Ex id lpk_new #i. GetRatchet(id, lpk_new) @ #i "

lemma executable_Trust: // proven

exists-trace

"Ex id1 id1_lsk id1_lpk id2 id2_lsk id2_lpk #i. TrustOK(id1, id1_lsk, id1_lpk, id2, id2_lsk, id2_lpk) @ #i "

en