[prev in list] [next in list] [prev in thread] [next in thread]
List: avispa-users
Subject: Re: [Avispa-users] Tighting security
From: "Tom Gao" <tom () tomgao ! com>
Date: 2011-04-02 7:41:15
Message-ID: 002d01cbf109$5a39fae0$0eadf0a0$ () tomgao ! com
[Download RAW message or body]
Thank you Tigran,
You were right the weakness was in A.
Do you know how I can strengthen security on A without having a return
message from Br as this is not how I planned my protocol. I've studied the
Alice Bob notation in the sample it seems when witness is only possible when
sending message from Alice and request is only initiated when message is
received on the 2nd message received from Alice.
I've tried to initiate secret, witness and request where I thought were
appropriate. However there is still weakness in A. Unless I structured the
HLPSL to have return message from Br which is not what I want.
Could everyone take a look at my protocol and recommend ways for
improvement.
Thank you,
Tom
_____
role alice (
A, Br: agent,
Kabr: public_key,
SND_ABR, RCV_ABR: channel (dy)
)
played_by A def=
local State : nat,
Ma : text
init State := 0
transition
0. State = 0 /\ RCV_ABR(start) =|>
State':= 1 /\ Ma' := new()
/\ SND_ABR({Ma'}_Kabr)
/\ secret(Ma',ma,{A,Br})
/\ witness(A,Br,broker_a_Ma,Ma')
/\ request(A,Br,broker_a_Ma,Ma')
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role broker(
A, Br, Db1, Db2, Db3, Db4, Bob: agent,
Kabr, Kbrdb1, Kbrdb2, Kbrdb3, Kbrdb4, Kbrbob: public_key,
SND_ABR, RCV_ABR,
SND_BRDB1, SND_BRDB2, SND_BRDB3, SND_BRDB4,
RCV_BRDB1, RCV_BRDB2, RCV_BRDB3, RCV_BRDB4,
SND_BRBOB, RCV_BRBOB : channel (dy)
)
played_by Br def=
local State : nat,
Ma, Ma1, Ma2, Ma3, Ma4, Mbr, Mbob: text
init State := 2
transition
%Respond back to Alice
2. State = 2 /\ RCV_ABR({Ma'}_Kabr) =|>
State':= 4 /\ Ma1' := new()
/\ SND_BRDB1({Ma1'}_Kbrdb1)
/\ secret(Ma1',ma1,{Br,Db1})
/\
witness(Br,Db1,broker_bdb1_Ma1,Ma1')
/\
request(Br,Db1,broker_bdb1_Ma1,Ma1')
4. State = 4 /\ RCV_BRDB1({Ma1'}_Kbrdb1) =|>
State':= 8 /\ Ma2' := new()
/\ SND_BRDB2({Ma2'}_Kbrdb2)
/\ secret(Ma2',ma2,{Br,Db2})
/\
witness(Br,Db2,broker_bdb2_Ma2,Ma2')
/\
request(Br,Db2,broker_bdb2_Ma2,Ma2')
6. State = 8 /\ RCV_BRDB2({Ma2'}_Kbrdb2) =|>
State':= 10 /\ Ma3' := new()
/\ SND_BRDB3({Ma3'}_Kbrdb3)
/\ secret(Ma3',ma3,{Br,Db3})
/\
witness(Br,Db3,broker_bdb3_Ma3,Ma3')
/\
request(Br,Db3,broker_bdb3_Ma3,Ma3')
8. State = 10 /\ RCV_BRDB3({Ma3'}_Kbrdb3) =|>
State':= 12 /\ Ma4' := new()
/\ SND_BRDB4({Ma4'}_Kbrdb4)
/\ secret(Ma4',ma4,{Br,Db4})
/\
witness(Br,Db4,broker_bdb4_Ma4,Ma4')
/\
request(Br,Db4,broker_bdb4_Ma4,Ma4')
10. State = 12 /\ RCV_BRDB4({Ma4'}_Kbrdb4) =|>
State':= 14 /\ Mbob' := new()
/\ SND_BRBOB({Mbob'}_Kbrbob)
/\ secret(Mbob',mb,{Br,Bob})
/\
witness(Br,Bob,broker_bbob_Mbob,Mbob')
/\
request(Br,Bob,broker_bbob_Mbob,Mbob')
12. State = 14 /\ RCV_BRBOB({Mbob'}_Kbrbob) =|>
State':= 16 /\ Mbob' := new()
/\ secret(Mbob',mb,{Br,Bob})
/\
witness(Br,Bob,broker_bbob_Mbob,Mbob')
/\
request(Br,Bob,broker_bbob_Mbob,Mbob')
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role db1(
Br, Db1: agent,
Kbrdb1: public_key,
SND_BRDB1, RCV_BRDB1: channel (dy)
)
played_by Db1 def=
local State : nat,
Ma1 : text
init State := 5
transition
3. State = 5 /\ RCV_BRDB1({Ma1'}_Kbrdb1) =|>
State':= 7 /\ SND_BRDB1({Ma1'}_Kbrdb1)
/\ secret(Ma1',ma1,{Db1,Br})
/\ witness(Db1,Br,db1_broker_Ma1,Ma1')
/\ request(Db1,Br,db1_broker_Ma1,Ma1')
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role db2(
Br, Db2: agent,
Kbrdb2: public_key,
SND_BRDB2, RCV_BRDB2: channel (dy)
)
played_by Db2 def=
local State : nat,
Ma2 : text
init State := 9
transition
5. State = 9 /\ RCV_BRDB2({Ma2'}_Kbrdb2) =|>
State':= 11 /\ SND_BRDB2({Ma2'}_Kbrdb2)
/\ secret(Ma2',ma2,{Db2,Br})
/\
witness(Db2,Br,db2_broker_Ma2,Ma2')
/\ request(Db2,Br,db2_broker_Ma2,Ma2')
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role db3(
Br, Db3: agent,
Kbrdb3: public_key,
SND_BRDB3, RCV_BRDB3: channel (dy)
)
played_by Db3 def=
local State : nat,
Ma3 : text
init State := 11
transition
7. State = 11 /\ RCV_BRDB3({Ma3'}_Kbrdb3) =|>
State':= 13 /\ SND_BRDB3({Ma3'}_Kbrdb3)
/\ secret(Ma3',ma3,{Db3,Br})
/\
witness(Db3,Br,db3_broker_Ma3,Ma3')
/\ request(Db3,Br,db3_broker_Ma3,Ma3')
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role db4(
Br, Db4: agent,
Kbrdb4: public_key,
SND_BRDB4, RCV_BRDB4: channel (dy)
)
played_by Db4 def=
local State : nat,
Ma4 : text
init State := 13
transition
9. State = 13 /\ RCV_BRDB4({Ma4'}_Kbrdb4) =|>
State':= 15 /\ SND_BRDB4({Ma4'}_Kbrdb4)
/\ secret(Ma4',ma4,{Db4,Br})
/\
witness(Db4,Br,db4_broker_Ma4,Ma4')
/\ request(Db4,Br,db4_broker_Ma4,Ma4')
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role bob(
Br, Bob: agent,
Kbrbob: public_key,
SND_BRBOB, RCV_BRBOB: channel (dy)
)
played_by Bob def=
local State : nat,
Mbob : text
init State := 17
transition
11. State = 17 /\ RCV_BRBOB({Mbob'}_Kbrbob) =|>
State':= 19 /\ SND_BRBOB({Mbob'}_Kbrbob)
/\ secret(Mbob',ma4,{Bob,Br})
/\
witness(Bob,Br,bob_broker_Mbob,Mbob')
/\
request(Bob,Br,bob_broker_Mbob,Mbob')
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role session(
A, Br, Db1, Db2, Db3, Db4, Bob: agent,
Kabr, Kbrdb1, Kbrdb2, Kbrdb3, Kbrdb4, Kbrbob: public_key
) def=
local SND_ABR, RCV_ABR,
SND_BRDB1, SND_BRDB2, SND_BRDB3, SND_BRDB4,
RCV_BRDB1, RCV_BRDB2, RCV_BRDB3, RCV_BRDB4,
SND_BRBOB, RCV_BRBOB : channel (dy)
composition
alice(A,Br,Kabr,SND_ABR,RCV_ABR)
/\ broker (A,Br,Db1,Db2,Db3,Db4,Bob,
Kabr,Kbrdb1,Kbrdb2,Kbrdb3,Kbrdb4,Kbrbob,
SND_ABR, RCV_ABR,
SND_BRDB1, SND_BRDB2, SND_BRDB3, SND_BRDB4,
RCV_BRDB1, RCV_BRDB2, RCV_BRDB3, RCV_BRDB4,
SND_BRBOB, RCV_BRBOB)
/\ db1 (Br,Db1,Kbrdb1,SND_BRDB1, RCV_BRDB1)
/\ db2 (Br,Db2,Kbrdb2,SND_BRDB2, RCV_BRDB2)
/\ db3 (Br,Db3,Kbrdb3,SND_BRDB3, RCV_BRDB3)
/\ db4 (Br,Db4,Kbrdb4,SND_BRDB4, RCV_BRDB4)
/\ bob (Br,Bob,Kbrbob,SND_BRBOB, RCV_BRBOB)
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
role environment() def=
const a, br, db1, db2, db3, db4, bob : agent,
kabr, kbrdb1, kbrdb2, kbrdb3, kbrdb4, kbrbob, ki : public_key,
ma, ma1, ma2, ma3, ma4, mb,
db1_broker_Ma1,
db2_broker_Ma2,
db3_broker_Ma3,
db4_broker_Ma4,
bob_broker_Mbob,
broker_a_Ma,
broker_bdb1_Ma1,
broker_bdb2_Ma2,
broker_bdb3_Ma3,
broker_bdb4_Ma4,
broker_bbob_Mbob : protocol_id
intruder_knowledge = {a, br, db1, db2, ki, inv(ki)}
composition
session(a,br,db1,db2,db3,db4,bob,kabr,kbrdb1,kbrdb2,kbrdb3,kbrdb4,kbrbob)
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
goal
secrecy_of ma, ma1, ma2, ma3, ma4, mb
authentication_on broker_a_Ma
authentication_on db1_broker_Ma1
authentication_on db2_broker_Ma2
authentication_on db3_broker_Ma3
authentication_on db4_broker_Ma4
authentication_on bob_broker_Mbob
authentication_on broker_bdb1_Ma1
authentication_on broker_bdb2_Ma2
authentication_on broker_bdb3_Ma3
authentication_on broker_bdb4_Ma4
authentication_on broker_bbob_Mbob
end goal
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
environment()
-----Original Message-----
>From: avispa-users-bounces@avispa-project.org
[mailto:avispa-users-bounces@avispa-project.org] On Behalf Of Tigran S.
Avanesov
Sent: Friday, 1 April 2011 11:33 PM
To: avispa-users@avispa-project.org
Subject: Re: [Avispa-users] Tighting security
Hi,
request(A,Br,a_broker_Ma,Ma')
causes your authentication attack.
You don't even have a corresponding "witness"
identified by
a_broker_Ma
Moreover, you don't have any witness in your specification, and thus, all
your authentication goals become meaningless.
Regadrs,
On 04/01/2011 02:23 PM, Tom Gao wrote:
> Hi Everyone,
>
> I'm trying to tighten the security of my shared secret implementation
> of HLPSL however I must have missed something for the AVISPA to still
> mark my HLPSL as unsafe.
>
> Any pointer to the right direction is appreciated.
>
>
> % OFMC
> % Version of 2006/02/13
> SUMMARY
> UNSAFE
> DETAILS
> ATTACK_FOUND
> PROTOCOL
> C:\progra~1\SPAN\testsuite\results\SharedSecret_Asymmetric.if
> GOAL
> authentication_on_a_broker_Ma
> BACKEND
> OFMC
> COMMENTS
> STATISTICS
> parseTime: 0.00s
> searchTime: 0.01s
> visitedNodes: 0 nodes
> depth: 0 plies
> ATTACK TRACE
> i -> (a,3): start
> (a,3) -> i: {Ma(1)}_kabr
>
>
> % Reached State:
> %
> % request(a,br,a_broker_Ma,Ma(1),3)
> % contains(a,set_181)
> % contains(br,set_181)
> % state_bob(bob,br,kbrbob,17,dummy_nonce,3)
> % state_db4(db4,br,kbrdb4,13,dummy_nonce,dummy_nonce,3)
> % state_db3(db3,br,kbrdb3,11,dummy_nonce,dummy_nonce,3)
> % state_db2(db2,br,kbrdb2,9,dummy_nonce,dummy_nonce,3)
> % state_db1(db1,br,kbrdb1,5,dummy_nonce,dummy_nonce,3)
> %
> state_broker(br,a,db1,db2,db3,db4,bob,kabr,kbrdb1,kbrdb2,kbrdb3,kbrdb4
> ,kbrbo
> b,2,dummy_nonce,dummy_nonce,dummy_nonce,dummy_nonce,dummy_nonce,dummy_
> nonce,
> dummy_nonce,set_188,set_189,set_190,set_191,set_192,set_193,3)
> % state_alice(a,br,kabr,1,Ma(1),dummy_nonce,dummy_nonce,set_181,3)
> % secret(Ma(1),ma,set_181)
>
>
> HLPSL
> ______________________
>
> role alice (
> A, Br: agent,
> Kabr: public_key,
> SND_ABR, RCV_ABR: channel (dy)
> )
>
>
> played_by A def=
>
> local State : nat,
> Ma, Mbr, Mdb1: text
>
> init State := 0
>
> transition
>
> 0. State = 0 /\ RCV_ABR(start) =|>
> State':= 1 /\ Ma' := new()
> /\
> SND_ABR({Ma'}_Kabr)
> /\
> secret(Ma',ma,{A,Br})
> /\
> request(A,Br,a_broker_Ma,Ma')
> end role
>
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %%
>
> role broker(
> A, Br, Db1, Db2, Db3, Db4, Bob: agent,
> Kabr, Kbrdb1, Kbrdb2, Kbrdb3, Kbrdb4, Kbrbob: public_key,
> SND_ABR, RCV_ABR,
> SND_BRDB1, SND_BRDB2, SND_BRDB3,
> SND_BRDB4,
>
> RCV_BRDB1, RCV_BRDB2, RCV_BRDB3,
> RCV_BRDB4,
>
> SND_BRBOB, RCV_BRBOB : channel (dy)
> )
>
>
> played_by Br def=
>
> local State : nat,
> Ma, Ma1, Ma2, Ma3, Ma4, Mbr, Mbob: text
>
>
> init State := 2
>
> transition
>
> 2. State = 2 /\ RCV_ABR({Ma'}_Kabr) =|>
> State':= 4 /\ Ma1' := new()
>
> /\ SND_BRDB1({Ma1'}_Kbrdb1)
>
> /\
> secret(Ma1',ma1,{Br,Db1})
>
> /\ request(Br,Db1,broker_bdb1_Ma1,Ma1')
>
>
> 4. State = 4 /\ RCV_BRDB1({Ma1'}_Kbrdb1) =|>
> State':= 8 /\ Ma2' := new()
>
> /\ SND_BRDB2({Ma2'}_Kbrdb2)
>
> /\
> secret(Ma2',ma2,{Br,Db2})
>
> /\ request(Br,Db2,broker_bdb2_Ma2,Ma2')
>
>
> 6. State = 8 /\ RCV_BRDB2({Ma2'}_Kbrdb2) =|>
> State':= 10 /\ Ma3' := new()
>
> /\ SND_BRDB3({Ma3'}_Kbrdb3)
>
> /\
> secret(Ma3',ma3,{Br,Db3})
>
> /\ request(Br,Db3,broker_bdb3_Ma3,Ma3')
>
>
> 8. State = 10 /\ RCV_BRDB3({Ma3'}_Kbrdb3) =|>
> State':= 12 /\ Ma4' := new()
>
> /\ SND_BRDB4({Ma4'}_Kbrdb4)
>
> /\
> secret(Ma4',ma4,{Br,Db4})
>
> /\ request(Br,Db4,broker_bdb4_Ma4,Ma4')
>
>
> 10. State = 12 /\ RCV_BRDB4({Ma4'}_Kbrdb4) =|>
> State':= 14 /\ Mbob' := new()
>
> /\ SND_BRBOB({Mbob'}_Kbrbob)
>
> /\
> secret(Mbob',mb,{Br,Bob})
>
> /\ request(Br,Bob,broker_bbob_Mbob,Mbob')
>
>
> 12. State = 14 /\ RCV_BRBOB({Mbob'}_Kbrbob) =|>
> State':= 16 /\ Mbob' := new()
>
> /\
> secret(Mbob',mb,{Br,Bob})
>
> /\ request(Br,Bob,broker_bbob_Mbob,Mbob')
>
> end role
>
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %%
>
> role db1(
> Br, Db1: agent,
> Kbrdb1: public_key,
> SND_BRDB1, RCV_BRDB1: channel (dy)
> )
>
>
> played_by Db1 def=
>
> local State : nat,
> Ma1, Mbr : text
>
> init State := 5
>
> transition
>
> 3. State = 5 /\ RCV_BRDB1({Ma1'}_Kbrdb1) =|>
> State':= 7 /\ SND_BRDB1({Ma1'}_Kbrdb1)
> /\
> request(Db1,Br,db1_broker_Ma1,Ma1')
>
>
> end role
>
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %%
>
>
> role db2(
> Br, Db2: agent,
> Kbrdb2: public_key,
> SND_BRDB2, RCV_BRDB2: channel (dy)
> )
>
>
> played_by Db2 def=
>
> local State : nat,
> Ma2, Mbr : text
>
> init State := 9
>
> transition
>
> 5. State = 9 /\ RCV_BRDB2({Ma2'}_Kbrdb2) =|>
> State':= 11 /\ SND_BRDB2({Ma2'}_Kbrdb2)
>
> /\
> request(Db2,Br,db2_broker_Ma2,Ma2')
>
> end role
>
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %%
>
>
> role db3(
> Br, Db3: agent,
> Kbrdb3: public_key,
> SND_BRDB3, RCV_BRDB3: channel (dy)
> )
>
>
> played_by Db3 def=
>
> local State : nat,
> Ma3, Mbr : text
>
> init State := 11
>
> transition
>
> 7. State = 11 /\ RCV_BRDB3({Ma3'}_Kbrdb3) =|>
> State':= 13 /\ SND_BRDB3({Ma3'}_Kbrdb3)
>
> /\
> request(Db3,Br,db3_broker_Ma3,Ma3')
>
> end role
>
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %%
>
>
> role db4(
> Br, Db4: agent,
> Kbrdb4: public_key,
> SND_BRDB4, RCV_BRDB4: channel (dy)
> )
>
>
> played_by Db4 def=
>
> local State : nat,
> Ma4, Mbr : text
>
> init State := 13
>
> transition
>
> 9. State = 13 /\ RCV_BRDB4({Ma4'}_Kbrdb4) =|>
> State':= 15 /\ SND_BRDB4({Ma4'}_Kbrdb4)
>
> /\
> request(Db4,Br,db4_broker_Ma4,Ma4')
>
> end role
>
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %%
>
> role bob(
> Br, Bob: agent,
> Kbrbob: public_key,
> SND_BRBOB, RCV_BRBOB: channel (dy)
> )
>
>
> played_by Bob def=
>
> local State : nat,
> Mbob : text
>
> init State := 17
>
> transition
>
> 11. State = 17 /\ RCV_BRBOB({Mbob'}_Kbrbob) =|>
> State':= 19 /\ SND_BRBOB({Mbob'}_Kbrbob)
>
> /\
> request(Bob,Br,bob_broker_Mbob,Mbob')
>
> end role
>
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %%
>
> role session(
> A, Br, Db1, Db2, Db3, Db4, Bob: agent,
> Kabr, Kbrdb1, Kbrdb2, Kbrdb3, Kbrdb4, Kbrbob: public_key
> ) def=
>
> local SND_ABR, RCV_ABR,
> SND_BRDB1, SND_BRDB2, SND_BRDB3, SND_BRDB4,
> RCV_BRDB1, RCV_BRDB2, RCV_BRDB3, RCV_BRDB4,
> SND_BRBOB, RCV_BRBOB : channel (dy)
>
>
>
> composition
>
> alice(A,Br,Kabr,SND_ABR,RCV_ABR)
> /\ broker (A,Br,Db1,Db2,Db3,Db4,Bob,
>
> Kabr,Kbrdb1,Kbrdb2,Kbrdb3,Kbrdb4,Kbrbob,
>
> SND_ABR, RCV_ABR,
>
> SND_BRDB1, SND_BRDB2, SND_BRDB3, SND_BRDB4,
>
> RCV_BRDB1, RCV_BRDB2, RCV_BRDB3, RCV_BRDB4,
>
> SND_BRBOB,
> RCV_BRBOB)
> /\ db1 (Br,Db1,Kbrdb1,SND_BRDB1, RCV_BRDB1)
> /\ db2 (Br,Db2,Kbrdb2,SND_BRDB2, RCV_BRDB2)
> /\ db3 (Br,Db3,Kbrdb3,SND_BRDB3, RCV_BRDB3)
> /\ db4 (Br,Db4,Kbrdb4,SND_BRDB4, RCV_BRDB4)
> /\ bob (Br,Bob,Kbrbob,SND_BRBOB, RCV_BRBOB)
>
>
> end role
>
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %%
>
> role environment() def=
>
> const a, br, db1, db2, db3, db4, bob : agent,
> kabr, kbrdb1, kbrdb2, kbrdb3, kbrdb4, kbrbob, ki :
> public_key,
>
> ma, ma1, ma2, ma3, ma4, mb,
>
> db1_broker_Ma1,
> db2_broker_Ma2,
> db3_broker_Ma3,
> db4_broker_Ma4,
> bob_broker_Mbob,
>
> a_broker_Ma,
> broker_bdb1_Ma1,
> broker_bdb2_Ma2,
> broker_bdb3_Ma3,
> broker_bdb4_Ma4,
> broker_bbob_Mbob : protocol_id
>
> intruder_knowledge = {db1}
>
> composition
>
>
>
> session(a,br,db1,db2,db3,db4,bob,kabr,kbrdb1,kbrdb2,kbrdb3,kbrdb4,kbrb
> ob)
>
> end role
>
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %%
>
> goal
>
> secrecy_of ma, ma1, ma2, ma3, ma4, mb
>
> authentication_on a_broker_Ma
> authentication_on db1_broker_Ma1
> authentication_on db2_broker_Ma2
> authentication_on db3_broker_Ma3
> authentication_on db4_broker_Ma4
> authentication_on bob_broker_Mbob
>
> authentication_on broker_bdb1_Ma1
> authentication_on broker_bdb2_Ma2
> authentication_on broker_bdb3_Ma3
> authentication_on broker_bdb4_Ma4
> authentication_on broker_bbob_Mbob
>
> end goal
>
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %%
>
> environment()
>
>
>
> Thank you.
> Tom
> _______________________________________________
> Avispa-users mailing list
> Avispa-users@avispa-project.org
> http://mail63.csoft.net/mailman/listinfo/avispa-users
>
_______________________________________________
Avispa-users mailing list
Avispa-users@avispa-project.org
http://mail63.csoft.net/mailman/listinfo/avispa-users
_______________________________________________
Avispa-users mailing list
Avispa-users@avispa-project.org
http://mail63.csoft.net/mailman/listinfo/avispa-users
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic