containers { MapContainer gamma; MultisetContainer e; } declarations { Name n, M, N; Principal A, I, J; Key k; Variable x, z; } tags { TypeTag Un, nonce; MessageTag auth; IdentityTag id; NonceTag verif, claim, verif?, claim?; } // rule definitions rules { // Typing process rule NIL(A) { { 0 } } rule IDENTITY(A) { { id(I) } actions { gamma.add(I, Un);e.add(id(I)); } } rule SYMMETRIC_KEY(A) { { let(k = sym-key(I, J)) } actions { gamma.add(k, key_sym(I, J)); } } rule ASYMMETRIC_KEY(A) { { let(k = asym-key(I)) } actions { gamma.add(k, key_asym(I)); } } rule RUN(A) { { run(A,I,{M}) } actions { e.add(run(A,I,{M})); } } rule INPUT(A) { { in(:::) } external actions { gamma.addFreeVar(:::); e.addEach(in(), :::); } } rule OUTPUT(A) { { out(...) } external conditions { thesis(gamma.checkType(..., Un)); } } rule NEW_NAME(A) { { new(n) } actions { gamma.add(n, Un); e.add(fresh(n)); } } rule NEW_SECRET_NONCE(A) { { new(n) } conditions { thesis(e.contains(id(I)) & (external)gamma.checkType(M,Un)); } actions { gamma.add(n, nonce(I,A,M)); e.add(fresh(n,I,A,M)); } } // Authentication rules: Encryption Rules rule SYMMETRIC_ENCRYPTION(I) { { encrypt(z={...}_k) } external conditions { thesis(gamma.checkType(..., Un) & (gamma.checkType(k, Un) | gamma.checkType(k, key_sym(I,J)))); } actions { gamma.add(z, Un); } } rule PUB_ASYMMETRIC_ENCRYPTION(I) { { encrypt(z={|...|}_Pub(k)) } external conditions { thesis(gamma.checkType(..., Un) & gamma.checkType(k, key_asym(J))); } actions { gamma.add(z, Un); } } rule PRIV_ASYMMETRIC_ENCRYPTION(I) { { encrypt(z={|...|}_Priv(k)) } external conditions { thesis(gamma.checkType(..., Un) & gamma.checkType(k, key_asym(I))); } actions { gamma.add(z, Un); } } rule SC_POSH_REQUEST(I) { { encrypt(z={I:id, N:claim, {M}:auth, ...}_k) } external conditions { thesis((native)e.contains(run(I,J,{M})) & gamma.checkType(N, {M}, ..., Un) & gamma.checkType(k, key_sym(I,J))); } actions { gamma.add(z, Un); e.delete(run(I,J,{M})); } } rule SV_POSH_REQUEST(I) { { encrypt(z={J:id, N:verif, {M}:auth, ...}_k) } external conditions { thesis((native)e.contains(run(I,J,{M})) & gamma.checkType(N, {M}, ..., Un) & gamma.checkType(k, key_sym(I,J))); } actions { gamma.add(z, Un); e.delete(run(I,J,{M})); } } rule AV_POSH_REQUEST(I) { { encrypt(z={|J:id, N:verif, {M}:auth, ...|}_Priv(k)) } external conditions { thesis((native)e.contains(run(I,J,{M})) & gamma.checkType(N, {M}, ..., Un) & gamma.checkType(k, key_asym(I))); } actions { gamma.add(z, Un); e.delete(run(I,J,{M})); } } rule SC_SOPH_SOSH_INQUIRY(J) { { encrypt(z={I:id, N:claim?, {M}:auth, ...}_k) } external conditions { thesis(gamma.checkType({M}, ..., Un) & gamma.checkType(N, nonce(I,J,{M})) & gamma.checkType(k, key_sym(I,J))); } actions { gamma.add(z, Un); } } rule SV_SOPH_SOSH_INQUIRY(J) { { encrypt(z={J:id, N:verif?, {M}:auth, ...}_k) } external conditions { thesis(gamma.checkType({M}, ..., Un) & gamma.checkType(N, nonce(I,J,{M})) & gamma.checkType(k, key_sym(I,J))); } actions { gamma.add(z, Un); } } rule AV_SOPH_SOSH_INQUIRY(J) { { encrypt(z={|J:id, N:verif?, {M}:auth, ...|}_Pub(k)) } external conditions { thesis(gamma.checkType({M}, ..., Un) & gamma.checkType(N, nonce(I,J,{M})) & gamma.checkType(k, key_asym(I))); } actions { gamma.add(z, Un); } } // Authentication rules: Secret Nonce Typing rule SOPH_SOSH_CONFIRM(I) { { run(I,J,{M}) } external conditions { thesis(gamma.checkType(z, nonce(I,J,{M}))); } actions { gamma.set(z, Un); } } // Authentication rules: Authentication rule SC_POSH_COMMIT(J) { { commit(J,I,{M}) } conditions { thesis(e.contains(fresh(n)) & e.contains(dec({I:id, n:claim, {M}:auth, ...}(_k))) & (external)gamma.checkType(n, {M}, ..., Un) & (external)gamma.checkType(k, key_sym(I,J))); } actions { e.delete(fresh(n)); } } rule SV_POSH_COMMIT(J) { { commit(J,I,{M}) } conditions { thesis(e.contains(fresh(n)) & e.contains(dec({J:id, n:verif, {M}:auth, ...}(_k))) & (external)gamma.checkType(n, {M}, ..., Un) & (external)gamma.checkType(k, key_sym(I,J))); } actions { e.delete(fresh(n)); } } rule AV_POSH_COMMIT(J) { { commit(J,I,{M}) } conditions { thesis(e.contains(fresh(n)) & e.contains(dec({|J:id, n:verif, {M}:auth, ...|}(_Priv(k)))) & (external)gamma.checkType(n, {M}, ..., Un) & (external)gamma.checkType(k, key_asym(I))); } actions { e.delete(fresh(n)); } } rule SOPH_SOSH_COMMIT(J) { { commit(J,I,{M}) } conditions { thesis(e.contains(fresh(n,I,J,{M})) & (e.contains(in(n)) | e.contains(dec({n, ...}(_k))) | e.contains(dec({|n, ...|}(_Priv(k)))) | e.contains(dec({|n, ...|}(_Pub(k))))) & (external)gamma.checkType(n, nonce(I,J,{M}))); } actions { e.delete(fresh(n,I,J,{M})); } } // Authentication rules: Decryption Rules rule SYMMETRIC_DECRYPTION(I) { { decrypt(z={...}(_k)) } external conditions { thesis(gamma.checkType(k, key_sym(I,J))); } actions { (external)gamma.addFreeVar(...); e.add(dec({...}(_k))); } } rule PUB_ASYMMETRIC_DECRYPTION(I) { { decrypt(z={|...|}(_Pub(k))) } external conditions { thesis(gamma.checkType(k, key_asym(J))); } actions { (external)gamma.addFreeVar(...); e.add(dec({|...|}(_Priv(k)))); } } rule PRIV_ASYMMETRIC_DECRYPTION(I) { { decrypt(z={|...|}(_Priv(k))) } external conditions { thesis(gamma.checkType(k, key_asym(I))); } actions { (external)gamma.addFreeVar(...); e.add(dec({|...|}(_Pub(k)))); } } rule SC_POSH_DECRYPTION(J) { { decrypt(z={I:id, n:claim, {x}:auth, ...}(_k)) } external conditions { thesis(gamma.checkType(k, key_sym(I,J)) & gamma.checkType(n, Un)); } external actions { gamma.addFreeVar(...); gamma.addAll({x}, Un); (native)e.add(dec({I:id, n:claim, {x}:auth, ...}(_k))); } } rule SV_POSH_DECRYPTION(J) { { decrypt(z={J:id, n:verif, {x}:auth, ...}(_k)) } external conditions { thesis(gamma.checkType(k, key_sym(I,J)) & gamma.checkType(n, Un)); } external actions { gamma.addAll({x}, Un); gamma.addFreeVar(...); (native)e.add(dec({J:id, n:verif, {x}:auth, ...}(_k))); } } rule AV_POSH_DECRYPTION(J) { { decrypt(z={|J:id, n:verif, {x}:auth, ...|}(_Pub(k))) } external conditions { thesis(gamma.checkType(k, key_asym(I)) & gamma.checkType(n, Un)); } external actions { gamma.addAll({x}, Un); gamma.addFreeVar(...); (native)e.add(dec({J:id, n:verif, {x}:auth, ...}(_Priv(k)))); } } rule SC_SOPH_SOSH_DECRYPTION(I) { { decrypt(z={I:id, x:claim?, {z}:auth, ...}(_k)) } external conditions { thesis(gamma.checkType(k, key_sym(I,J))); } actions { gamma.add(x, nonce(I,J,{z})); (external)gamma.addAll({z}, Un); (external)gamma.addFreeVar(...); e.add(dec({I:id, x:claim?, {z}:auth, ...}(_k))); } } rule SV_SOPH_SOSH_DECRYPTION(I) { { decrypt(z={J:id, x:verif?, {z}:auth, ...}(_k)) } external conditions { thesis(gamma.checkType(k, key_sym(I,J))); } actions { gamma.add(x, nonce(I,J,{z})); (external)gamma.addAll({z}, Un); (external)gamma.addFreeVar(...); e.add(dec({J:id, x:verif?, {z}:auth, ...}(_k))); } } rule AV_SOPH_SOSH_DECRYPTION(I) { { decrypt(z={|J:id, x:verif?, {z}:auth, ...|}(_Priv(k))) } external conditions { thesis(gamma.checkType(k, key_asym(I))); } actions { gamma.add(x, nonce(I,J,{z})); (external)gamma.addAll({z}, Un); (external)gamma.addFreeVar(...); e.add(dec({|J:id, x:verif?, {z}:auth, ...|}(_Pub(k)))); } } }