From 7a2d354bacefd4401e3198330c5d5884fccbbbe1 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Tue, 27 Nov 2012 21:55:54 +0100 Subject: [PATCH] Added Wimax models from compositionality paper. Previously we had not included the IEEE 802.16e Wimax PKM models to the Scyther distribution, although the models had been around for years. --- gui/Protocols/IEEE-WIMAX/pkmv2rsa.spdl | 46 ++++++++++ .../IEEE-WIMAX/pkmv2rsacorrected.spdl | 46 ++++++++++ gui/Protocols/IEEE-WIMAX/pkmv2satek.spdl | 63 ++++++++++++++ gui/Protocols/IEEE-WIMAX/pqr.spdl | 84 +++++++++++++++++++ gui/Protocols/IEEE-WIMAX/rsaplussatek.spdl | 74 ++++++++++++++++ .../IEEE-WIMAX/rsaplussatekcorrected.spdl | 73 ++++++++++++++++ 6 files changed, 386 insertions(+) create mode 100644 gui/Protocols/IEEE-WIMAX/pkmv2rsa.spdl create mode 100644 gui/Protocols/IEEE-WIMAX/pkmv2rsacorrected.spdl create mode 100644 gui/Protocols/IEEE-WIMAX/pkmv2satek.spdl create mode 100644 gui/Protocols/IEEE-WIMAX/pqr.spdl create mode 100644 gui/Protocols/IEEE-WIMAX/rsaplussatek.spdl create mode 100644 gui/Protocols/IEEE-WIMAX/rsaplussatekcorrected.spdl diff --git a/gui/Protocols/IEEE-WIMAX/pkmv2rsa.spdl b/gui/Protocols/IEEE-WIMAX/pkmv2rsa.spdl new file mode 100644 index 0000000..73133a7 --- /dev/null +++ b/gui/Protocols/IEEE-WIMAX/pkmv2rsa.spdl @@ -0,0 +1,46 @@ +/* + * PKMv2-RSA + * + * Initial model by: Sjouke Mauw, Sasa Radomirovic (2007) + * Model changes: Cas Cremers (Nov 2012) + * + * Analysed in: "A framework for compositional verification of security protocols" + * With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic. + * Information and Computation, Special issue on Computer Security: + * Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459, + * Elsevier, 2008. + */ + +// The protocol description + +protocol pkmv2rsa(MS,BS) +{ + role MS + { + fresh msrand, said: Nonce; + var prepak, bsrand: Nonce; + + send_rsa1(MS,BS, {msrand, said, MS}sk(MS) ); + recv_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) ); + send_rsa3(MS,BS, {bsrand}sk(MS) ); + + claim_rsai3(MS,Niagree); + claim_rsai4(MS,Nisynch); + claim_rsai5(MS,SKR,prepak); + } + + role BS + { + var msrand, said: Nonce; + fresh prepak, bsrand: Nonce; + + recv_rsa1(MS,BS, {msrand, said, MS}sk(MS) ); + send_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) ); + recv_rsa3(MS,BS, {bsrand}sk(MS) ); + + claim_rsar3(BS,Niagree); + claim_rsar4(BS,Nisynch); + claim_rsar5(BS,SKR,prepak); + } +} + diff --git a/gui/Protocols/IEEE-WIMAX/pkmv2rsacorrected.spdl b/gui/Protocols/IEEE-WIMAX/pkmv2rsacorrected.spdl new file mode 100644 index 0000000..4bd5205 --- /dev/null +++ b/gui/Protocols/IEEE-WIMAX/pkmv2rsacorrected.spdl @@ -0,0 +1,46 @@ +/* + * PKMv2-RSA + * + * Initial model by: Sjouke Mauw, Sasa Radomirovic (2007) + * Model changes: Cas Cremers (Nov 2012) + * + * Analysed in: "A framework for compositional verification of security protocols" + * With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic. + * Information and Computation, Special issue on Computer Security: + * Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459, + * Elsevier, 2008. + */ + +// The protocol description + +protocol pkmv2rsa(MS,BS) +{ + role MS + { + fresh msrand, said: Nonce; + var prepak, bsrand: Nonce; + + send_rsa1(MS,BS, {msrand, said, MS}sk(MS) ); + recv_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) ); + send_rsa3(MS,BS, {bsrand,BS}sk(MS) ); + + claim_rsai3(MS,Niagree); + claim_rsai4(MS,Nisynch); + claim_rsai5(MS,SKR,prepak); + } + + role BS + { + var msrand, said: Nonce; + fresh prepak, bsrand: Nonce; + + recv_rsa1(MS,BS, {msrand, said, MS}sk(MS) ); + send_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) ); + recv_rsa3(MS,BS, {bsrand,BS}sk(MS) ); + + claim_rsar3(BS,Niagree); + claim_rsar4(BS,Nisynch); + claim_rsar5(BS,SKR,prepak); + } +} + diff --git a/gui/Protocols/IEEE-WIMAX/pkmv2satek.spdl b/gui/Protocols/IEEE-WIMAX/pkmv2satek.spdl new file mode 100644 index 0000000..b166a1b --- /dev/null +++ b/gui/Protocols/IEEE-WIMAX/pkmv2satek.spdl @@ -0,0 +1,63 @@ +/* + * PKMv2-SA-TEK + * + * Initial model by: Sjouke Mauw, Sasa Radomirovic (2007) + * Model changes: Cas Cremers (Nov 2012) + * + * Analysed in: "A framework for compositional verification of security protocols" + * With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic. + * Information and Computation, Special issue on Computer Security: + * Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459, + * Elsevier, 2008. + */ + +// Setup + +hashfunction hash; +hashfunction prepak; +const akid; +const u,d; + +// The protocol description + +protocol pkmv2satek(MS,BS) +{ + role MS + { + fresh msrand': Nonce; + var bsrand', tek0, tek1: Nonce; + + recv_satek1(BS,MS, bsrand',akid, + hash(d,prepak(MS,BS),BS,MS,bsrand',akid) ); + send_satek2(MS,BS, msrand',bsrand',akid, + hash(u,prepak(MS,BS),BS,MS,msrand',bsrand',akid) ); + recv_satek3(BS,MS, + msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS)), + hash(d,prepak(MS,BS),msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS)))); + + claim_rsai3(MS,Niagree); + claim_rsai4(MS,Nisynch); + claim_rsai6(MS,SKR,tek0); + claim_rsai7(MS,SKR,tek1); + } + + role BS + { + var msrand': Nonce; + fresh bsrand', tek0, tek1: Nonce; + + send_satek1(BS,MS, bsrand',akid, + hash(d,prepak(MS,BS),BS,MS,bsrand',akid) ); + recv_satek2(MS,BS, msrand',bsrand',akid, + hash(u,prepak(MS,BS),BS,MS,msrand',bsrand',akid) ); + send_satek3(BS,MS, + msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS)), + hash(d,prepak(MS,BS),msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS)))); + + claim_rsar3(BS,Niagree); + claim_rsar4(BS,Nisynch); + claim_rsar6(BS,SKR,tek0); + claim_rsar7(BS,SKR,tek1); + } +} + diff --git a/gui/Protocols/IEEE-WIMAX/pqr.spdl b/gui/Protocols/IEEE-WIMAX/pqr.spdl new file mode 100644 index 0000000..731d369 --- /dev/null +++ b/gui/Protocols/IEEE-WIMAX/pqr.spdl @@ -0,0 +1,84 @@ +/* + * PKMv2-RSA + * + * Initial model by: Sjouke Mauw, Sasa Radomirovic (2007) + * Model changes: Cas Cremers (Nov 2012) + * + * Analysed in: "A framework for compositional verification of security protocols" + * With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic. + * Information and Computation, Special issue on Computer Security: + * Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459, + * Elsevier, 2008. + */ + +// Setup + +hashfunction hash; +hashfunction prepak; +const akid; +const u,d; + +// The protocol description + +protocol rsaplussatek(MS,BS) + +{ + role MS + { + fresh msrand, msrand', said, c: Nonce; + var prepak, bsrand, bsrand', tek0, tek1, tek2, tek3: Nonce; + + send_rsa1(MS,BS, {msrand, said, MS}sk(MS) ); + recv_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) ); + send_rsa3(MS,BS, {bsrand, BS}sk(MS) ); + + recv_satek1(BS,MS, bsrand',akid, + hash(d,prepak,BS,MS,bsrand',akid) ); + send_satek2(MS,BS, msrand',bsrand',akid, + hash(u,prepak,BS,MS,msrand',bsrand',akid) ); + recv_satek3(BS,MS, + msrand',bsrand',akid,{tek0,tek1}hash(prepak), + hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak))); + + send_tekup1(MS,BS,{c}hash(prepak)); + recv_tekup2(BS,MS,{c,tek2,tek3}hash(prepak)); + + claim_rsai3(MS,Niagree); + claim_rsai4(MS,Nisynch); + claim_rsai5(MS,SKR,prepak); + claim_rsai6(MS,SKR,tek0); + claim_rsai7(MS,SKR,tek1); + claim_rsar8(MS,SKR,tek2); + claim_rsar9(MS,SKR,tek3); + } + + role BS + { + var msrand, msrand', said, c: Nonce; + fresh prepak, bsrand, bsrand', tek0, tek1, tek2, tek3: Nonce; + + recv_rsa1(MS,BS, {msrand, said, MS}sk(MS) ); + send_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) ); + recv_rsa3(MS,BS, {bsrand, BS}sk(MS) ); + + send_satek1(BS,MS, bsrand',akid, + hash(d,prepak,BS,MS,bsrand',akid) ); + recv_satek2(MS,BS, msrand',bsrand',akid, + hash(u,prepak,BS,MS,msrand',bsrand',akid) ); + send_satek3(BS,MS, + msrand',bsrand',akid,{tek0,tek1}hash(prepak), + hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak))); + + recv_tekup1(MS,BS,{c}hash(prepak)); + send_tekup2(BS,MS,{c,tek2,tek3}hash(prepak)); + + claim_rsar3(BS,Niagree); + claim_rsar4(BS,Nisynch); + claim_rsar5(BS,SKR,prepak); + claim_rsar6(BS,SKR,tek0); + claim_rsar7(BS,SKR,tek1); + claim_rsar8(BS,SKR,tek2); + claim_rsar9(BS,SKR,tek3); + } +} + diff --git a/gui/Protocols/IEEE-WIMAX/rsaplussatek.spdl b/gui/Protocols/IEEE-WIMAX/rsaplussatek.spdl new file mode 100644 index 0000000..eb15dde --- /dev/null +++ b/gui/Protocols/IEEE-WIMAX/rsaplussatek.spdl @@ -0,0 +1,74 @@ +/* + * PKMv2-RSA + * + * Initial model by: Sjouke Mauw, Sasa Radomirovic (2007) + * Model changes: Cas Cremers (Nov 2012) + * + * Analysed in: "A framework for compositional verification of security protocols" + * With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic. + * Information and Computation, Special issue on Computer Security: + * Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459, + * Elsevier, 2008. + */ + +// Setup + +hashfunction hash; +hashfunction prepak; +const akid; +const u,d; + +// The protocol description + +protocol rsaplussatek(MS,BS) + +{ + role MS + { + fresh msrand, msrand', said: Nonce; + var prepak, bsrand, bsrand', tek0, tek1: Nonce; + + send_rsa1(MS,BS, {msrand, said, MS}sk(MS) ); + recv_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) ); + send_rsa3(MS,BS, {bsrand}sk(MS) ); + + recv_satek1(BS,MS, bsrand',akid, + hash(d,prepak,BS,MS,bsrand',akid) ); + send_satek2(MS,BS, msrand',bsrand',akid, + hash(u,prepak,BS,MS,msrand',bsrand',akid) ); + recv_satek3(BS,MS, + msrand',bsrand',akid,{tek0,tek1}hash(prepak), + hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak))); + + claim_rsai3(MS,Niagree); + claim_rsai4(MS,Nisynch); +// claim_rsai5(MS,SKR,prepak); +// claim_rsai6(MS,SKR,tek0); +// claim_rsai7(MS,SKR,tek1); + } + + role BS + { + var msrand, msrand', said: Nonce; + fresh prepak, bsrand, bsrand', tek0, tek1: Nonce; + + recv_rsa1(MS,BS, {msrand, said, MS}sk(MS) ); + send_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) ); + recv_rsa3(MS,BS, {bsrand}sk(MS) ); + + send_satek1(BS,MS, bsrand',akid, + hash(d,prepak,BS,MS,bsrand',akid) ); + recv_satek2(MS,BS, msrand',bsrand',akid, + hash(u,prepak,BS,MS,msrand',bsrand',akid) ); + send_satek3(BS,MS, + msrand',bsrand',akid,{tek0,tek1}hash(prepak), + hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak))); + + claim_rsar3(BS,Niagree); + claim_rsar4(BS,Nisynch); +// claim_rsar5(BS,SKR,prepak); +// claim_rsar6(BS,SKR,tek0); +// claim_rsar7(BS,SKR,tek1); + } +} + diff --git a/gui/Protocols/IEEE-WIMAX/rsaplussatekcorrected.spdl b/gui/Protocols/IEEE-WIMAX/rsaplussatekcorrected.spdl new file mode 100644 index 0000000..b8051d8 --- /dev/null +++ b/gui/Protocols/IEEE-WIMAX/rsaplussatekcorrected.spdl @@ -0,0 +1,73 @@ +/* + * PKMv2-RSA + * + * Initial model by: Sjouke Mauw, Sasa Radomirovic (2007) + * Model changes: Cas Cremers (Nov 2012) + * + * Analysed in: "A framework for compositional verification of security protocols" + * With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic. + * Information and Computation, Special issue on Computer Security: + * Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459, + * Elsevier, 2008. + */ + +// Setup + +hashfunction hash; +hashfunction prepak; +const akid; +const u,d; + +// The protocol description + +protocol rsaplussatek(MS,BS) + +{ + role MS + { + fresh msrand, msrand', said: Nonce; + var prepak, bsrand, bsrand', tek0, tek1: Nonce; + + send_rsa1(MS,BS, {msrand, said, MS}sk(MS) ); + recv_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) ); + send_rsa3(MS,BS, {bsrand, BS}sk(MS) ); + + recv_satek1(BS,MS, bsrand',akid, + hash(d,prepak,BS,MS,bsrand',akid) ); + send_satek2(MS,BS, msrand',bsrand',akid, + hash(u,prepak,BS,MS,msrand',bsrand',akid) ); + recv_satek3(BS,MS, + msrand',bsrand',akid,{tek0,tek1}hash(prepak), + hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak))); + + claim_rsai3(MS,Niagree); + claim_rsai4(MS,Nisynch); + claim_rsai5(MS,SKR,prepak); + claim_rsai6(MS,SKR,tek0); + claim_rsai7(MS,SKR,tek1); + } + + role BS + { + var msrand, msrand', said: Nonce; + fresh prepak, bsrand, bsrand', tek0, tek1: Nonce; + + recv_rsa1(MS,BS, {msrand, said, MS}sk(MS) ); + send_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) ); + recv_rsa3(MS,BS, {bsrand, BS}sk(MS) ); + + send_satek1(BS,MS, bsrand',akid, + hash(d,prepak,BS,MS,bsrand',akid) ); + recv_satek2(MS,BS, msrand',bsrand',akid, + hash(u,prepak,BS,MS,msrand',bsrand',akid) ); + send_satek3(BS,MS, + msrand',bsrand',akid,{tek0,tek1}hash(prepak), + hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak))); + + claim_rsar3(BS,Niagree); + claim_rsar4(BS,Nisynch); + claim_rsar5(BS,SKR,prepak); + claim_rsar6(BS,SKR,tek0); + claim_rsar7(BS,SKR,tek1); + } +}