@desc[a (not) very long description] containers { SetContainer gamma; OrdContainer pi; } declarations { Name n, M; Principal I, A, B, T; Key k, d, yp, ks, kBT, kAT; Variable x, y, z; } tags { TypeTag Un, nonce; KeyTag key; IdentityTag id; NonceTag verif, claim, owner; } // rule definitions rules { // Protocol correctness rule SYM_KEY(I) { { let(k = sym-key(A, B)) } conditions { thesis(!pi.contains(k=sym-key(A, B))); } actions { pi.add(k=sym-key(A, B)); } } rule ASYM_KEY(I) { { let(k = asym-key(A)) } conditions { thesis(!pi.contains(k = asym-key(A))); } actions { pi.add(k = asym-key(A)); } } // Local correctness: Generic Principal Rules rule NIL(I) { { 0 } } rule NEW_NAME(I) { { new(n) } external conditions { thesis(gamma.fresh(n)); } actions { gamma.add(n="unchecked"); } } rule INPUT(I) { { in(...) } } rule OUTPUT(I) { { out(...) } } rule OWNER(A) { { encrypt(y={:::}_x) } conditions { @ra thesis(pi.contains(k=sym-key(A, T)) & pi.contains(any=dec({B:id, n:owner, x:key, ...}(_k))) & (external)pi.isLast(B=run())); } actions { pi.add(y=enc({:::}_x)); } } rule ENCRYPTION(I) { { encrypt(y={...}_d) } conditions { ipothesis(pi.contains(any=dec({d:key, :::}(_k)))); thesis(pi.contains(B=run()) & (external)pi.isNext(x=enc({...}_d))); } actions { pi.add(y=enc({...}_d)); } } rule DECRYPTION(I) { { decrypt(y={:::}(_d)) } actions { pi.add(y=dec({:::}(_d))); } } // Local correctness: TTP and Principal Rules - Claimant and Verifier Rules rule AUTHENTICATE_CLAIM(A) { { commit(A, B) } conditions { thesis(gamma.contains(n="unchecked") & pi.contains(any=dec({B:id, n:claim, ...}(_k))) & (pi.contains(k=sym-key(A, T)) | pi.contains(k=sym-key(A, B)))); } actions { gamma.set(n="checked"); } } rule AUTHENTICATE_VERIF(A) { { commit(A, B) } conditions { thesis(gamma.contains(n="unchecked") & pi.contains(any=dec({A:id, n:verif, ...}(_k))) & pi.contains(k=sym-key(A, B))); } actions { gamma.set(n="checked"); } } rule AUTHENTICATE_OWNER(A) { { commit(A, B) } conditions { @ra thesis(gamma.contains(n="unchecked") & pi.contains(k=sym-key(A, T)) & pi.contains(any=dec({B:id, n:owner, y:key, ...}(_k)))); @ra thesis(pi.contains(x=dec({:::}(_y)))); @ra ipothesis(pi.contains(z=enc({:::}_yp))); thesis(!(external)x.contentEquals(pi, z)); } actions { gamma.set(n="checked"); } } rule CLAIMANT(A) { { encrypt(y={A:id, x:claim, ...}_k) } conditions { thesis(pi.contains(k=sym-key(A, B)) & (external)pi.isLast(B=run())); } actions { pi.add(y=enc({A:id, x:claim}_k)); } } rule VERIFIER(A) { { encrypt(y={B:id, x:verif, ...}_k) } conditions { thesis((pi.contains(k=sym-key(A, T)) | pi.contains(k=sym-key(A, B))) & (external)pi.isLast(B=run())); } actions { pi.add(y=enc({B:id, x:verif}_k)); } } rule RUN(A) { { run(A, B) } actions { pi.add(B=run()); } } // Local correctness: TTP and Principal Rules - TTP Rules rule TTP_FORWARD_AND_CHECK(T) { { encrypt(y={A:id, x:claim, ...}_kBT) } conditions { @ra thesis(gamma.contains(n="unchecked") & pi.contains(kBT=sym-key(B, T)) & pi.contains(kAT=sym-key(A, T)) & pi.contains(any=dec({B:id, n:verif, ...}(_kAT)))); } actions { gamma.set(n="checked"); pi.add(y=enc({A:id, x:claim}_kBT)); } } rule TTP_FORWARD(T) { { encrypt(y={A:id, x:claim, ...}_kBT) } conditions { @ra thesis(pi.contains(kBT=sym-key(B, T)) & pi.contains(kAT=sym-key(A, T)) & pi.contains(any=dec({B:id, x:verif, ...}(_kAT)))); } actions { pi.add(y=enc({A:id, x:claim}_kBT)); } } rule TTP_DISTRIBUTE(T) { { encrypt(y={A:id, x:owner, ks:key, ...}_k) } external conditions { thesis(gamma.match(n="unchecked")); } actions { gamma.set(n="checked"); pi.add(y=enc({A:id, x:owner, ks:key}_k)); } } }