SAPIC+ Channel Questions

[Daniel Zimmerman]

Hi! This is the first of a few (more) questions I'm going to be posting about SAPIC+, SAPIC+ translation to ProVerif, and how constructs like channels, state, etc. are meant to be understood.

I wrote a fairly simple example that uses a private channel, and some lemmas that I thought would be straightforward to prove:

theory test_private_channels begin

let reader(sc: channel) = (

in(sc, x);

event Read(x);

out(sc, 'newstate')

)

process:(

new sc: channel;

(

out(sc, 'oldstate') ||

!reader(sc)

)

)

lemma ExOld:

exists-trace

"Ex #i. Read('oldstate')@i"

lemma ExNew:

exists-trace

"Ex #i. Read('newstate')@i"

lemma AlwaysOldOrNew:

"All x #i. Read(x)@i ==> x = 'oldstate' | x = 'newstate'"

lemma OldThenNew:

"All #i #j.

Read('newstate')@i & Read('oldstate')@j ==> j < i"

end

Tamarin quickly proves the first 3 lemmas, but gets stuck forever (and eventually runs out of memory) proving OldThenNew. But if I replace my process definition with:

process:(

new sc: channel;

(

out(sc, 'oldstate') ||

reader(sc) || reader(sc) || reader(sc) || ...

)

)

for any finite number of reader(sc) processes I choose to put there, it proves OldThenNew (though it takes longer and longer with each additional reader(sc) process, and rapidly becomes impractical).

My assumption about the semantics of private channels is that, if a process calls out(p,X) on a private channel p, X can be received one time by any number of concurrent executions of in(p) (so that it is possible for an arbitrary number of processes to "simultaneously" receive 'oldstate' in my example, and thus an arbitrary number of "Read('oldstate')" events to occur), but that once X has been received in a particular process, an additional in(p) in that process would block until some other process called out(p); also, once another out(p, Y) is called, all subsequent (concurrent) executions of in(p) would receive Y. With that semantics, it seems to me that I should be able to prove "OldThenNew", and the fact that Tamarin can prove it automatically for an arbitrary finite number of instantiations of reader (modulo available memory and time) also points in that direction... but I don't have any idea how, or if it's possible, to prove it in the infinite process replication case; I've tried doing it manually, and when I do that, no matter what I try, I end up in an infinite regress of steps that are proven by contradiction and marked "/* cyclic */" in the Tamarin UI.

Any suggestions, or help with my potential lack of understanding of the SAPIC+ channel semantics, would be greatly appreciated. Thanks!

-Dan Zimmerman

[Robert K]

d...@freeandfair.us schrieb am Mittwoch, 19. Februar 2025 um 08:35:56 UTC+1:

Hi! This is the first of a few (more) questions I'm going to be posting about SAPIC+, SAPIC+ translation to ProVerif, and how constructs like channels, state, etc. are meant to be understood.

 

Cas pointed me to the mailing list (I am the maintainer of SAPIC+) recently. I saw that there were some older question – let me know if they are still open, then I'll take a closer look. Anyway, happy to see you trying it out!

I wrote a fairly simple example that uses a private channel, and some lemmas that I thought would be straightforward to prove: [..]

 

My assumption about the semantics of private channels is that, if a process calls out(p,X) on a private channel p, X can be received one time by any number of concurrent executions of in(p) (so that it is possible for an arbitrary number of processes to "simultaneously" receive 'oldstate' in my example, and thus an arbitrary number of "Read('oldstate')" events to occur), but that once X has been received in a particular process, an additional in(p) in that process would block until some other process called out(p); also, once another out(p, Y) is called, all subsequent (concurrent) executions of in(p) would receive Y.

For secret channels, the communication semantics are synchronous, meaning that an "out" picks exactly one "in" (instead of many). If the channel is public, then the adversary can pick up messages and delay them, so the semantics are asynchronous in that case, plus the adversary can forward to many "ins". 
 

With that semantics, it seems to me that I should be able to prove "OldThenNew", and the fact that Tamarin can prove it automatically for an arbitrary finite number of instantiations of reader (modulo available memory and time) also points in that direction... but I don't have any idea how, or if it's possible, to prove it in the infinite process replication case; I've tried doing it manually, and when I do that, no matter what I try, I end up in an infinite regress of steps that are proven by contradiction and marked "/* cyclic */" in the Tamarin UI.

Any suggestions, or help with my potential lack of understanding of the SAPIC+ channel semantics, would be greatly appreciated. Thanks!

There's (at least :D) two things you could try.

For one, the lemma you want to show is inductive in nature, either a newstate comes from a previous newstate, or from the old state. Try adding the attribute use_induction to the lemma (https://tamarin-prover.com/manual/master/book/007_property-specification.html) 

For two, SAPIC+ has two translations for state, because sometimes one is better than the other (although the default is pretty good in the majority of cases). You can simply add the (global) option
"translation-state-optimisation" (https://tamarin-prover.com/manual/master/book/007_property-specification.html). The alternative translation makes better use of tamarin's ability to recognise loops in state facts, so it could just solve the problem.

Cheers, Robert

[Daniel Zimmerman]

On Wednesday, February 19, 2025 at 4:20:40 PM UTC+8 Robert K wrote:

For secret channels, the communication semantics are synchronous, meaning that an "out" picks exactly one "in" (instead of many). If the channel is public, then the adversary can pick up messages and delay them, so the semantics are asynchronous in that case, plus the adversary can forward to many "ins". 

That was actually how I thought it should work... I had previously attempted to prove a lemma stating "there is only one Read('oldstate') event" (I think I'd written it as "All #i #j. Read('oldstate')@i & Read('oldstate')@j ==> #i = #j"), and it would not verify, so I wasn't sure; but apparently I must have written it incorrectly the first time because I was able to verify it just now. Thanks for the clarification!

 

Any suggestions, or help with my potential lack of understanding of the SAPIC+ channel semantics, would be greatly appreciated. Thanks!

There's (at least :D) two things you could try.

For one, the lemma you want to show is inductive in nature, either a newstate comes from a previous newstate, or from the old state. Try adding the attribute use_induction to the lemma (https://tamarin-prover.com/manual/master/book/007_property-specification.html) 

For two, SAPIC+ has two translations for state, because sometimes one is better than the other (although the default is pretty good in the majority of cases). You can simply add the (global) option
"translation-state-optimisation" (https://tamarin-prover.com/manual/master/book/007_property-specification.html). The alternative translation makes better use of tamarin's ability to recognise loops in state facts, so it could just solve the problem.

Unfortunately, it seems like even with both of those - and adding my "there is only one Read('oldstate') event" lemma with the reuse attribute, and adding the reuse attribute to the AlwaysOldOrNew lemma (both of which I would think might help to prove that a newstate never precedes an oldstate), it seems that I still can't prove it. If you have any other suggestions, I'd appreciate it.

Thanks for the help!

-Dan