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); } } 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:Un) } actions { gamma.add(n, Un); e.add(fresh(n)); } } rule NEW_SECRET_NONCE(A) { { new(n:nonce(I,A,M)) } 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)); } actions { (external)gamma.addFreeVar(...); gamma.add(x, Un); 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)); } actions { gamma.add(x, Un); (external)gamma.addFreeVar(...); 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)); } actions { gamma.add(x, Un); (external)gamma.addFreeVar(...); 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)); gamma.add(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)); gamma.add(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)); gamma.add(z, Un); (external)gamma.addFreeVar(...); e.add(dec({|J:id, x:verif?, z:auth, ...|}(_Pub(k)))); } } }