Commit 3d6cf6df authored by Joy Mitra's avatar Joy Mitra

restructuring

parent 3f41317d
No preview for this file type
......@@ -17,74 +17,74 @@ endfm
fmod PROTOCOL-SPECIFICATION is protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
eq STRANDS-DOLEVYAO =
eq STRANDS-DOLEVYAO =
:: nil ::
[ nil |
-(X:Msg),
+(sk(i, X:Msg)), nil] &
[ nil |
-(X:Msg),
+(sk(i, X:Msg)), nil] &
:: nil ::
[ nil |
-(Y:Msg),
-(X:Msg),
+(X:Msg ; Y:Msg), nil] &
[ nil |
-(Y:Msg),
-(X:Msg),
+(X:Msg ; Y:Msg), nil] &
:: nil ::
[ nil |
-(A:Name),
-(X:Msg),
+(pk(A:Name, X:Msg)), nil] &
[ nil |
-(A:Name),
-(X:Msg),
+(pk(A:Name, X:Msg)), nil] &
:: nil ::
[ nil |
-(X:Msg ; Y:Msg),
+(X:Msg), nil] &
[ nil |
-(X:Msg ; Y:Msg),
+(X:Msg), nil] &
:: nil ::
[ nil |
-(X:Msg ; Y:Msg),
+(Y:Msg), nil] &
[ nil |
-(X:Msg ; Y:Msg),
+(Y:Msg), nil] &
:: r1:Fresh ::
[ nil |
[ nil |
+(n(i, r1:Fresh)), nil] [nonexec].
eq STRANDS-PROTOCOL =
eq STRANDS-PROTOCOL =
:: r1:Fresh ::
[ nil |
+(pk(BName:Name, AName:Name ; n(AName:Name, r1:Fresh))),
-(pk(AName:Name, n(AName:Name, r1:Fresh) ; N2:Nonce)),
+(pk(BName:Name, N2:Nonce)), nil] &
[ nil |
+(pk(BName:Name, AName:Name ; n(AName:Name, r1:Fresh))),
-(pk(AName:Name, n(AName:Name, r1:Fresh) ; N2:Nonce)),
+(pk(BName:Name, N2:Nonce)), nil] &
:: r2:Fresh ::
[ nil |
-(pk(BName:Name, AName:Name ; N1:Nonce)),
+(pk(AName:Name, N1:Nonce ; n(BName:Name, r2:Fresh))),
[ nil |
-(pk(BName:Name, AName:Name ; N1:Nonce)),
+(pk(AName:Name, N1:Nonce ; n(BName:Name, r2:Fresh))),
-(pk(BName:Name, n(BName:Name, r2:Fresh))), nil] [nonexec].
var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)=
var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)=
:: r2:Fresh ::
[ nil,
-(pk(b, a ; N1:Nonce)),
+(pk(a, N1:Nonce ; n(b, r2:Fresh))),
-(pk(b, n(b, r2:Fresh))) | nil]
||
[ nil,
-(pk(b, a ; N1:Nonce)),
+(pk(a, N1:Nonce ; n(b, r2:Fresh))),
-(pk(b, n(b, r2:Fresh))) | nil]
||
n(b, r2:Fresh) inI
||
||
nil
||
||
nil
||
||
nil[nonexec].
eq ATTACK-STATE(1)=
eq ATTACK-STATE(1)=
:: r2:Fresh ::
[ nil,
-(pk(b, a ; N1:Nonce)),
+(pk(a, N1:Nonce ; n(b, r2:Fresh))),
-(pk(b, n(b, r2:Fresh))) | nil]
||
[ nil,
-(pk(b, a ; N1:Nonce)),
+(pk(a, N1:Nonce ; n(b, r2:Fresh))),
-(pk(b, n(b, r2:Fresh))) | nil]
||
n(b, r2:Fresh) inI
||
||
nil
||
||
nil
|| never((S &
|| never((S &
:: r1:Fresh ::
[ nil,
+(pk(b, a ; n(a, r1:Fresh))),
-(pk(a, n(a, r1:Fresh) ; N2:Nonce)),
[ nil,
+(pk(b, a ; n(a, r1:Fresh))),
-(pk(a, n(a, r1:Fresh) ; N2:Nonce)),
+(pk(b, N2:Nonce)) | nil] ) || K)[nonexec].
endfm
select MAUDE-NPA .
select MAUDE-NPA .
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment