lemmas.txt

lemma secrecy:
    "All A B x #i.
        Secret(A,B,x)@i &
        not ((Ex #r. Reveal(A)@r) | (Ex #r. Reveal(B)@r))
        ==> not (Ex #j. K(x)@j)"


lemma secrecy_PFS:
    "All A B x #i.
        Secret(A,B,x)@i &
        not ((Ex #r. Reveal(A)@r & r < i) |
        (Ex #r. Reveal(B)@r & r < i))
        ==> not (Ex #j. K(x)@j)"


lemma noninjectiveagreementINITIATOR:
    "All a b t #i.
        Commit(a,b,<’I’,’R’,t>)@i &
        not ((Ex #r. Reveal(a)@r) | (Ex #r. Reveal(b)@r))
        ==> (Ex #j. Running(b,a,<’I’,’R’,t>)@j)"


lemma injectiveagreementINITIATOR:
    "All a b t #i.
        Commit(a,b,<’I’,’R’,t>)@i &
        not ((Ex #r. Reveal(a)@r) | (Ex #r. Reveal(b)@r))
        ==> (Ex #j. Running(b,a,<’I’,’R’,t>)@j
            & not (Ex a2 b2 #i2. Commit(a2,b2,<’I’,’R’,t>)@i2
            & not (#i2 = #i)))"


lemma noninjectiveagreementRESPONDER:
    "All a b t #i.
        Commit(a,b,<’R’,’I’,t>)@i &
        not ((Ex #r. Reveal(a)@r) | (Ex #r. Reveal(b)@r))
        ==> (Ex #j. Running(b,a,<’R’,’I’,t>)@j)"


lemma injectiveagreementRESPONDER:
    "All a b t #i.
        Commit(a,b,<’R’,’I’,t>)@i &
        not ((Ex #r. Reveal(a)@r) | (Ex #r. Reveal(b)@r))
        ==> (Ex #j. Running(b,a,<’R’,’I’,t>)@j
            & not (Ex a2 b2 #i2. Commit(a2,b2,<’R’,’I’,t>)@i2
            & not (#i2 = #i)))"