From a10c424d6a4b668f58e3cf7d726e960fefcba677 Mon Sep 17 00:00:00 2001 From: jm71syxy <jonas.mueller.97@stud.tu-darmstadt.de> Date: Wed, 19 Jun 2024 14:45:30 +0200 Subject: [PATCH] Update SigPQEAC results --- ...ARIN => 45992234.err.ALL_SigPQEAC_TAMARIN} | 10 +- ...ARIN => 45992234.out.ALL_SigPQEAC_TAMARIN} | 1242 ++++++++--------- 2 files changed, 605 insertions(+), 647 deletions(-) rename results/{45991790.err.ALL_SigPQEAC_TAMARIN => 45992234.err.ALL_SigPQEAC_TAMARIN} (66%) rename results/{45991790.out.ALL_SigPQEAC_TAMARIN => 45992234.out.ALL_SigPQEAC_TAMARIN} (82%) diff --git a/results/45991790.err.ALL_SigPQEAC_TAMARIN b/results/45992234.err.ALL_SigPQEAC_TAMARIN similarity index 66% rename from results/45991790.err.ALL_SigPQEAC_TAMARIN rename to results/45992234.err.ALL_SigPQEAC_TAMARIN index e8b69d9..3503e35 100644 --- a/results/45991790.err.ALL_SigPQEAC_TAMARIN +++ b/results/45992234.err.ALL_SigPQEAC_TAMARIN @@ -24,5 +24,11 @@ [Saturating Sources] Step 2/5 [Saturating Sources] Step 1/5 [Saturating Sources] Step 2/5 -WARNING: you should run this program as super-user. -WARNING: output may be incomplete or inaccurate, you should run this program as super-user. +[Saturating Sources] Step 1/5 +[Saturating Sources] Step 2/5 +[Saturating Sources] Step 1/5 +[Saturating Sources] Step 2/5 +[Saturating Sources] Step 1/5 +[Saturating Sources] Step 2/5 +/var/spool/slurmd/job45992234/slurm_script: line 29: output/hw/45992234.cpu: No such file or directory +/var/spool/slurmd/job45992234/slurm_script: line 30: output/hw/45992234.processor: No such file or directory diff --git a/results/45991790.out.ALL_SigPQEAC_TAMARIN b/results/45992234.out.ALL_SigPQEAC_TAMARIN similarity index 82% rename from results/45991790.out.ALL_SigPQEAC_TAMARIN rename to results/45992234.out.ALL_SigPQEAC_TAMARIN index 9a2b1ad..cc39be4 100644 --- a/results/45991790.out.ALL_SigPQEAC_TAMARIN +++ b/results/45992234.out.ALL_SigPQEAC_TAMARIN @@ -1,7 +1,7 @@ maude tool: 'maude' checking version: 3.3.1. OK. checking installation: OK. -theory FastSigPQEAC begin +theory SigPQEAC begin // Function signature and definition of the equational theory E @@ -78,288 +78,253 @@ rule (modulo E) TA_INIT_T: /* has exactly the trivial AC variant */ rule (modulo E) TA_CHALLENGE_C: - [ - In( <certT, '1', 't'> ), Fr( ~r1 ), Fr( ~id_c ), Fr( ~iid ), Fr( ~r2 ), - !Cert( $C, certC, 'chip' ) - ] + [ In( <certT, '1', 't'> ), Fr( ~r1 ), Fr( ~id_c ), Fr( ~iid ) ] --[ Eq( verify_cert(certT, 'terminal'), true ), Started( ) ]-> [ - Out( <~id_c, ~r1, certC, ~r2, '2', 'c'> ), Out( ~iid ), - TAChallengeC( <$C, ~iid>, certT, ~id_c, ~r1, ~r2 ) + Out( <~id_c, ~r1, '2', 'c'> ), + TAChallengeC( <$C, ~iid>, certT, ~id_c, ~r1 ) ] /* rule (modulo AC) TA_CHALLENGE_C: - [ - In( <certT, '1', 't'> ), Fr( ~r1 ), Fr( ~id_c ), Fr( ~iid ), Fr( ~r2 ), - !Cert( $C, certC, 'chip' ) - ] + [ In( <certT, '1', 't'> ), Fr( ~r1 ), Fr( ~id_c ), Fr( ~iid ) ] --[ Eq( z, true ), Started( ) ]-> [ - Out( <~id_c, ~r1, certC, ~r2, '2', 'c'> ), Out( ~iid ), - TAChallengeC( <$C, ~iid>, certT, ~id_c, ~r1, ~r2 ) + Out( <~id_c, ~r1, '2', 'c'> ), + TAChallengeC( <$C, ~iid>, certT, ~id_c, ~r1 ) ] variants (modulo AC) - 1. certT = certT.15 - z = verify(cert_sig(certT.15), - <cert_pk(certT.15), cert_id(certT.15), 'terminal'>, pk(ca_sk)) + 1. certT = certT.12 + z = verify(cert_sig(certT.12), + <cert_pk(certT.12), cert_id(certT.12), 'terminal'>, pk(ca_sk)) - 2. certT = cert(x.16, sign(<x.16, x.17, 'terminal'>, ca_sk), x.17) + 2. certT = cert(x.13, sign(<x.13, x.14, 'terminal'>, ca_sk), x.14) z = true - 3. certT = cert(x.17, x.18, x.19) - z = verify(x.18, <x.17, x.19, 'terminal'>, pk(ca_sk)) + 3. certT = cert(x.14, x.15, x.16) + z = verify(x.15, <x.14, x.16, 'terminal'>, pk(ca_sk)) */ rule (modulo E) TA_RESPONSE_T: [ - In( <id_c, r1, certC, r2, '2', 'c'> ), TAInitT( <$T, iid> ), - !Ltk( $T, ~skT, 'terminal' ), !Cert( $T, certT, 'terminal' ), Fr( ~k ) + In( <id_c, r1, '2', 'c'> ), TAInitT( <$T, iid> ), + !Ltk( $T, ~skT, 'terminal' ) + ] + --> + [ + Out( <sign(<'TA', id_c, r1>, ~skT), '3', 't'> ), + TAResponseT( <$T, iid>, id_c ) + ] + + /* has exactly the trivial AC variant */ + +rule (modulo E) TA_COMPLETE_C: + [ In( <s, '3', 't'> ), TAChallengeC( <$C, iid>, certT, id_c, r1 ) ] + --[ + Eq( verify(s, <'TA', id_c, r1>, cert_pk(certT)), true ), + CompletedTA( $C, iid, cert_id(certT) ) + ]-> + [ TACompleteC( <$C, iid>, certT, id_c, r1 ) ] + + /* + rule (modulo AC) TA_COMPLETE_C: + [ In( <s, '3', 't'> ), TAChallengeC( <$C, iid>, certT, id_c, r1 ) ] + --[ Eq( z, true ), CompletedTA( $C, iid, z.1 ) ]-> + [ TACompleteC( <$C, iid>, certT, id_c, r1 ) ] + variants (modulo AC) + 1. certT = certT.16 + id_c = id_c.17 + r1 = r1.19 + s = s.20 + z = verify(s.20, <'TA', id_c.17, r1.19>, cert_pk(certT.16)) + z.1 = cert_id(certT.16) + + 2. certT = cert(x.37, x.38, z.28) + id_c = id_c.21 + r1 = r1.23 + s = s.24 + z = verify(s.24, <'TA', id_c.21, r1.23>, x.37) + z.1 = z.28 + + 3. certT = cert(pk(x.37), x.38, z.28) + id_c = id_c.21 + r1 = r1.23 + s = sign(<'TA', id_c.21, r1.23>, x.37) + z = true + z.1 = z.28 + */ + +rule (modulo E) CA_INIT_C: + [ + Fr( ~r2 ), TACompleteC( <$C, iid>, certT, id_c, r1 ), + !Cert( $C, certC, 'chip' ) + ] + --> + [ + Out( <certC, ~r2, '4', 'c'> ), Out( iid ), + CAInitC( <$C, iid>, certT, id_c, r1, ~r2 ) + ] + + /* has exactly the trivial AC variant */ + +rule (modulo E) CA_INIT_T: + [ + In( <certC, r2, '4', 'c'> ), Fr( ~k ), TAResponseT( <$T, iid>, id_c ), + !Ltk( $T, ~skT, 'terminal' ), !Cert( $T, certT, 'terminal' ) ] --[ Eq( verify_cert(certC, 'chip'), true ) ]-> [ - Out( <encaps(~k, cert_pk(certC)), sign(<'TA', id_c, r1>, ~skT), - sign(<'CA', certT, certC, r2, encaps(~k, cert_pk(certC))>, ~skT), '3', + Out( <encaps(~k, cert_pk(certC)), + sign(<'CA', certT, certC, r2, encaps(~k, cert_pk(certC))>, ~skT), '5', 't'> ), CAInitT( <$T, iid>, id_c, certC, r2, <~k, encaps(~k, cert_pk(certC))> ) ] /* - rule (modulo AC) TA_RESPONSE_T: + rule (modulo AC) CA_INIT_T: [ - In( <id_c, r1, certC, r2, '2', 'c'> ), TAInitT( <$T, iid> ), - !Ltk( $T, ~skT, 'terminal' ), !Cert( $T, certT, 'terminal' ), Fr( ~k ) + In( <certC, r2, '4', 'c'> ), Fr( ~k ), TAResponseT( <$T, iid>, id_c ), + !Ltk( $T, ~skT, 'terminal' ), !Cert( $T, certT, 'terminal' ) ] --[ Eq( z.1, true ) ]-> [ - Out( <encaps(~k, z), sign(<'TA', id_c, r1>, ~skT), - sign(<'CA', certT, certC, r2, encaps(~k, z)>, ~skT), '3', 't'> + Out( <encaps(~k, z), + sign(<'CA', certT, certC, r2, encaps(~k, z)>, ~skT), '5', 't'> ), CAInitT( <$T, iid>, id_c, certC, r2, <~k, encaps(~k, z)> ) ] variants (modulo AC) - 1. certC = certC.20 - z = cert_pk(certC.20) - z.1 = verify(cert_sig(certC.20), - <cert_pk(certC.20), cert_id(certC.20), 'chip'>, pk(ca_sk)) + 1. certC = certC.18 + z = cert_pk(certC.18) + z.1 = verify(cert_sig(certC.18), + <cert_pk(certC.18), cert_id(certC.18), 'chip'>, pk(ca_sk)) - 2. certC = cert(z.57, sign(<z.57, x.100, 'chip'>, ca_sk), x.100) - z = z.57 + 2. certC = cert(z.44, sign(<z.44, x.75, 'chip'>, ca_sk), x.75) + z = z.44 z.1 = true - 3. certC = cert(z.58, x.101, x.102) - z = z.58 - z.1 = verify(x.101, <z.58, x.102, 'chip'>, pk(ca_sk)) + 3. certC = cert(z.45, x.76, x.77) + z = z.45 + z.1 = verify(x.76, <z.45, x.77, 'chip'>, pk(ca_sk)) */ -rule (modulo E) TA_COMPLETE_C: +rule (modulo E) CA_FINISH_C: [ - In( <cip, s1, s2, '3', 't'> ), - TAChallengeC( <$C, iid>, certT, id_c, r1, r2 ), !Ltk( $C, ~skC, 'chip' ), - !Cert( $C, certC, 'chip' ) + In( <cip, s, '5', 't'> ), CAInitC( <$C, iid>, certT, id_c, r1, r2 ), + !Ltk( $C, ~skC, 'chip' ), !Cert( $C, certC, 'chip' ) ] --[ - Eq( verify(s1, <'TA', id_c, r1>, cert_pk(certT)), true ), - Eq( verify(s2, <'CA', certT, certC, r2, cip>, cert_pk(certT)), true ), - CompletedTA( $C, iid, cert_id(certT) ), + Eq( verify(s, <'CA', certT, certC, r2, cip>, cert_pk(certT)), true ), Completed( kdf(<'KEY', certT, certC, r2, cip>, decaps(cip, ~skC)), <certT, certC, r2, cip>, $C, 'chip', cert_id(certT) ) ]-> [ - Out( <kdf(<'CNF', certT, certC, r2, cip>, decaps(cip, ~skC)), '4', 'c'> + Out( <kdf(<'CNF', certT, certC, r2, cip>, decaps(cip, ~skC)), '6', 'c'> ), - TACompleteC( <$C, iid>, certT, id_c, r1, r2 ) + CAFinishC( $C, cert_id(certT), + kdf(<'KEY', certT, certC, r2, cip>, decaps(cip, ~skC)) + ) ] /* - rule (modulo AC) TA_COMPLETE_C: + rule (modulo AC) CA_FINISH_C: [ - In( <cip, s1, s2, '3', 't'> ), - TAChallengeC( <$C, iid>, certT, id_c, r1, r2 ), !Ltk( $C, ~skC, 'chip' ), - !Cert( $C, certC, 'chip' ) + In( <cip, s, '5', 't'> ), CAInitC( <$C, iid>, certT, id_c, r1, r2 ), + !Ltk( $C, ~skC, 'chip' ), !Cert( $C, certC, 'chip' ) ] --[ - Eq( z.1, true ), Eq( z.2, true ), CompletedTA( $C, iid, z.3 ), + Eq( z.2, true ), Completed( kdf(<'KEY', certT, certC, r2, cip>, z), - <certT, certC, r2, cip>, $C, 'chip', z.3 + <certT, certC, r2, cip>, $C, 'chip', z.1 ) ]-> [ - Out( <kdf(<'CNF', certT, certC, r2, cip>, z), '4', 'c'> ), - TACompleteC( <$C, iid>, certT, id_c, r1, r2 ) + Out( <kdf(<'CNF', certT, certC, r2, cip>, z), '6', 'c'> ), + CAFinishC( $C, z.1, kdf(<'KEY', certT, certC, r2, cip>, z) ) ] variants (modulo AC) - 1. ~skC = ~skC.32 - certC = certC.33 - certT = certT.34 - cip = cip.35 - id_c = id_c.36 - r1 = r1.38 - r2 = r2.39 - s1 = s1.40 - s2 = s2.41 - z = decaps(cip.35, ~skC.32) - z.1 = verify(s1.40, <'TA', id_c.36, r1.38>, cert_pk(certT.34)) - z.2 = verify(s2.41, <'CA', certT.34, certC.33, r2.39, cip.35>, - cert_pk(certT.34)) - z.3 = cert_id(certT.34) - - 2. ~skC = ~skC.37 - certC = certC.38 - certT = certT.39 - cip = encaps(z.51, pk(~skC.37)) - id_c = id_c.41 - r1 = r1.43 - r2 = r2.44 - s1 = s1.45 - s2 = s2.46 - z = z.51 - z.1 = verify(s1.45, <'TA', id_c.41, r1.43>, cert_pk(certT.39)) - z.2 = verify(s2.46, - <'CA', certT.39, certC.38, r2.44, encaps(z.51, pk(~skC.37))>, - cert_pk(certT.39)) - z.3 = cert_id(certT.39) - - 3. ~skC = ~skC.150 - certC = certC.151 - certT = cert(x.296, x.297, z.169) - cip = cip.153 - id_c = id_c.154 - r1 = r1.156 - r2 = r2.157 - s1 = s1.158 - s2 = s2.159 - z = decaps(cip.153, ~skC.150) - z.1 = verify(s1.158, <'TA', id_c.154, r1.156>, x.296) - z.2 = verify(s2.159, - <'CA', cert(x.296, x.297, z.169), certC.151, r2.157, cip.153>, x.296) - z.3 = z.169 - - 4. ~skC = ~skC.150 - certC = certC.151 - certT = cert(pk(x.296), x.297, z.169) - cip = cip.153 - id_c = id_c.154 - r1 = r1.156 - r2 = r2.157 - s1 = sign(<'TA', id_c.154, r1.156>, x.296) - s2 = s2.159 - z = decaps(cip.153, ~skC.150) - z.1 = true - z.2 = verify(s2.159, - <'CA', cert(pk(x.296), x.297, z.169), certC.151, r2.157, cip.153>, - pk(x.296)) - z.3 = z.169 - - 5. ~skC = ~skC.151 - certC = certC.152 - certT = cert(pk(x.298), x.299, z.170) - cip = cip.154 - id_c = id_c.155 - r1 = r1.157 - r2 = r2.158 - s1 = s1.159 - s2 = sign(<'CA', cert(pk(x.298), x.299, z.170), certC.152, r2.158, - cip.154>, - x.298) - z = decaps(cip.154, ~skC.151) - z.1 = verify(s1.159, <'TA', id_c.155, r1.157>, pk(x.298)) - z.2 = true - z.3 = z.170 - - 6. ~skC = ~skC.151 - certC = certC.152 - certT = cert(pk(x.298), x.299, z.170) - cip = cip.154 - id_c = id_c.155 - r1 = r1.157 - r2 = r2.158 - s1 = sign(<'TA', id_c.155, r1.157>, x.298) - s2 = sign(<'CA', cert(pk(x.298), x.299, z.170), certC.152, r2.158, - cip.154>, - x.298) - z = decaps(cip.154, ~skC.151) - z.1 = true - z.2 = true - z.3 = z.170 - - 7. ~skC = ~skC.152 - certC = certC.153 - certT = cert(x.300, x.301, z.171) - cip = encaps(z.166, pk(~skC.152)) - id_c = id_c.156 - r1 = r1.158 - r2 = r2.159 - s1 = s1.160 - s2 = s2.161 - z = z.166 - z.1 = verify(s1.160, <'TA', id_c.156, r1.158>, x.300) - z.2 = verify(s2.161, - <'CA', cert(x.300, x.301, z.171), certC.153, r2.159, - encaps(z.166, pk(~skC.152))>, - x.300) - z.3 = z.171 - - 8. ~skC = ~skC.152 - certC = certC.153 - certT = cert(pk(x.300), x.301, z.171) - cip = encaps(z.166, pk(~skC.152)) - id_c = id_c.156 - r1 = r1.158 - r2 = r2.159 - s1 = s1.160 - s2 = sign(<'CA', cert(pk(x.300), x.301, z.171), certC.153, r2.159, - encaps(z.166, pk(~skC.152))>, - x.300) - z = z.166 - z.1 = verify(s1.160, <'TA', id_c.156, r1.158>, pk(x.300)) - z.2 = true - z.3 = z.171 - - 9. ~skC = ~skC.152 - certC = certC.153 - certT = cert(pk(x.300), x.301, z.171) - cip = encaps(z.166, pk(~skC.152)) - id_c = id_c.156 - r1 = r1.158 - r2 = r2.159 - s1 = sign(<'TA', id_c.156, r1.158>, x.300) - s2 = s2.161 - z = z.166 - z.1 = true - z.2 = verify(s2.161, - <'CA', cert(pk(x.300), x.301, z.171), certC.153, r2.159, - encaps(z.166, pk(~skC.152))>, - pk(x.300)) - z.3 = z.171 - - 10. ~skC = ~skC.152 - certC = certC.153 - certT = cert(pk(x.300), x.301, z.171) - cip = encaps(z.166, pk(~skC.152)) - id_c = id_c.156 - r1 = r1.158 - r2 = r2.159 - s1 = sign(<'TA', id_c.156, r1.158>, x.300) - s2 = sign(<'CA', cert(pk(x.300), x.301, z.171), certC.153, r2.159, - encaps(z.166, pk(~skC.152))>, - x.300) - z = z.166 - z.1 = true - z.2 = true - z.3 = z.171 + 1. ~skC = ~skC.30 + certC = certC.31 + certT = certT.32 + cip = cip.33 + r2 = r2.37 + s = s.38 + z = decaps(cip.33, ~skC.30) + z.1 = cert_id(certT.32) + z.2 = verify(s.38, <'CA', certT.32, certC.31, r2.37, cip.33>, + cert_pk(certT.32)) + + 2. ~skC = ~skC.35 + certC = certC.36 + certT = certT.37 + cip = encaps(z.48, pk(~skC.35)) + r2 = r2.42 + s = s.43 + z = z.48 + z.1 = cert_id(certT.37) + z.2 = verify(s.43, + <'CA', certT.37, certC.36, r2.42, encaps(z.48, pk(~skC.35))>, + cert_pk(certT.37)) + + 3. ~skC = ~skC.137 + certC = certC.138 + certT = cert(x.270, x.271, z.153) + cip = cip.140 + r2 = r2.144 + s = s.145 + z = decaps(cip.140, ~skC.137) + z.1 = z.153 + z.2 = verify(s.145, + <'CA', cert(x.270, x.271, z.153), certC.138, r2.144, cip.140>, x.270) + + 4. ~skC = ~skC.138 + certC = certC.139 + certT = cert(pk(x.272), x.273, z.154) + cip = cip.141 + r2 = r2.145 + s = sign(<'CA', cert(pk(x.272), x.273, z.154), certC.139, r2.145, + cip.141>, + x.272) + z = decaps(cip.141, ~skC.138) + z.1 = z.154 + z.2 = true + + 5. ~skC = ~skC.139 + certC = certC.140 + certT = cert(x.274, x.275, z.155) + cip = encaps(z.152, pk(~skC.139)) + r2 = r2.146 + s = s.147 + z = z.152 + z.1 = z.155 + z.2 = verify(s.147, + <'CA', cert(x.274, x.275, z.155), certC.140, r2.146, + encaps(z.152, pk(~skC.139))>, + x.274) + + 6. ~skC = ~skC.139 + certC = certC.140 + certT = cert(pk(x.274), x.275, z.155) + cip = encaps(z.152, pk(~skC.139)) + r2 = r2.146 + s = sign(<'CA', cert(pk(x.274), x.275, z.155), certC.140, r2.146, + encaps(z.152, pk(~skC.139))>, + x.274) + z = z.152 + z.1 = z.155 + z.2 = true */ rule (modulo E) CA_FINISH_T: [ - In( <kCNF_C, '4', 'c'> ), + In( <kCNF_c, '6', 'c'> ), CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ), !Cert( $T, certT, 'terminal' ) ] --[ - Eq( kdf(<'CNF', certT, certC, r2, cip>, k), kCNF_C ), + Eq( kdf(<'CNF', certT, certC, r2, cip>, k), kCNF_c ), Completed( kdf(<'KEY', certT, certC, r2, cip>, k), <certT, certC, r2, cip>, $T, 'terminal', cert_id(certC) ), @@ -375,12 +340,12 @@ rule (modulo E) CA_FINISH_T: /* rule (modulo AC) CA_FINISH_T: [ - In( <kCNF_C, '4', 'c'> ), + In( <kCNF_c, '6', 'c'> ), CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ), !Cert( $T, certT, 'terminal' ) ] --[ - Eq( kdf(<'CNF', certT, certC, r2, cip>, k), kCNF_C ), + Eq( kdf(<'CNF', certT, certC, r2, cip>, k), kCNF_c ), Completed( kdf(<'KEY', certT, certC, r2, cip>, k), <certT, certC, r2, cip>, $T, 'terminal', z ), @@ -2240,10 +2205,9 @@ guarded formula characterizing all satisfying traces: */ simplify solve( Completed( k, sid, C, 'chip', T ) @ #i ) - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 - ) ▶₁ #i ) - case TA_CHALLENGE_C + case CA_FINISH_C + solve( CAInitC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 ) ▶₁ #i ) + case CA_INIT_C solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) case Generate_chip_key_pair solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) @@ -2260,44 +2224,54 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) solve( CAInitT( <$T, iid.1>, id_c.1, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip> ) ▶₁ #j ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), 'terminal' ) ▶₂ #j ) case CA_Sign_ltk - solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.3 ) - case TA_RESPONSE_T - solve( !KU( sign(<'CA', - cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, - encaps(~k, pk(~ltk))>, - ~ltk.1) - ) @ #vk.5 ) + solve( !KU( sign(<'CA', + cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), + cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, + encaps(~k, pk(~ltk))>, + ~ltk.1) + ) @ #vk.3 ) + case CA_INIT_T + solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.11 ) case TA_RESPONSE_T - solve( !KU( cert(z, sign(<z, x, 'chip'>, ca_sk), x) ) @ #vk.34 ) - case CA_Sign_ltk - solve( !KU( ~r2 ) @ #vk.30 ) + solve( !KU( ~r2 ) @ #vk.28 ) + case CA_INIT_C + solve( !KU( ~id_c ) @ #vk.34 ) case TA_CHALLENGE_C - solve( !KU( ~id_c ) @ #vk.33 ) + solve( !KU( ~r1 ) @ #vk.35 ) case TA_CHALLENGE_C - solve( !KU( ~r1 ) @ #vk.34 ) - case TA_CHALLENGE_C - solve( !KU( cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T) - ) @ #vk.20 ) - case CA_Sign_ltk - solve( !KU( kdf(<'CNF', - cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, - encaps(~k, pk(~ltk))>, - ~k) - ) @ #vk.24 ) - case TA_COMPLETE_C - solve( !KU( cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C) - ) @ #vk.33 ) - case CA_Sign_ltk - solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.21 ) - case TA_RESPONSE_T - SOLVED // trace found + solve( !KU( cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T) + ) @ #vk.19 ) + case CA_Sign_ltk + solve( !KU( kdf(<'CNF', + cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), + cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, + encaps(~k, pk(~ltk))>, + ~k) + ) @ #vk.23 ) + case CA_FINISH_C + solve( !KU( cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C) + ) @ #vk.31 ) + case CA_INIT_C + solve( !KU( sign(<'TA', ~id_c.2, ~r1.2>, x) ) @ #vk.38 ) + case TA_RESPONSE_T + solve( !KU( cert(pk(~skT.2), sign(<pk(~skT.2), z, 'terminal'>, ca_sk), z) + ) @ #vk.40 ) + case CA_Sign_ltk + solve( !KU( ~id_c.2 ) @ #vk.42 ) + case TA_CHALLENGE_C + solve( !KU( ~r1.1 ) @ #vk.43 ) + case TA_CHALLENGE_C + solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.24 ) + case CA_INIT_T + SOLVED // trace found + qed + qed + qed qed qed qed @@ -2338,10 +2312,9 @@ guarded formula characterizing all satisfying traces: */ simplify solve( Completed( k, sid, C, 'chip', T ) @ #i ) - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 - ) ▶₁ #i ) - case TA_CHALLENGE_C + case CA_FINISH_C + solve( CAInitC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 ) ▶₁ #i ) + case CA_INIT_C solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) case Generate_chip_key_pair solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) @@ -2358,17 +2331,16 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) solve( CAInitT( <$T, iid.1>, id_c.1, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip> ) ▶₁ #j ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), 'terminal' ) ▶₂ #j ) case CA_Sign_ltk solve( Completed( k2, sid2, $C, 'chip', $T ) @ #i2 ) - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid.1>, cert(pk(x), x.1, $T), id_c.1, r1.1, - r2.1 + case CA_FINISH_C + solve( CAInitC( <$C, iid.1>, cert(pk(x), x.1, $T), id_c.1, r1.1, r2.1 ) ▶₁ #i2 ) - case TA_CHALLENGE_C + case CA_INIT_C solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i2 ) case Generate_chip_key_pair solve( !Cert( $C, certC, 'chip' ) ▶₃ #i2 ) @@ -2388,104 +2360,133 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) cert(pk(~ltk.2), sign(<pk(~ltk.2), $C, 'chip'>, ca_sk), $C), ~r2.1, <z, cip> ) ▶₁ #j2 ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), 'terminal' ) ▶₂ #j2 ) case CA_Sign_ltk - solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.3 ) - case TA_RESPONSE_T - solve( !KU( sign(<'CA', - cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), - $T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, - encaps(~k, pk(~ltk))>, - ~ltk.1) - ) @ #vk.5 ) + solve( !KU( sign(<'CA', + cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), + $T), + cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, + encaps(~k, pk(~ltk))>, + ~ltk.1) + ) @ #vk.3 ) + case CA_INIT_T + solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.15 ) case TA_RESPONSE_T - solve( !KU( sign(<'TA', ~id_c.1, ~r1.1>, ~ltk.1) ) @ #vk.40 ) - case TA_RESPONSE_T - solve( !KU( sign(<'CA', - cert(pk(~ltk.1), - sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), - cert(pk(~skC), sign(<pk(~skC), $C, 'chip'>, ca_sk), $C), - ~r2.1, encaps(~k.1, pk(~skC))>, - ~ltk.1) - ) @ #vk.43 ) + solve( !KU( sign(<'CA', + cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), + $T), + cert(pk(~skC), sign(<pk(~skC), $C, 'chip'>, ca_sk), $C), + ~r2.1, encaps(~k.1, pk(~skC))>, + ~ltk.1) + ) @ #vk.43 ) + case CA_INIT_T + solve( !KU( sign(<'TA', ~id_c.1, ~r1.1>, ~ltk.1) ) @ #vk.45 ) case TA_RESPONSE_T - solve( !KU( cert(z, sign(<z, x, 'chip'>, ca_sk), x) ) @ #vk.54 ) - case CA_Sign_ltk - solve( !KU( cert(z, sign(<z, x, 'chip'>, ca_sk), x) ) @ #vk.60 ) - case CA_Sign_ltk - solve( !KU( ~r2 ) @ #vk.47 ) + solve( !KU( ~r2 ) @ #vk.41 ) + case CA_INIT_C + solve( !KU( ~r2.1 ) @ #vk.51 ) + case CA_INIT_C + solve( !KU( ~id_c ) @ #vk.54 ) case TA_CHALLENGE_C - solve( !KU( ~r2.1 ) @ #vk.55 ) + solve( !KU( ~r1 ) @ #vk.55 ) case TA_CHALLENGE_C - solve( !KU( ~id_c ) @ #vk.56 ) + solve( !KU( ~id_c.1 ) @ #vk.56 ) case TA_CHALLENGE_C - solve( !KU( ~r1 ) @ #vk.57 ) + solve( !KU( ~r1.1 ) @ #vk.57 ) case TA_CHALLENGE_C - solve( !KU( ~id_c.1 ) @ #vk.59 ) - case TA_CHALLENGE_C - solve( !KU( ~r1.1 ) @ #vk.60 ) - case TA_CHALLENGE_C - solve( !KU( cert(pk(~skT), - sign(<pk(~skT), $T, 'terminal'>, ca_sk), - $T) - ) @ #vk.39 ) - case CA_Sign_ltk - solve( !KU( kdf(<'CNF', - cert(pk(~skT), - sign(<pk(~skT), $T, 'terminal'>, - ca_sk), - $T), - cert(pk(~ltk), - sign(<pk(~ltk), $C, 'chip'>, - ca_sk), - $C), - ~r2, encaps(~k, pk(~ltk))>, - ~k) - ) @ #vk.42 ) - case TA_COMPLETE_C - solve( !KU( cert(pk(~ltk), - sign(<pk(~ltk), $C, 'chip'>, ca_sk), - $C) - ) @ #vk.52 ) + solve( !KU( cert(pk(~skT), + sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T) + ) @ #vk.32 ) + case CA_Sign_ltk + solve( !KU( kdf(<'CNF', + cert(pk(~skT), + sign(<pk(~skT), $T, 'terminal'>, + ca_sk), + $T), + cert(pk(~ltk), + sign(<pk(~ltk), $C, 'chip'>, ca_sk), + $C), + ~r2, encaps(~k, pk(~ltk))>, + ~k) + ) @ #vk.36 ) + case CA_FINISH_C + solve( !KU( cert(pk(~ltk), + sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C) + ) @ #vk.47 ) + case CA_INIT_C + solve( !KU( sign(<'TA', ~id_c.4, ~r1.4>, x) ) @ #vk.60 ) + case TA_RESPONSE_T + solve( !KU( cert(pk(~skT.3), + sign(<pk(~skT.3), z, 'terminal'>, + ca_sk), + z) + ) @ #vk.62 ) case CA_Sign_ltk - solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.37 ) - case TA_RESPONSE_T - solve( !KU( cert(pk(~ltk.1), - sign(<pk(~ltk.1), $T, 'terminal' - >, - ca_sk), - $T) - ) @ #vk.55 ) - case CA_Sign_ltk - solve( !KU( kdf(<'CNF', - cert(pk(~ltk.1), - sign(<pk(~ltk.1), $T, - 'terminal'>, - ca_sk), - $T), - cert(pk(~skC), - sign(<pk(~skC), $C, 'chip' - >, - ca_sk), - $C), - ~r2.1, encaps(~k.1, pk(~skC))>, - ~k.1) - ) @ #vk.56 ) - case TA_COMPLETE_C - solve( !KU( cert(pk(~skC), - sign(<pk(~skC), $C, 'chip'>, + solve( !KU( ~id_c.4 ) @ #vk.64 ) + case TA_CHALLENGE_C + solve( !KU( ~r1.3 ) @ #vk.65 ) + case TA_CHALLENGE_C + solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.36 ) + case CA_INIT_T + solve( !KU( cert(pk(~ltk.1), + sign(<pk(~ltk.1), $T, + 'terminal'>, ca_sk), - $C) - ) @ #vk.59 ) + $T) + ) @ #vk.61 ) case CA_Sign_ltk - solve( !KU( encaps(~k.1, pk(~skC)) - ) @ #vk.57 ) - case TA_RESPONSE_T - SOLVED // trace found + solve( !KU( kdf(<'CNF', + cert(pk(~ltk.1), + sign(<pk(~ltk.1), $T, + 'terminal'>, + ca_sk), + $T), + cert(pk(~skC), + sign(<pk(~skC), $C, + 'chip'>, + ca_sk), + $C), + ~r2.1, + encaps(~k.1, pk(~skC))>, + ~k.1) + ) @ #vk.62 ) + case CA_FINISH_C + solve( !KU( cert(pk(~skC), + sign(<pk(~skC), $C, + 'chip'>, + ca_sk), + $C) + ) @ #vk.63 ) + case CA_INIT_C + solve( !KU( sign(<'TA', ~id_c.5, ~r1.5>, + x) + ) @ #vk.68 ) + case TA_RESPONSE_T + solve( !KU( cert(pk(~skT.4), + sign(<pk(~skT.4), z, + 'terminal'>, + ca_sk), + z) + ) @ #vk.70 ) + case CA_Sign_ltk + solve( !KU( ~id_c.5 ) @ #vk.72 ) + case TA_CHALLENGE_C + solve( !KU( ~r1.4 ) @ #vk.73 ) + case TA_CHALLENGE_C + solve( !KU( encaps(~k.1, + pk(~skC)) + ) @ #vk.71 ) + case CA_INIT_T + SOLVED // trace found + qed + qed + qed + qed + qed + qed qed qed qed @@ -2539,7 +2540,7 @@ guarded formula characterizing all counter-examples: */ simplify solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t ) case CA_Sign_ltk solve( Completed( k.1, @@ -2547,11 +2548,11 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), r2, encaps(~k, z)>, C, 'chip', T.1 ) @ #i ) - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid>, - cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), id_c, r1, r2 + case CA_FINISH_C + solve( CAInitC( <$C, iid>, + cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), id_c, r1, r2 ) ▶₁ #i ) - case TA_CHALLENGE_C + case CA_INIT_C solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) case Generate_chip_key_pair solve( !Cert( $C, cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), 'chip' @@ -2583,7 +2584,7 @@ guarded formula characterizing all counter-examples: */ simplify solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t ) case CA_Sign_ltk solve( Completed( k.1, @@ -2595,48 +2596,48 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) solve( CAInitT( <$T.1, iid>, id_c, cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, <k.1, encaps(~k, z)> ) ▶₁ #i ) - case TA_RESPONSE_T + case CA_INIT_T solve( !KU( kdf(<'CNF', cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, encaps(~k, z)>, ~k) ) @ #vk.1 ) - case TA_COMPLETE_C + case CA_FINISH_C by contradiction /* from formulas */ next case c_kdf - solve( !KU( ~k ) @ #vk.18 ) - case TA_RESPONSE_T + solve( !KU( ~k ) @ #vk.20 ) + case CA_INIT_T solve( !KU( cert(pk(sk), sign(<pk(sk), C, 'chip'>, ca_sk), C) - ) @ #vk.13 ) - case CA_Sign_ltk - solve( !KU( ~ltk.1 ) @ #vk.23 ) + ) @ #vk.12 ) + case CA_INIT_C + solve( !KU( ~ltk.1 ) @ #vk.25 ) case Corrupt_ltk by contradiction /* from formulas */ qed next - case TA_CHALLENGE_C - solve( !KU( ~ltk.1 ) @ #vk.23 ) + case CA_Sign_ltk + solve( !KU( ~ltk.1 ) @ #vk.25 ) case Corrupt_ltk by contradiction /* from formulas */ qed next case c_cert - solve( !KU( sign(<pk(sk), C, 'chip'>, ca_sk) ) @ #vk.25 ) - case CA_Sign_ltk - solve( !KU( ~ltk.1 ) @ #vk.24 ) + solve( !KU( sign(<pk(sk), C, 'chip'>, ca_sk) ) @ #vk.27 ) + case CA_INIT_C + solve( !KU( ~ltk.1 ) @ #vk.26 ) case Corrupt_ltk by contradiction /* from formulas */ qed next - case TA_CHALLENGE_C - solve( !KU( ~ltk.1 ) @ #vk.24 ) + case CA_Sign_ltk + solve( !KU( ~ltk.1 ) @ #vk.26 ) case Corrupt_ltk by contradiction /* from formulas */ qed next case c_sign - by solve( !KU( ca_sk ) @ #vk.29 ) + by solve( !KU( ca_sk ) @ #vk.31 ) qed qed qed @@ -2664,7 +2665,7 @@ guarded formula characterizing all counter-examples: */ simplify solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t ) case CA_Sign_ltk solve( Completed( k.1, @@ -2672,11 +2673,11 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), r2, encaps(~k, z)>, C, 'chip', T.1 ) @ #i ) - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid>, - cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), id_c, r1, r2 + case CA_FINISH_C + solve( CAInitC( <$C, iid>, + cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), id_c, r1, r2 ) ▶₁ #i ) - case TA_CHALLENGE_C + case CA_INIT_C solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) case Generate_chip_key_pair solve( !Cert( $C, cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), 'chip' @@ -2687,24 +2688,24 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) by contradiction /* from formulas */ next case split_case_2 - solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.18 ) - case TA_RESPONSE_T - solve( !KU( sign(<'CA', - cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, - encaps(~k, pk(~ltk))>, - ~ltk.1) - ) @ #vk.21 ) + solve( !KU( sign(<'CA', + cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), + cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, + encaps(~k, pk(~ltk))>, + ~ltk.1) + ) @ #vk.20 ) + case CA_INIT_T + solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.28 ) case TA_RESPONSE_T solve( !KU( kdf(<'CNF', cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, encaps(~k, pk(~ltk))>, ~k) - ) @ #vk.4 ) + ) @ #vk.5 ) case c_kdf solve( !KU( ~k ) @ #vk.40 ) - case TA_RESPONSE_T + case CA_INIT_T solve( !KU( ~ltk ) @ #vk.42 ) case Corrupt_ltk by contradiction /* from formulas */ @@ -2713,14 +2714,14 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) qed next case c_sign - solve( !KU( ~ltk.1 ) @ #vk.40 ) + solve( !KU( ~skT ) @ #vk.33 ) case Corrupt_ltk by contradiction /* from formulas */ qed qed next case c_sign - solve( !KU( ~ltk.1 ) @ #vk.29 ) + solve( !KU( ~ltk.1 ) @ #vk.36 ) case Corrupt_ltk by contradiction /* from formulas */ qed @@ -2751,7 +2752,7 @@ guarded formula characterizing all counter-examples: */ simplify solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t ) case CA_Sign_ltk solve( Completed( k.1, @@ -2763,48 +2764,48 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) solve( CAInitT( <$T.1, iid>, id_c, cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, <k.1, encaps(~k, z)> ) ▶₁ #i ) - case TA_RESPONSE_T + case CA_INIT_T solve( !KU( kdf(<'CNF', cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, encaps(~k, z)>, ~k) ) @ #vk.1 ) - case TA_COMPLETE_C + case CA_FINISH_C by contradiction /* from formulas */ next case c_kdf - solve( !KU( ~k ) @ #vk.18 ) - case TA_RESPONSE_T + solve( !KU( ~k ) @ #vk.20 ) + case CA_INIT_T solve( !KU( cert(pk(sk), sign(<pk(sk), C, 'chip'>, ca_sk), C) - ) @ #vk.13 ) - case CA_Sign_ltk - solve( !KU( ~ltk.1 ) @ #vk.23 ) + ) @ #vk.12 ) + case CA_INIT_C + solve( !KU( ~ltk.1 ) @ #vk.25 ) case Corrupt_ltk by contradiction /* from formulas */ qed next - case TA_CHALLENGE_C - solve( !KU( ~ltk.1 ) @ #vk.23 ) + case CA_Sign_ltk + solve( !KU( ~ltk.1 ) @ #vk.25 ) case Corrupt_ltk by contradiction /* from formulas */ qed next case c_cert - solve( !KU( sign(<pk(sk), C, 'chip'>, ca_sk) ) @ #vk.25 ) - case CA_Sign_ltk - solve( !KU( ~ltk.1 ) @ #vk.24 ) + solve( !KU( sign(<pk(sk), C, 'chip'>, ca_sk) ) @ #vk.27 ) + case CA_INIT_C + solve( !KU( ~ltk.1 ) @ #vk.26 ) case Corrupt_ltk by contradiction /* from formulas */ qed next - case TA_CHALLENGE_C - solve( !KU( ~ltk.1 ) @ #vk.24 ) + case CA_Sign_ltk + solve( !KU( ~ltk.1 ) @ #vk.26 ) case Corrupt_ltk by contradiction /* from formulas */ qed next case c_sign - by solve( !KU( ca_sk ) @ #vk.29 ) + by solve( !KU( ca_sk ) @ #vk.31 ) qed qed qed @@ -2830,7 +2831,7 @@ guarded formula characterizing all counter-examples: */ simplify solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t ) case CA_Sign_ltk solve( Completed( k.1, @@ -2838,60 +2839,60 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), r2, encaps(~k, z)>, A, role, B ) @ #i ) + case CA_FINISH_C + by contradiction /* from formulas */ + next case CA_FINISH_T solve( CAInitT( <$T.1, iid>, id_c, cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, <k.1, encaps(~k, z)> ) ▶₁ #i ) - case TA_RESPONSE_T + case CA_INIT_T solve( !KU( kdf(<'CNF', cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, encaps(~k, z)>, ~k) ) @ #vk.1 ) - case TA_COMPLETE_C + case CA_FINISH_C by contradiction /* from formulas */ next case c_kdf - solve( !KU( ~k ) @ #vk.18 ) - case TA_RESPONSE_T + solve( !KU( ~k ) @ #vk.20 ) + case CA_INIT_T solve( !KU( cert(pk(sk), sign(<pk(sk), B, 'chip'>, ca_sk), B) - ) @ #vk.13 ) - case CA_Sign_ltk - solve( !KU( ~ltk.1 ) @ #vk.23 ) + ) @ #vk.12 ) + case CA_INIT_C + solve( !KU( ~ltk.1 ) @ #vk.25 ) case Corrupt_ltk by contradiction /* from formulas */ qed next - case TA_CHALLENGE_C - solve( !KU( ~ltk.1 ) @ #vk.23 ) + case CA_Sign_ltk + solve( !KU( ~ltk.1 ) @ #vk.25 ) case Corrupt_ltk by contradiction /* from formulas */ qed next case c_cert - solve( !KU( sign(<pk(sk), B, 'chip'>, ca_sk) ) @ #vk.25 ) - case CA_Sign_ltk - solve( !KU( ~ltk.1 ) @ #vk.24 ) + solve( !KU( sign(<pk(sk), B, 'chip'>, ca_sk) ) @ #vk.27 ) + case CA_INIT_C + solve( !KU( ~ltk.1 ) @ #vk.26 ) case Corrupt_ltk by contradiction /* from formulas */ qed next - case TA_CHALLENGE_C - solve( !KU( ~ltk.1 ) @ #vk.24 ) + case CA_Sign_ltk + solve( !KU( ~ltk.1 ) @ #vk.26 ) case Corrupt_ltk by contradiction /* from formulas */ qed next case c_sign - by solve( !KU( ca_sk ) @ #vk.29 ) + by solve( !KU( ca_sk ) @ #vk.31 ) qed qed qed qed qed - next - case TA_COMPLETE_C - by contradiction /* from formulas */ qed qed qed @@ -2916,9 +2917,34 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) ) solve( (#i < #j) ∥ (#j < #i) ) case case_1 solve( Completed( k, sid, A, role, B ) @ #i ) + case CA_FINISH_C + solve( CAInitC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 ) ▶₁ #i ) + case CA_INIT_C + solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) + case Generate_chip_key_pair + solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) + case CA_Sign_ltk + solve( Completed( kdf(<'KEY', + cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B), + cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cip>, + z), + sid2, $C, 'chip', B + ) @ #j ) + case CA_FINISH_C + solve( CAInitC( <$C, iid.1>, + cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B), id_c.1, r1.1, ~r2 + ) ▶₁ #j ) + case CA_INIT_C + by contradiction /* cyclic */ + qed + qed + qed + qed + qed + next case CA_FINISH_T solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #i ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, certT, 'terminal' ) ▶₂ #i ) case CA_Sign_ltk solve( Completed( kdf(<'KEY', @@ -2931,17 +2957,19 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) ) solve( CAInitT( <$T, iid.1>, id_c.1, cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, <~k, encaps(~k, z)> ) ▶₁ #j ) - case TA_RESPONSE_T + case CA_INIT_T by contradiction /* cyclic */ qed qed qed qed - next - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 - ) ▶₁ #i ) - case TA_CHALLENGE_C + qed + next + case case_2 + solve( Completed( k, sid, A, role, B ) @ #i ) + case CA_FINISH_C + solve( CAInitC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 ) ▶₁ #i ) + case CA_INIT_C solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) case Generate_chip_key_pair solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) @@ -2952,24 +2980,21 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) ) z), sid2, $C, 'chip', B ) @ #j ) - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid.1>, - cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B), id_c.1, r1.1, ~r2 + case CA_FINISH_C + solve( CAInitC( <$C, iid.1>, + cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B), id_c.1, r1.1, ~r2 ) ▶₁ #j ) - case TA_CHALLENGE_C + case CA_INIT_C by contradiction /* cyclic */ qed qed qed qed qed - qed - next - case case_2 - solve( Completed( k, sid, A, role, B ) @ #i ) + next case CA_FINISH_T solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #i ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, certT, 'terminal' ) ▶₂ #i ) case CA_Sign_ltk solve( Completed( kdf(<'KEY', @@ -2982,64 +3007,20 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) ) solve( CAInitT( <$T, iid.1>, id_c.1, cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, <~k, encaps(~k, z)> ) ▶₁ #j ) - case TA_RESPONSE_T + case CA_INIT_T by contradiction /* cyclic */ qed qed qed qed - next - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 - ) ▶₁ #i ) - case TA_CHALLENGE_C - solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) - case Generate_chip_key_pair - solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) - case CA_Sign_ltk - solve( Completed( kdf(<'KEY', - cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cip>, - z), - sid2, $C, 'chip', B - ) @ #j ) - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid.1>, - cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B), id_c.1, r1.1, ~r2 - ) ▶₁ #j ) - case TA_CHALLENGE_C - by contradiction /* cyclic */ - qed - qed - qed - qed - qed qed qed next case case_2 solve( Completed( k, sid, A, role, B ) @ #i ) - case CA_FINISH_T - solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #i ) - case TA_RESPONSE_T - solve( !Cert( $T, certT, 'terminal' ) ▶₂ #i ) - case CA_Sign_ltk - solve( Completed( kdf(<'KEY', - cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), - cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, encaps(~k, z)>, - ~k), - sid2, $T, 'terminal', B - ) @ #j ) - case CA_FINISH_T - by contradiction /* from formulas */ - qed - qed - qed - next - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 - ) ▶₁ #i ) - case TA_CHALLENGE_C + case CA_FINISH_C + solve( CAInitC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 ) ▶₁ #i ) + case CA_INIT_C solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) case Generate_chip_key_pair solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) @@ -3050,12 +3031,29 @@ next z), sid2, $C, 'chip', B ) @ #j ) - case TA_COMPLETE_C + case CA_FINISH_C by contradiction /* from formulas */ qed qed qed qed + next + case CA_FINISH_T + solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #i ) + case CA_INIT_T + solve( !Cert( $T, certT, 'terminal' ) ▶₂ #i ) + case CA_Sign_ltk + solve( Completed( kdf(<'KEY', + cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), + cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, encaps(~k, z)>, + ~k), + sid2, $T, 'terminal', B + ) @ #j ) + case CA_FINISH_T + by contradiction /* from formulas */ + qed + qed + qed qed qed @@ -3075,10 +3073,9 @@ guarded formula characterizing all counter-examples: */ simplify solve( Completed( k, sid, C, 'chip', T ) @ #i ) - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 - ) ▶₁ #i ) - case TA_CHALLENGE_C + case CA_FINISH_C + solve( CAInitC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 ) ▶₁ #i ) + case CA_INIT_C solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) case Generate_chip_key_pair solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) @@ -3092,7 +3089,7 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) solve( CAInitT( <$T, iid.1>, id_c.1, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <k, cip> ) ▶₁ #j ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), 'terminal' ) ▶₂ #j ) @@ -3102,24 +3099,24 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) by contradiction /* from formulas */ next case split_case_2 - solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.3 ) - case TA_RESPONSE_T - solve( !KU( sign(<'CA', - cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, - encaps(~k, pk(~ltk))>, - ~ltk.1) - ) @ #vk.5 ) + solve( !KU( sign(<'CA', + cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), + cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, + encaps(~k, pk(~ltk))>, + ~ltk.1) + ) @ #vk.3 ) + case CA_INIT_T + solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.11 ) case TA_RESPONSE_T solve( !KU( kdf(<'CNF', cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, encaps(~k, pk(~ltk))>, ~k) - ) @ #vk.14 ) + ) @ #vk.16 ) case c_kdf solve( !KU( ~k ) @ #vk.40 ) - case TA_RESPONSE_T + case CA_INIT_T solve( !KU( ~ltk ) @ #vk.42 ) case Corrupt_ltk by contradiction /* from formulas */ @@ -3128,18 +3125,18 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) qed next case c_sign - solve( !KU( ~ltk.1 ) @ #vk.40 ) + solve( !KU( ~skT ) @ #vk.33 ) case Corrupt_ltk solve( !KU( kdf(<'CNF', - cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), + cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, encaps(~k, pk(~ltk))>, ~k) - ) @ #vk.19 ) + ) @ #vk.17 ) case c_kdf - solve( !KU( ~k ) @ #vk.43 ) - case TA_RESPONSE_T - solve( !KU( ~ltk ) @ #vk.45 ) + solve( !KU( ~k ) @ #vk.42 ) + case CA_INIT_T + solve( !KU( ~ltk ) @ #vk.44 ) case Corrupt_ltk by contradiction /* from formulas */ qed @@ -3149,25 +3146,20 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) qed next case c_sign - solve( !KU( ~ltk.1 ) @ #vk.29 ) + solve( !KU( ~ltk.1 ) @ #vk.36 ) case Corrupt_ltk - solve( !KU( sign(<'CA', - cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, - encaps(~k, pk(~ltk))>, - ~ltk.1) - ) @ #vk.6 ) + solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.14 ) case TA_RESPONSE_T solve( !KU( kdf(<'CNF', - cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), + cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, encaps(~k, pk(~ltk))>, ~k) - ) @ #vk.15 ) + ) @ #vk.21 ) case c_kdf - solve( !KU( ~k ) @ #vk.38 ) - case TA_RESPONSE_T - solve( !KU( ~ltk ) @ #vk.40 ) + solve( !KU( ~k ) @ #vk.43 ) + case CA_INIT_T + solve( !KU( ~ltk ) @ #vk.45 ) case Corrupt_ltk by contradiction /* from formulas */ qed @@ -3180,11 +3172,11 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, encaps(~k, pk(~ltk))>, ~k) - ) @ #vk.17 ) + ) @ #vk.21 ) case c_kdf - solve( !KU( ~k ) @ #vk.40 ) - case TA_RESPONSE_T - solve( !KU( ~ltk ) @ #vk.42 ) + solve( !KU( ~k ) @ #vk.44 ) + case CA_INIT_T + solve( !KU( ~ltk ) @ #vk.46 ) case Corrupt_ltk by contradiction /* from formulas */ qed @@ -3221,10 +3213,9 @@ guarded formula characterizing all counter-examples: */ simplify solve( Completed( k, sid, C, 'chip', T ) @ #i ) - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 - ) ▶₁ #i ) - case TA_CHALLENGE_C + case CA_FINISH_C + solve( CAInitC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 ) ▶₁ #i ) + case CA_INIT_C solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) case Generate_chip_key_pair solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) @@ -3241,32 +3232,32 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) solve( CAInitT( <$T, iid.1>, id_c.1, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip> ) ▶₁ #j ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), 'terminal' ) ▶₂ #j ) case CA_Sign_ltk - solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.4 ) - case TA_RESPONSE_T - solve( !KU( sign(<'CA', - cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, - encaps(~k, pk(~ltk))>, - ~ltk.1) - ) @ #vk.6 ) + solve( !KU( sign(<'CA', + cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), + cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, + encaps(~k, pk(~ltk))>, + ~ltk.1) + ) @ #vk.4 ) + case CA_INIT_T + solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.12 ) case TA_RESPONSE_T solve( !KU( kdf(<'KEY', cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, encaps(~k, pk(~ltk))>, ~k) - ) @ #vk.3 ) + ) @ #vk.4 ) case Reveal_session by contradiction /* from formulas */ next case c_kdf solve( !KU( ~k ) @ #vk.41 ) - case TA_RESPONSE_T + case CA_INIT_T solve( !KU( ~ltk ) @ #vk.43 ) case Corrupt_ltk by contradiction /* from formulas */ @@ -3275,10 +3266,10 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) qed next case c_sign - solve( !KU( ~ltk.1 ) @ #vk.41 ) + solve( !KU( ~skT ) @ #vk.34 ) case Corrupt_ltk solve( !KU( kdf(<'KEY', - cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), + cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, encaps(~k, pk(~ltk))>, ~k) @@ -3287,9 +3278,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) by contradiction /* from formulas */ next case c_kdf - solve( !KU( ~k ) @ #vk.44 ) - case TA_RESPONSE_T - solve( !KU( ~ltk ) @ #vk.46 ) + solve( !KU( ~k ) @ #vk.43 ) + case CA_INIT_T + solve( !KU( ~ltk ) @ #vk.45 ) case Corrupt_ltk by contradiction /* from formulas */ qed @@ -3299,17 +3290,12 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) qed next case c_sign - solve( !KU( ~ltk.1 ) @ #vk.30 ) + solve( !KU( ~ltk.1 ) @ #vk.37 ) case Corrupt_ltk - solve( !KU( sign(<'CA', - cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, - encaps(~k, pk(~ltk))>, - ~ltk.1) - ) @ #vk.7 ) + solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.15 ) case TA_RESPONSE_T solve( !KU( kdf(<'KEY', - cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), + cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, encaps(~k, pk(~ltk))>, ~k) @@ -3318,9 +3304,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) by contradiction /* from formulas */ next case c_kdf - solve( !KU( ~k ) @ #vk.39 ) - case TA_RESPONSE_T - solve( !KU( ~ltk ) @ #vk.41 ) + solve( !KU( ~k ) @ #vk.44 ) + case CA_INIT_T + solve( !KU( ~ltk ) @ #vk.46 ) case Corrupt_ltk by contradiction /* from formulas */ qed @@ -3338,9 +3324,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) by contradiction /* from formulas */ next case c_kdf - solve( !KU( ~k ) @ #vk.41 ) - case TA_RESPONSE_T - solve( !KU( ~ltk ) @ #vk.43 ) + solve( !KU( ~k ) @ #vk.45 ) + case CA_INIT_T + solve( !KU( ~ltk ) @ #vk.47 ) case Corrupt_ltk by contradiction /* from formulas */ qed @@ -3370,54 +3356,11 @@ guarded formula characterizing all counter-examples: (∃ #m. (K( iid ) @ #m)) ∧ (∀ #m. (K( iid ) @ #m) ⇒ ¬(#i < #m))" */ simplify -solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 - ) ▶₁ #i ) +solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1 ) ▶₁ #i ) case TA_CHALLENGE_C - solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) - case Generate_chip_key_pair - solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) - case CA_Sign_ltk - solve( splitEqs(0) ) - case split_case_1 - solve( !KU( sign(<'TA', ~id_c, ~r1>, x) ) @ #vk.3 ) - case TA_RESPONSE_T - solve( !KU( sign(<'CA', - cert(pk(~skT), sign(<pk(~skT), T, 'terminal'>, ca_sk), T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cip>, - ~skT) - ) @ #vk.5 ) - case TA_RESPONSE_T - solve( !KU( cert(z, sign(<z, x, 'chip'>, ca_sk), x) ) @ #vk.19 ) - case CA_Sign_ltk - solve( !KU( ~iid ) @ #vk.12 ) - case TA_CHALLENGE_C - solve( !KU( ~id_c ) @ #vk.17 ) - case TA_CHALLENGE_C - solve( !KU( ~r1 ) @ #vk.19 ) - case TA_CHALLENGE_C - solve( !KU( ~r2 ) @ #vk.32 ) - case TA_CHALLENGE_C - solve( !KU( cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T) - ) @ #vk.19 ) - case CA_Sign_ltk - solve( !KU( cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C) - ) @ #vk.32 ) - case CA_Sign_ltk - solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.18 ) - case TA_RESPONSE_T - SOLVED // trace found - qed - qed - qed - qed - qed - qed - qed - qed - qed - qed - qed - qed + solve( !KU( ~iid ) @ #vk.6 ) + case CA_INIT_C + by contradiction /* cyclic */ qed qed @@ -3536,10 +3479,9 @@ guarded formula characterizing all counter-examples: */ simplify solve( Completed( k, sid, C, 'chip', T ) @ #i ) - case TA_COMPLETE_C - solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 - ) ▶₁ #i ) - case TA_CHALLENGE_C + case CA_FINISH_C + solve( CAInitC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 ) ▶₁ #i ) + case CA_INIT_C solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) case Generate_chip_key_pair solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) @@ -3556,56 +3498,66 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) solve( CAInitT( <$T, iid.1>, id_c.1, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip> ) ▶₁ #j ) - case TA_RESPONSE_T + case CA_INIT_T solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), 'terminal' ) ▶₂ #j ) case CA_Sign_ltk - solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.4 ) - case TA_RESPONSE_T - solve( !KU( sign(<'CA', - cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, - encaps(~k, pk(~ltk))>, - ~ltk.1) - ) @ #vk.6 ) + solve( !KU( sign(<'CA', + cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), + cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, + encaps(~k, pk(~ltk))>, + ~ltk.1) + ) @ #vk.4 ) + case CA_INIT_T + solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.12 ) case TA_RESPONSE_T solve( !KU( kdf(<'KEY', cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, encaps(~k, pk(~ltk))>, ~k) - ) @ #vk.3 ) + ) @ #vk.4 ) case c_kdf solve( !KU( ~k ) @ #vk.41 ) - case TA_RESPONSE_T + case CA_INIT_T solve( !KU( ~ltk ) @ #vk.43 ) case Corrupt_ltk - solve( !KU( cert(z, sign(<z, x, 'chip'>, ca_sk), x) ) @ #vk.41 ) - case CA_Sign_ltk - solve( !KU( ~r2 ) @ #vk.38 ) + solve( !KU( ~r2 ) @ #vk.36 ) + case CA_INIT_C + solve( !KU( ~id_c ) @ #vk.41 ) case TA_CHALLENGE_C - solve( !KU( ~id_c ) @ #vk.40 ) + solve( !KU( ~r1 ) @ #vk.42 ) case TA_CHALLENGE_C - solve( !KU( ~r1 ) @ #vk.41 ) - case TA_CHALLENGE_C - solve( !KU( cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T) - ) @ #vk.27 ) - case CA_Sign_ltk - solve( !KU( kdf(<'CNF', - cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), - $T), - cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), - ~r2, encaps(~k, pk(~ltk))>, - ~k) - ) @ #vk.31 ) - case TA_COMPLETE_C - solve( !KU( cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C) - ) @ #vk.40 ) - case CA_Sign_ltk - solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.28 ) - case TA_RESPONSE_T - SOLVED // trace found + solve( !KU( cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T) + ) @ #vk.26 ) + case CA_Sign_ltk + solve( !KU( kdf(<'CNF', + cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), + cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), + ~r2, encaps(~k, pk(~ltk))>, + ~k) + ) @ #vk.30 ) + case CA_FINISH_C + solve( !KU( cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C) + ) @ #vk.38 ) + case CA_INIT_C + solve( !KU( sign(<'TA', ~id_c.2, ~r1.2>, x) ) @ #vk.46 ) + case TA_RESPONSE_T + solve( !KU( cert(pk(~skT.2), sign(<pk(~skT.2), z, 'terminal'>, ca_sk), + z) + ) @ #vk.48 ) + case CA_Sign_ltk + solve( !KU( ~id_c.2 ) @ #vk.50 ) + case TA_CHALLENGE_C + solve( !KU( ~r1.1 ) @ #vk.51 ) + case TA_CHALLENGE_C + solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.31 ) + case CA_INIT_T + SOLVED // trace found + qed + qed + qed qed qed qed @@ -3674,10 +3626,10 @@ summary of summaries: analyzed: tmp.spthy - processing time: 754.39s + processing time: 98.76s - session_exist (exists-trace): verified (19 steps) - two_session_exist (exists-trace): verified (36 steps) + session_exist (exists-trace): verified (22 steps) + two_session_exist (exists-trace): verified (42 steps) weak_agreement_C (all-traces): verified (8 steps) weak_agreement_T (all-traces): verified (19 steps) agreement_C (all-traces): verified (19 steps) @@ -3686,9 +3638,9 @@ analyzed: tmp.spthy session_uniqueness (all-traces): verified (37 steps) consistency (all-traces): verified (31 steps) key_secrecy (all-traces): verified (33 steps) - chip_hiding (all-traces): falsified - found trace (16 steps) + chip_hiding (all-traces): verified (4 steps) nonRepudiation_terminal (exists-trace): verified (13 steps) nonRepudiation_chip (exists-trace): falsified - no trace found (7 steps) - pfs (all-traces): falsified - found trace (22 steps) + pfs (all-traces): falsified - found trace (25 steps) ============================================================================== -- GitLab